added TIS interpreter support

diff --git a/.gitignore b/.gitignore
index 4987a3209924b7edcbb2a5b1b79e60d0f25474ff..f160ef631788119752bab2336ae10f953755c60b 100644 (file)
--- a/.gitignore
+++ b/.gitignore
@@ -6,7 +6,7 @@
 *.profraw
 *.profdata
 bin/*
-frama-c/*
+formal-analysis/*
 properties
 vectors
 sodium

diff --git a/frama-c.sh b/frama-c.sh
index 2c4de8b11582cbad1b4faea50d35b3499d725b39..aafad45f6365eb46d950b4e6183c4ab875e07386 100755 (executable)
--- a/frama-c.sh
+++ b/frama-c.sh
@@ -1,7 +1,7 @@
 #! /bin/sh
 
 # Parses the source code
-frama-c frama-c/*.c -cpp-extra-args="-DED25519_SHA512" -save parsed.sav
+frama-c 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

diff --git a/makefile b/makefile
index d27c18a015b53e27c7166f2fc8af0148152e1745..315350964b2017c7a25e9ff87703d24e42281fe5 100644 (file)
--- a/makefile
+++ b/makefile
@@ -27,7 +27,7 @@ CFLAGS= -I src -pedantic -Wall -Wextra -O3 -march=native
 all: vectors properties sodium donna
 
 clean:
-       rm -rf bin frama-c
+       rm -rf bin formal-analysis
        rm -f src/*.gch src/rename_*
        rm -f vectors properties sodium donna speed
 
@@ -114,10 +114,13 @@ rename_%.h: %.h
        sed 's/monocypher.h/rename_monocypher.h/' <$@1 >$@2
        sed 's/sha512.h/rename_sha512.h/'         <$@2 >$@
 
-frama-c: $(GEN_HEADERS)                    \
+formal-analysis: $(GEN_HEADERS)                    \
          src/monocypher.c src/monocypher.h \
          src/sha512.c src/sha512.h         \
          tests/vectors.c
-       @echo copy sources to frama-c directory for analysis
-       @mkdir -p frama-c
-       @cp $^ frama-c
+       @echo "copy sources to formal-analysis directory for analysis (frama-c or TIS)"
+       @mkdir -p formal-analysis
+       @cp $^ formal-analysis
+       @echo "add #define ED25519_SHA512 on top of monocypher.c (for ed25519)"
+       @echo "#define ED25519_SHA512" > formal-analysis/tmp
+       @cat formal-analysis/tmp src/monocypher.c > formal-analysis/monocypher.c