Restored formal analysis scripts

diff --git a/.gitignore b/.gitignore
index 159de6bf59c7472e5cee596ff5c7e87dfc309339..e694a006cbfcb52a6e1b108f5f6224c22032b152 100644 (file)
--- a/.gitignore
+++ b/.gitignore
@@ -9,6 +9,6 @@
 *.sav
 *.profraw
 *.profdata
-formal-analysis/*
+tests/formal-analysis/*
 man/3monocypher/*.html
 tests/vectors.h

diff --git a/README.md b/README.md
index f2eadb27eb33c382d7869ddded6f8712d24ea3fc..6a1a5563e7f8c363031d4b04ed91aeb03c7a13c7 100644 (file)
--- a/README.md
+++ b/README.md
@@ -85,20 +85,18 @@ You can also run the tests under Valgrind:
 
 ### Serious auditing
 
-_TODO: This section is obsolete._
-
 The code may be analysed more formally with [Frama-c][] and the
 [TIS interpreter][TIS].  To analyse the code with Frama-c, run:
 
-    $ make formal-analysis
-    $ ./frama-c.sh
+    $ tests/formal-analysis.sh
+    $ tests/frama-c.sh
 
 This will have Frama-c parse, and analyse the code, then launch a GUI.
 You must have Frama-c installed.  See `frama-c.sh` for the recommended
 settings.  To run the code under the TIS interpreter, run
 
-    $ make formal-analysis
-    $ cd formal-analysis
+    $ tests/formal-analysis.sh
+    $ cd tests/formal-analysis
     $ tis-interpreter.sh *.c
 
 (Note: `tis-interpreter.sh` is part of TIS.  If it is not in your

diff --git a/tests/formal-analysis.sh b/tests/formal-analysis.sh
new file mode 100755 (executable)
index 0000000..5bdbf67
--- /dev/null
+++ b/tests/formal-analysis.sh
@@ -0,0 +1,4 @@
+#! /bin/sh
+
+mkdir -p formal-analysis
+cp src/* tests/utils.c tests/utils.h tests/test.c tests/vectors.h tests/formal-analysis

diff --git a/tests/frama-c.sh b/tests/frama-c.sh
index aafad45f6365eb46d950b4e6183c4ab875e07386..e01624a8702cee72f65060af5cb453b88daf80a8 100755 (executable)
--- a/tests/frama-c.sh
+++ b/tests/frama-c.sh
@@ -1,7 +1,7 @@
 #! /bin/sh
 
 # Parses the source code
-frama-c formal-analysis/*.c -save parsed.sav
+frama-c tests/formal-analysis/*.c -save parsed.sav
 
 # Analyses the source code
 frama-c -load parsed.sav -val-builtins-auto -val -save value.sav -no-val-show-progress -memexec-all