From: Loup Vaillant <loup@loup-vaillant.fr>
Date: Tue, 6 Jun 2017 21:49:12 +0000 (+0200)
Subject: added frama-c analysis
X-Git-Url: https://git.codecow.com/?a=commitdiff_plain;h=cca10293eeb4471d8e2050b4e7fa6c837189cfea;p=Monocypher.git

added frama-c analysis
---

diff --git a/.gitignore b/.gitignore
index 59369ed..682c054 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,7 +2,9 @@
 *~
 *.o
 *.gch
+*.sav
 bin/*
+frama-c/*
 test
 sodium
 donna
diff --git a/README b/README
index 8908dac..33ee6c7 100644
--- a/README
+++ b/README
@@ -7,20 +7,36 @@ Current status
 Test suite
 ----------
 
+    $ make all
     $ ./test.sh
 
 It should display a nice printout of all the tests, all starting with
 "OK".  If you see "FAILURE" anywhere, something has gone very wrong
-somewhere.
+somewhere.  Note: the fuzz tests depend on libsodium.  Install it
+before you run them.
 
 To run only the self contained tests, run
 
     $ make test
     $ ./test
 
+To run only the edDSA fuzz tests (compares Monocypher with
+ed25519-donna), run
+
+    $ make donna
+    $ ./donna
+
 *Do not* use Monocypher without having run the self contained tests at
 least once.
 
+To analyse the code with frama-c, run
+
+    $ make frama-c
+    $ ./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.
 
 Integration to your project
 ---------------------------
diff --git a/frama-c.sh b/frama-c.sh
new file mode 100755
index 0000000..2c4de8b
--- /dev/null
+++ b/frama-c.sh
@@ -0,0 +1,10 @@
+#! /bin/sh
+
+# Parses the source code
+frama-c frama-c/*.c -cpp-extra-args="-DED25519_SHA512" -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
+
+# Launches the Gui
+frama-c-gui -load value.sav
diff --git a/makefile b/makefile
index 4fe8973..2faecac 100644
--- a/makefile
+++ b/makefile
@@ -10,32 +10,35 @@ CFLAGS= -I src -O2 -Wall -Wextra -std=c11 -pedantic
 all: test sodium donna
 
 clean:
-	rm -rf bin
+	rm -rf bin frama-c
 	rm -f src/*.gch src/rename_*
 	rm -f test sodium donna
 
-# Test suite based on test vectors
 TEST_DEPS=tests/test.c bin/monocypher.o bin/sha512.o
-test: $(TEST_DEPS)       \
-      bin/argon2i.h      \
-      bin/blake2b.h      \
-      bin/blake2b_easy.h \
-      bin/chacha20.h     \
-      bin/ed25519_key.h  \
-      bin/ed25519_sign.h \
-      bin/h_chacha20.h   \
-      bin/key_exchange.h \
-      bin/poly1305.h     \
-      bin/v_sha512.h     \
-      bin/x25519.h       \
-      bin/x_chacha20.h
+GEN_HEADERS=bin/argon2i.h      \
+            bin/blake2b.h      \
+            bin/blake2b_easy.h \
+            bin/chacha20.h     \
+            bin/ed25519_key.h  \
+            bin/ed25519_sign.h \
+            bin/h_chacha20.h   \
+            bin/key_exchange.h \
+            bin/poly1305.h     \
+            bin/v_sha512.h     \
+            bin/x25519.h       \
+            bin/x_chacha20.h
+
+# Test suite based on test vectors
+test: $(TEST_DEPS) $(GEN_HEADERS)
 	$(CC) $(CFLAGS) -I bin -o $@ $(TEST_DEPS)
 
 bin/vector: tests/vector_to_header.c
+	@mkdir -p $(@D)
 	$(CC) $(CFLAGS) -o $@ $^
 
 bin/%.h: tests/vectors/% bin/vector
-	bin/vector $$(basename $<) <$< >$@
+	@echo generate $@
+	@bin/vector $$(basename $<) <$< >$@
 
 # Test suite based on comparison with libsodium
 C_SODIUM_FLAGS=$$(pkg-config --cflags libsodium)
@@ -81,3 +84,11 @@ rename_%.h: %.h
 	sed 's/crypto_/rename_/g' <$^ >$@
 	sed 's/monocypher.h/rename_monocypher.h/' -i $@
 	sed 's/sha512.h/rename_sha512.h/'         -i $@
+
+frama-c: $(GEN_HEADERS)                    \
+         src/monocypher.c src/monocypher.h \
+         src/sha512.c src/sha512.h         \
+         tests/test.c
+	@echo copy sources to frama-c directory for analysis
+	@mkdir -p frama-c
+	@cp $^ frama-c