From: Loup Vaillant <loup@loup-vaillant.fr>
Date: Sun, 24 Sep 2017 10:56:48 +0000 (+0200)
Subject: Restored formal analysis scripts
X-Git-Url: https://git.codecow.com/?a=commitdiff_plain;h=a8b105005534216e862076d723be37aa23ced948;p=Monocypher.git

Restored formal analysis scripts
---

diff --git a/.gitignore b/.gitignore
index 159de6b..e694a00 100644
--- 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 f2eadb2..6a1a556 100644
--- 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
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 aafad45..e01624a 100755
--- 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