From: Loup Vaillant <loup@loup-vaillant.fr>
Date: Tue, 18 Jul 2017 17:01:03 +0000 (+0200)
Subject: added TIS interpreter support
X-Git-Url: https://git.codecow.com/?a=commitdiff_plain;h=b9f2a16d728b23ff79fc17ab2f40b15aea7ff845;p=Monocypher.git

added TIS interpreter support
---

diff --git a/.gitignore b/.gitignore
index 4987a32..f160ef6 100644
--- 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 2c4de8b..aafad45 100755
--- 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 d27c18a..3153509 100644
--- 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