.gitignore

@@ -2,7 +2,6 @@
 *.sav
 *.o
 *~
-.frama-c
 config.status
 lia.cache
 
@@ -13,9 +12,6 @@ eva.log
 stats.txt
 flamegraph.txt
 
-# ignore timestamped versions
-*_20*-*.eva
-*_20*-*.parse
 *.error
 
 benchs-value.csv

2048/.frama-c/GNUmakefile

+# Makefile template for Frama-C/Eva case studies.
+# For details and usage information, see the Frama-C User Manual.
+
+### Prologue. Do not modify this block. #######################################
+-include path.mk
+FRAMAC ?= frama-c
+include $(shell $(FRAMAC)-config -scripts)/prologue.mk
+###############################################################################
+
+# Edit below as needed. MACHDEP is mandatory. Suggested flags are optional.
+
+MACHDEP = x86_32
+
+## Preprocessing flags (for -cpp-extra-args)
+CPPFLAGS    += \
+  -CC
+
+## General flags
+FCFLAGS     += \
+  -add-symbolic-path=.:.. \
+  -kernel-warn-key annot:missing-spec=abort \
+  -kernel-warn-key typing:implicit-function-declaration=abort \
+
+## Eva-specific flags
+EVAFLAGS    += \
+  -eva-warn-key builtins:missing-spec=abort \
+
+## GUI-only flags
+FCGUIFLAGS += \
+  -add-symbolic-path=.:.. \
+
+## Analysis targets (suffixed with .eva)
+TARGETS = 2048.eva
+
+### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
+2048.parse: \
+  ../2048.c \
+
+### Epilogue. Do not modify this block. #######################################
+include $(shell $(FRAMAC)-config -scripts)/epilogue.mk
+###############################################################################
+
+# optional, for OSCS
+-include ../../Makefile.common

2048/.frama-c/path.mk

+../../path.mk
\ No newline at end of file

2048/GNUmakefile

-# TEMPLATE FOR MAKEFILE TO USE IN FRAMA-C/EVA CASE STUDIES
-
-# DO NOT EDIT THE LINES BETWEEN THE '#'S
-
-###############################################################################
-# Improves analysis time, at the cost of extra memory usage
-export FRAMA_C_MEMORY_FOOTPRINT = 8
-#
-# frama-c-path.mk contains variables which are specific to each
-# user and should not be versioned, such as the path to the
-# frama-c binaries (e.g. FRAMAC and FRAMAC_GUI).
-# It is an optional include, unnecessary if frama-c is in the PATH
--include frama-c-path.mk
-#
-# FRAMAC_CONFIG is defined in frama-c-path.mk when it is included, so the
-# line below will be safely ignored if this is the case
-FRAMAC_CONFIG ?= frama-c-config
-#
-# frama-c.mk contains the main rules and targets
--include $(shell $(FRAMAC_CONFIG) -print-share-path)/analysis-scripts/frama-c.mk
-#
-###############################################################################
-
-# EDIT VARIABLES AND TARGETS BELOW AS NEEDED
-# The flags below are only suggestions to use with Eva, and can be removed
-
-# (Optional) preprocessing flags, usually handled by -json-compilation-database
-CPPFLAGS    += -CC
-
-# (Optional) Frama-C general flags (parsing and kernel)
-FCFLAGS     += \
-  -kernel-warn-key annot:missing-spec=abort \
-  -kernel-warn-key typing:implicit-function-declaration=abort \
-
-# (Optional) Eva-specific flags
-EVAFLAGS    += \
-  -eva-warn-key builtins:missing-spec=abort \
-
-# (MANDATORY) Name of the main target
-MAIN_TARGET := 2048
-
-# Add other targets if needed
-TARGETS = $(MAIN_TARGET).eva
-
-# Default target
-all: $(TARGETS)
-help:
-	@echo "targets: $(TARGETS)"
-display-targets:
-	@echo "$(TARGETS)"
-
-# (MANDATORY) List of source files used by MAIN_TARGET.
-# If there is a JSON compilation database,
-# 'frama-c-script list-files' can help obtain it
-$(MAIN_TARGET).parse: 2048.c
-
-
-# The following targets are optional and provided for convenience only
-parse: $(TARGETS:%.eva=%.parse)
-gui: $(MAIN_TARGET).eva.gui
-
-stats: $(TARGETS:%.eva=%.parse) $(TARGETS)
-	../show_stats.sh "$(notdir $(CURDIR))" $^
-
-# optional, for OSCS
--include ../Makefile.common

2048/frama-c-path.mk

-../frama-c-path.mk
\ No newline at end of file

Makefile

@@ -70,6 +70,7 @@ TARGETS=\
   papabench \
   polarssl \
   qlz \
+  safestringlib \
   semver \
   solitaire \
   tweetnacl-usable \
@@ -85,30 +86,33 @@ QUICK_TARGETS=$(filter-out polarssl gzip124 libmodbus monocypher chrony,$(TARGET
 
 all: $(TARGETS)
 
+summary:
+	frama-c/share/analysis-scripts/summary.py
+
 $(TARGETS):
-	+$(MAKE) -C $@
+	+$(MAKE) -C $@/.frama-c
 
 quick: $(QUICK_TARGETS)
 
 %.clean:
-	$(MAKE) -C $* clean
+	$(MAKE) -C $*/.frama-c clean
 
 clean: $(addsuffix .clean,$(TARGETS))
 
 %.parse:
-	$(MAKE) -C $* parse
+	$(MAKE) -C $*/.frama-c parse
 
 parse: $(addsuffix .parse,$(TARGETS))
 
 %.stats:
-	$(MAKE) -C $* stats
+	$(MAKE) -C $*/.frama-c stats
 
 stats: $(addsuffix .stats,$(TARGETS))
 
 display-targets:
 	@echo $(foreach target,$(TARGETS),\
 	        $(addprefix $(target)/,\
-	          $(shell $(MAKE) --quiet -C $(target) display-targets)))
+	          $(shell $(MAKE) --quiet -C $(target)/.frama-c display-targets)))
 
 .PHONY: $(TARGETS) frama-c/build/bin/frama-c clean-all help stats-all
 

README.md

@@ -141,6 +141,7 @@ when available. We also summarize the license of each directory below.
 - `papabench`: GPL
 - `polarssl`: GPL
 - `qlz`: GPL
+- `safestringlib`: MIT
 - `semver`: MIT
 - `solitaire`: public domain (see `solitaire.c`)
 - `tweetnacl-usable`: public domain (see `LICENSE.txt`)

basic-cwe-examples/.frama-c/GNUmakefile

+# Makefile template for Frama-C/Eva case studies.
+# For details and usage information, see the Frama-C User Manual.
+
+### Prologue. Do not modify this block. #######################################
+-include path.mk
+FRAMAC ?= frama-c
+include $(shell $(FRAMAC)-config -scripts)/prologue.mk
+###############################################################################
+
+# Edit below as needed. MACHDEP is mandatory. Suggested flags are optional.
+
+MACHDEP = x86_32
+
+## Preprocessing flags (for -cpp-extra-args)
+CPPFLAGS    += \
+
+## General flags
+FCFLAGS     += \
+  -add-symbolic-path=.:.. \
+  -kernel-warn-key annot:missing-spec=abort \
+  -kernel-warn-key typing:implicit-function-declaration=abort \
+
+# (Optional) Eva-specific flags
+EVAFLAGS    += \
+  -eva-warn-key builtins:missing-spec=abort \
+
+## Analysis targets (suffixed with .eva)
+IMPRECISE_TARGETS = cwe20.eva cwe119.eva cwe190.eva cwe416.eva cwe787.eva
+
+PRECISE_TARGETS = $(subst .eva,-precise.eva,$(IMPRECISE_TARGETS))
+
+TARGETS = $(IMPRECISE_TARGETS) $(PRECISE_TARGETS)
+
+### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
+cwe20.parse:  ../cwe20.c
+cwe119.parse: ../cwe119.c
+cwe190.parse: ../cwe190.c
+cwe416.parse: ../cwe416.c
+cwe787.parse: ../cwe787.c
+
+cwe20-precise.parse:  ../cwe20.c
+cwe119-precise.parse: ../cwe119.c
+cwe190-precise.parse: ../cwe190.c
+cwe416-precise.parse: ../cwe416.c
+cwe787-precise.parse: ../cwe787.c
+
+cwe20-precise.eva:  EVAFLAGS +=
+cwe119-precise.eva: EVAFLAGS += -eva-precision 1
+cwe190-precise.eva: EVAFLAGS += -warn-unsigned-overflow -eva-no-alloc-returns-null
+cwe416-precise.eva: EVAFLAGS += -eva-precision 1
+cwe787-precise.eva: EVAFLAGS += -eva-precision 2 -eva-no-alloc-returns-null
+
+### Epilogue. Do not modify this block. #######################################
+include $(shell $(FRAMAC)-config -scripts)/epilogue.mk
+###############################################################################
+
+# optional, for OSCS
+-include ../../Makefile.common