From: Loup Vaillant <loup@loup-vaillant.fr>
Date: Thu, 30 May 2019 22:33:54 +0000 (+0200)
Subject: Worked around TIS interpreter volatile bug
X-Git-Url: https://git.codecow.com/?a=commitdiff_plain;h=1c658ef8dee04fae3069426af6ca08bd699fbabb;p=Monocypher.git

Worked around TIS interpreter volatile bug
---

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/