added frama-c analysis

diff --git a/.gitignore b/.gitignore
index 59369ed327d2a4c5c2865a751f88ef0d46ca5b4c..682c054273ad90fe9ffe96d8ec88eb6cdab4fc47 100644 (file)
--- a/.gitignore
+++ b/.gitignore
@@ -2,7 +2,9 @@
 *~
 *.o
 *.gch
+*.sav
 bin/*
+frama-c/*
 test
 sodium
 donna

diff --git a/README b/README
index 8908dac88363dff2636a4964b31da32b97072f92..33ee6c7e4662d3aaf8e5fe1f932e570476b9d95d 100644 (file)
--- 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 (executable)
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 4fe8973137b7b298eb690e2d8c088db9f6e49dee..2faecacff614771774c2e3b43faec10c5fee4ae8 100644 (file)
--- 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