From 1c658ef8dee04fae3069426af6ca08bd699fbabb Mon Sep 17 00:00:00 2001 From: Loup Vaillant Date: Fri, 31 May 2019 00:33:54 +0200 Subject: [PATCH] Worked around TIS interpreter volatile bug --- README.md | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 6bd2a33..3d41396 100644 --- a/README.md +++ b/README.md @@ -102,10 +102,18 @@ You must have Frama-c installed. See `frama-c.sh` for the recommended settings. To run the code under the TIS interpreter, run $ tests/formal-analysis.sh - $ tis-interpreter.sh tests/formal-analysis/*.c + $ tis-interpreter.sh --cc -Dvolatile= tests/formal-analysis/*.c -(Note: `tis-interpreter.sh` is part of TIS. If it is not in your -path, adjust the command accordingly.) +Notes: + +- `tis-interpreter.sh` is part of TIS. If it is not in your path, + adjust the command accordingly. + +- The TIS interpreter sometimes fails to evaluate correct programs when + they use the `volatile` keyword (which is only used as an attempt to + prevent dead store elimination for memory wipes). The `-cc + -Dvolatile=` option works around that bug by ignoring `volatile` + altogether. [Frama-c]:https://frama-c.com/ [TIS]: https://trust-in-soft.com/tis-interpreter/ -- 2.47.3