.githooks/pre-commit

+#!/usr/bin/sh
+
+# Redirect output to stderr.
+exec 1>&2
+
+errors=0
+
+for p in $(git ls-files '*/.frama-c/path.mk'); do
+    if [ ! -L "$p" ]; then
+       echo "pre-commit error: $p should be a symbolic link"
+       errors=$((errors+1))
+    fi
+done
+
+if [ $errors -gt 0 ]; then
+   echo "$errors error(s), aborting commit. Add '--no-verify' to bypass hooks."
+   exit 1
+fi

.gitignore

@@ -13,6 +13,16 @@ stats.txt
 flamegraph.txt
 
 *.error
+*.break
+*#
 
 benchs-value.csv
 bench_clone
+
+.vscode/
+
+.ivette
+
+# SARIF files are currently not versioned
+*.sarif
+*.reparse

.gitlab-ci.yml

+default:
+  image: framac/frama-c:dev
+
+variables:
+  GIT_CLEAN_FLAGS: none #each use case cleans its own directory
+
+__update-summary:
+  tags:
+    - docker
+  script:
+    - git config --global --add safe.directory $PWD
+    - ./compute-summary.sh
+    - git diff --exit-code summary.md
+
+.make_job: &make_job
+  tags:
+    - docker
+  script:
+    - make -C $TARGET/.frama-c clean
+    - make $TARGET
+    # note: the command below is needed due to recent git releases, which
+    #       enforce stricter permission controls w.r.t to ownership of '.git'.
+    - git config --global --add safe.directory $PWD
+    - git diff --exit-code $TARGET
+    - make $TARGET.sarif
+  artifacts:
+    paths:
+    - "$TARGET/.frama-c/*.sarif"
+
+_2048:
+  variables:
+    TARGET: 2048
+  <<: *make_job
+
+basic-cwe-examples:
+  variables:
+    TARGET: basic-cwe-examples
+  <<: *make_job
+
+bench-moerman2018:
+  variables:
+    TARGET: bench-moerman2018
+  <<: *make_job
+
+cerberus:
+  variables:
+    TARGET: cerberus
+  <<: *make_job
+
+chrony:
+  variables:
+    TARGET: chrony
+  <<: *make_job
+
+c-testsuite:
+  variables:
+    TARGET: c-testsuite
+  <<: *make_job
+
+c-utils:
+  variables:
+    TARGET: c-utils
+  <<: *make_job
+
+debie1:
+  variables:
+    TARGET: debie1
+  <<: *make_job
+
+genann:
+  variables:
+    TARGET: genann
+  <<: *make_job
+
+gnugo:
+  variables:
+    TARGET: gnugo
+  <<: *make_job
+
+gzip124:
+  variables:
+    TARGET: gzip124
+  <<: *make_job
+
+hiredis:
+  variables:
+    TARGET: hiredis
+  <<: *make_job
+
+icpc:
+  variables:
+    TARGET: icpc
+  <<: *make_job
+
+ioccc:
+  variables:
+    TARGET: ioccc
+  <<: *make_job
+
+itc-benchmarks:
+  variables:
+    TARGET: itc-benchmarks
+  <<: *make_job
+
+jsmn:
+  variables:
+    TARGET: jsmn
+  <<: *make_job
+
+kgflags:
+  variables:
+    TARGET: kgflags
+  <<: *make_job
+
+khash:
+  variables:
+    TARGET: khash
+  <<: *make_job
+
+kilo:
+  variables:
+    TARGET: kilo
+  <<: *make_job
+
+libmodbus:
+  variables:
+    TARGET: libmodbus
+  <<: *make_job
+
+libspng:
+  variables:
+    TARGET: libspng
+  <<: *make_job
+
+libyaml:
+  variables:
+    TARGET: libyaml
+  <<: *make_job
+
+line-following-robot:
+  variables:
+    TARGET: line-following-robot
+  <<: *make_job
+
+microstrain:
+  variables:
+    TARGET: microstrain
+  <<: *make_job
+
+mini-gmp:
+  variables:
+    TARGET: mini-gmp
+  <<: *make_job
+
+miniz:
+  variables:
+    TARGET: miniz
+  <<: *make_job
+
+monocypher:
+  variables:
+    TARGET: monocypher
+  <<: *make_job
+
+papabench:
+  variables:
+    TARGET: papabench
+  <<: *make_job
+
+polarssl:
+  variables:
+    TARGET: polarssl
+  <<: *make_job
+
+powerwindow:
+  variables:
+    TARGET: powerwindow
+  <<: *make_job
+
+qlz:
+  variables:
+    TARGET: qlz
+  <<: *make_job
+
+safestringlib:
+  variables:
+    TARGET: safestringlib
+  <<: *make_job
+
+semver:
+  variables:
+    TARGET: semver
+  <<: *make_job
+
+solitaire:
+  variables:
+    TARGET: solitaire
+  <<: *make_job
+
+stmr:
+  variables:
+    TARGET: stmr
+  <<: *make_job
+
+tsvc:
+  variables:
+    TARGET: tsvc
+  <<: *make_job
+
+tweetnacl-usable:
+  variables:
+    TARGET: tweetnacl-usable
+  <<: *make_job
+
+verisec:
+  variables:
+    TARGET: verisec
+  <<: *make_job
+
+x509-parser:
+  variables:
+    TARGET: x509-parser
+  <<: *make_job

2048/.frama-c/2048.eva/alarms.csv

 directory	file	line	function	property kind	status	property
 .	2048.c	37	getColor	mem_access	Unknown	\valid_read(foreground)
 .	2048.c	51	drawBoard	precondition of printf_va_3	Unknown	valid_read_string(param0)
-.	2048.c	51	printf_va_3	precondition	Unknown	valid_read_string(param0)
 .	2048.c	58	drawBoard	precondition of printf_va_7	Unknown	valid_read_string(param0)
-.	2048.c	58	printf_va_7	precondition	Unknown	valid_read_string(param0)
 .	2048.c	61	drawBoard	shift	Unknown	0 ≤ (int)(*(board + x))[y] < 32
 .	2048.c	62	drawBoard	precondition of strlen	Unknown	valid_string_s: valid_read_string(s)
 .	2048.c	63	drawBoard	precondition of printf_va_8	Unknown	valid_read_string(param2)
-.	2048.c	63	printf_va_8	precondition	Unknown	valid_read_string(param2)
 .	2048.c	72	drawBoard	precondition of printf_va_12	Unknown	valid_read_string(param0)
-.	2048.c	72	printf_va_12	precondition	Unknown	valid_read_string(param0)
 .	2048.c	90	findTarget	mem_access	Unknown	\valid_read(array + t)
 .	2048.c	123	slideArray	shift	Unknown	0 ≤ (int)*(array + t) < 32
 .	2048.c	249	addRandom	initialization	Unknown	\initialized(&list[r][0])
 .	2048.c	250	addRandom	initialization	Unknown	\initialized(&list[r][1])
 .	2048.c	287	setBufferedInput	initialization	Unknown	\initialized(&new.c_lflag)
-FRAMAC_SHARE/libc	string.h	125	strlen	precondition	Unknown	valid_string_s: valid_read_string(s)
+FRAMAC_SHARE/libc	stdio.h	253	printf_va_12	precondition	Unknown	valid_read_string(param0)
+FRAMAC_SHARE/libc	stdio.h	253	printf_va_3	precondition	Unknown	valid_read_string(param0)
+FRAMAC_SHARE/libc	stdio.h	253	printf_va_7	precondition	Unknown	valid_read_string(param0)
+FRAMAC_SHARE/libc	stdio.h	253	printf_va_8	precondition	Unknown	valid_read_string(param2)
+FRAMAC_SHARE/libc	string.h	168	strlen	precondition	Unknown	valid_string_s: valid_read_string(s)

2048/.frama-c/2048.eva/metrics.log

@@ -11,7 +11,7 @@ Unreached functions (1) =
 Function main references signal_callback_handler (at 2048.c:383)
 [metrics] Statements analyzed by Eva
 --------------------------
-329 stmts in analyzed functions, 326 stmts analyzed (99.1%)
+328 stmts in analyzed functions, 325 stmts analyzed (99.1%)
 addRandom: 32 stmts out of 32 (100.0%)
 countEmpty: 16 stmts out of 16 (100.0%)
 drawBoard: 51 stmts out of 51 (100.0%)
@@ -19,7 +19,7 @@ findPairDown: 19 stmts out of 19 (100.0%)
 gameEnded: 20 stmts out of 20 (100.0%)
 getColor: 20 stmts out of 20 (100.0%)
 initBoard: 18 stmts out of 18 (100.0%)
-main: 48 stmts out of 48 (100.0%)
+main: 47 stmts out of 47 (100.0%)
 moveDown: 6 stmts out of 6 (100.0%)
 moveLeft: 6 stmts out of 6 (100.0%)
 moveRight: 6 stmts out of 6 (100.0%)

2048/.frama-c/2048.parse/metrics.log

@@ -26,7 +26,7 @@ Potential entry points (2)
 
 Global metrics
 ============== 
-Sloc = 399
+Sloc = 398
 Decision point = 61
 Global variables = 5
 If = 57

2048/.frama-c/2048.parse/warnings.log

-2048.c:46:[variadic] warning: Incorrect type for argument 2. The argument will be cast from uint32_t to int.
+2048.c:46:[variadic:typing] warning: Incorrect type for argument 2. The argument will be cast from uint32_t to int.

2048/.frama-c/GNUmakefile

@@ -4,10 +4,10 @@
 ### Prologue. Do not modify this block. #######################################
 -include path.mk
 FRAMAC ?= frama-c
-include $(shell $(FRAMAC)-config -scripts)/prologue.mk
+include $(shell $(FRAMAC)-config -print-lib-path)/analysis-scripts/prologue.mk
 ###############################################################################
 
-# Edit below as needed. MACHDEP is mandatory. Suggested flags are optional.
+# Edit below as needed. Suggested flags are optional.
 
 MACHDEP = x86_32
 
@@ -17,7 +17,7 @@ CPPFLAGS    += \
 
 ## General flags
 FCFLAGS     += \
-  -add-symbolic-path=.:.. \
+  -add-symbolic-path=..:. \
   -kernel-warn-key annot:missing-spec=abort \
   -kernel-warn-key typing:implicit-function-declaration=abort \
 
@@ -27,7 +27,6 @@ EVAFLAGS    += \
 
 ## GUI-only flags
 FCGUIFLAGS += \
-  -add-symbolic-path=.:.. \
 
 ## Analysis targets (suffixed with .eva)
 TARGETS = 2048.eva
@@ -37,7 +36,7 @@ TARGETS = 2048.eva
   ../2048.c \
 
 ### Epilogue. Do not modify this block. #######################################
-include $(shell $(FRAMAC)-config -scripts)/epilogue.mk
+include $(shell $(FRAMAC)-config -print-lib-path)/analysis-scripts/epilogue.mk
 ###############################################################################
 
 # optional, for OSCS

2048/.gitignore

+2048

2048/Makefile

+../Makefile.single-target
\ No newline at end of file

2048/OSCS-README.txt

+Console version of the game 2048
+https://github.com/mevdschee/2048.c
+NO_DYN_ALLOC, NO_RECURSION, NO_FLOAT

Makefile

 .ONESHELL:
+ROOT_DIR := $(dir $(realpath $(lastword $(MAKEFILE_LIST))))
 
 help::
 	@echo "*** PREPARATION TARGETS (first-time user)"
@@ -15,7 +16,15 @@ help::
 	@echo "- 'make clean': clean all analyses"
 	@echo ""
 	@echo "*** USAGE WITH FRAMA-C INSTALLED IN THE PATH"
-	@echo "- delete 'frama-c-path.mk' or comment its lines"
+	@echo "- delete 'path.mk' or comment its lines"
+	@echo ""
+	@echo "*** NON-FRAMA-C BUILD TARGETS"
+	@echo "- 'make build': build each case study, using its own Makefile,"
+	@echo "  CMake, Meson, etc. You can set BUILD_WRAPPER to a command"
+	@echo "  which will wrap the calls to the build tool."
+	@echo "  Note: this is highly system-dependent and requires several"
+	@echo "  libraries and tools. This target is only provided for "
+	@echo "  convenience, and cannot be relied upon for CI runs."
 
 # Note: if the user runs `make framac` before `make submodules`, the latter
 # will fail.
@@ -33,49 +42,55 @@ framac: frama-c/build/bin/frama-c
 # a submodule, it does not have a `.git` directory.
 # also, such dependency would prevent usage with FRAMAC=path/to/other/framac
 frama-c/build/bin/frama-c:
-	@echo "Compiling and installing local Frama-C..."
+	@echo "Compiling and (re)installing local Frama-C..."
 	mkdir -p frama-c/build
-	{
-	  cd frama-c
-	  echo "*** running autoconf..."
-	  autoconf -f >/dev/null 2>/dev/null
-	  echo "*** running configure..."
-	  ./configure --prefix=`pwd`/build --quiet >/dev/null
-	  $(MAKE) clean >/dev/null
-	  echo "*** running make..."
-	  $(MAKE) -j --quiet >/dev/null
-	  echo "*** running make install..."
-	  $(MAKE) install >/dev/null
-	};
+	echo "*** cleaning previous builds..."
+	$(MAKE) -C frama-c clean >/dev/null
+	echo "*** running make..."
+	$(MAKE) -C frama-c -j --quiet >/dev/null
+	echo "*** running make install..."
+	$(MAKE) -C frama-c install PREFIX=$(ROOT_DIR)/frama-c/build >/dev/null
 	echo "Local Frama-C (re-)installed."
 
 TARGETS=\
   2048 \
   basic-cwe-examples \
   bench-moerman2018 \
+  c-testsuite \
+  c-utils \
   cerberus \
   chrony \
   debie1 \
+  genann \
+  gnugo \
   gzip124 \
   hiredis \
   icpc \
+  ioccc \
   itc-benchmarks \
   jsmn \
+  kgflags \
   khash \
   kilo \
   libmodbus \
   libspng \
+  libyaml \
+  line-following-robot \
   microstrain \
   mini-gmp \
   miniz \
   monocypher \
   papabench \
   polarssl \
+  powerwindow \
   qlz \
   safestringlib \
   semver \
   solitaire \
+  stmr \
+  tsvc \
   tweetnacl-usable \
+  verisec \
   x509-parser \
 
 help::
@@ -83,10 +98,15 @@ help::
 	@echo "Known targets:"
 	@echo "$(sort $(TARGETS))"
 
-# A target for "fast" analyses, used to speed up testing
-QUICK_TARGETS=$(filter-out polarssl gzip124 libmodbus monocypher chrony,$(TARGETS))
+# Targets sorted by "longest-running first"
+SLOW_TARGETS=monocypher chrony debie1 polarssl libmodbus
+
+QUICK_TARGETS=$(filter-out $(SLOW_TARGETS),$(TARGETS))
 
-all: $(TARGETS)
+# Start long-running targets first, to minimize overall wall-clock time
+# Note: we rely on the fact that GNU make tends to start running targets
+# in left-to-right order
+all: $(SLOW_TARGETS) $(QUICK_TARGETS)
 
 summary:
 	frama-c/share/analysis-scripts/summary.py
@@ -106,22 +126,43 @@ clean: $(addsuffix .clean,$(TARGETS))
 
 parse: $(addsuffix .parse,$(TARGETS))
 
-%.stats:
-	$(MAKE) -C $*/.frama-c stats
+%.sarif:
+	$(MAKE) -C $*/.frama-c sarif
 
-stats: $(addsuffix .stats,$(TARGETS))
+sarif: $(addsuffix .sarif,$(TARGETS))
 
 display-targets:
 	@echo $(foreach target,$(TARGETS),\
 	        $(addprefix $(target)/,\
 	          $(shell $(MAKE) --quiet -C $(target)/.frama-c display-targets)))
 
-.PHONY: $(TARGETS) frama-c/build/bin/frama-c clean-all help stats-all
+%.eva: .FORCE
+	$(MAKE) -C $(dir $@) $(notdir $@)
+
+# For most case studies, 'make' is sufficient, but some of them require other
+# commands (which are overridden below).
+%.build:
+	$(BUILD_WRAPPER) $(MAKE) -C $*
+
+%.build.clean:
+	$(MAKE) -C $* clean
+
+build: $(addsuffix .build,$(TARGETS))
+
+build-clean: $(addsuffix .build.clean,$(TARGETS))
+
+cerberus.build:
+	@echo "Some Cerberus tests are not compilable (by design)"
+
+cerberus.build.clean:
+	@echo "Cerberus: nothing to clean"
+
+icpc.build:
+	$(BUILD_WRAPPER) $(MAKE) -C icpc/src
+
+icpc.build.clean:
+	$(MAKE) -C icpc/src clean
 
-# for continuous integration: runs all tests, then uses git status and
-# git diff to check for unexpected differences
-ci-tests: all stats-all
-	git status --porcelain
-	git diff --exit-code
+.FORCE:
 
-ci-tests: export FCFLAGS=-value-verbose 0 -kernel-verbose 0
+.PHONY: $(TARGETS) frama-c/build/bin/frama-c help

Makefile.common

 # Makefile optionally included by each GNUmakefile in the target directories.
 # Note: it must be included at the end of the makefiles,
 # to ensure e.g. TARGETS and other variables are properly defined.
+
+### Extra targets for SARIF report
+# '-noautoload-plugins -load-module eva,markdown-report' minimize loading time
+# of several dozens of calls to Frama-C
+%.sarif: %.eva
+	$(FRAMAC) -no-autoload-plugins -load-module eva,markdown-report -load $^/framac.sav -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic -mdr-out $@
+
+sarif: $(TARGETS:%.eva=%.sarif)

Makefile.single-target

+# This is a generic Makefile for directories containing a single target that
+# have do not already have a Makefile themselves.
+
+# This Makefile is NOT for running Frama-C, but for compiling the case study
+# itself.
+
+# Usage: `cd` to directory and `ln -s ../Makefile.single-target Makefile`
+
+TARGET = $(shell basename `pwd`)
+
+SOURCES := $(sort $(wildcard *.c))
+
+all: $(TARGET)
+
+# Some directories complement this Makefile with their own
+-include Makefile.own
+
+$(TARGET): $(SOURCES)
+	$(CC) $(CPPFLAGS) $(CFLAGS) -o $@ $^ $(LDFLAGS)
+
+clean:
+	rm -f $(TARGET)
+
+.PHONY: clean

README.md

+![Pipeline status badge](https://git.frama-c.com/pub/open-source-case-studies/badges/master/pipeline.svg)
+
 Open source case studies for Frama-C
 ====================================
 
@@ -12,7 +14,7 @@ A few contain sets of tests, benchmarks or tutorials.
 # Requirements
 
 - GNU Make >= 4.0;
-- (optional, for some scripts) Python >= 3.6.
+- (optional, for some scripts) Python >= 3.7.
 
 # Basic usage
 
@@ -20,17 +22,24 @@ A few contain sets of tests, benchmarks or tutorials.
 - (required once) `make framac`: prepares a git submodule with a clone
   of the public git of Frama-C, compiles it and installs it locally
   (in `frama-c/build/bin`);
-- `cd` to one of the case studies;
+- (required once) add the following alias to your shell:
+
+        alias fcmake='make -C .frama-c'
+
+  Each "case study" contains a `.frama-c` subdirectory with the Frama-C
+  Makefile. Running `fcmake` will run Frama-C related targets;
+  running `make` will run the case study's original Makefile (if it exists).
+- `cd` to the subdirectory of one of the case studies;
   We recommend `2048` for a short and fast analysis, or `debie1` for
   a finalized analysis.
-- Run `make` to parse and run Eva on the predefined targets.
+- Run `fcmake` to parse and run Eva on the predefined targets.
 
 ## Makefile targets
 
 The scripts provided with Frama-C create several Makefile targets,
 according to the intended usage. The main ones are:
 
-- `help`: lists the base targets
+- `display-targets`: lists the base targets
 - For each base target `t`, the following targets are generated:
   - `t.parse`: parse the sources;
   - `t.eva`: run Eva;
@@ -49,37 +58,40 @@ Other generated targets:
 
 - The output of `t.eva` is verbose, but you can ignore it;
   the important information (warnings and alarms) can be inspected via the GUI.
-- The result of each analysis is stored in a directory containing the full logs
-  and Frama-C save files; successive runs are copied into timestamped
-  directories, to allow comparing them (e.g. via `meld`);
+- The result of the analysis is stored inside `.frama-c`, in subdirectories
+  `t.parse` for parsing and `t.eva` for the Eva analysis.
+  Each subdirectory contains a few log files.
 - To try other parametrizations, simply edit variables
-  `CPPFLAGS/FCFLAGS/EVAFLAGS` in `GNUmakefile` and re-run `make`.
-- Technical remark: the default file used by GNU Make is `GNUmakefile`,
-  if it exists.
-  We use this to avoid renaming the original Makefile, if any. It also means
-  that, if you want to *compile* the code using its Makefile, you have to
-  explicitly name it (e.g. `make -f Makefile`).
-
+  `CPPFLAGS/FCFLAGS/EVAFLAGS` in `.frama-c/GNUmakefile` and re-run `fcmake`.
 
 # Notes
 
+A summary of the case studies, with a brief description, URL, number of Eva
+targets, etc, is available at [summary.md](summary.md).
+
 ## Source code modifications
 
-Only minor modifications were performed on each of these case studies:
-
-- File `GNUmakefile` is added to each case study, with Frama-C/Eva-specific
-  rules for parsing and running the analysis;
-- When necessary, syntactic modifications were performed to ensure better
-  C99-compliance and/or the inclusion of stubs to allow Frama-C to parse the
-  files;
-- In some cases, an `eva_main` function was added to provide a better initial
-  context for the analysis;
-- When recursive calls are present, the functions containing them need to be
-  replaced with specifications;
-- Some ACSL annotations were added to the sources
-  (to illustrate their usage, or to improve the analysis);
+We attempt to minimize changes to each case study, to keep the code close to
+the original. Here are the most common kinds of changes:
+
+- A `.frama-c` directory is added, with a `GNUmakefile` which defines the
+  Frama-C targets and parameters;
+- Some stubs file (e.g. `stubs.c`) are added to the `.frama-c` directory,
+  either to emulate an initial state with command-line arguments, or to provide
+  code/specifications for library functions, missing code, non-portable
+  features, etc.
+- When code modifications are needed (and cannot be moved to the stubs file,
+  e.g. when adding a specification to a `static` functions), we often
+  protect them by `#ifdef __FRAMAC__` guards, to ensure the code compiles
+  as before when not using Frama-C. Note that this is not always the case.
 - Some unnecessary files for the analysis (e.g. documentation, project setups
-  for IDEs, non-code resources) were removed.
+  for IDEs, non-code resources) are removed.
+- Some Makefiles were renamed `Makefile.original`, and a simplified
+  OSCS-related `Makefile` has been added. This enables compiling some targets
+  in a way that is useful for certain build tools.
+
+In case studies related to benchmarking, examples or test suites, we often
+apply modifications more liberally.
 
 ## Rationale
 
@@ -98,7 +110,7 @@ Only a few constitute "finalized" case studies.
 
 If you know of other open source code bases where Frama-C/Eva produces
 interesting results, please contribute with pull requests including the
-sources and the `GNUmakefile` that you have devised to run Frama-C.
+case study sources and your `.frama-c/GNUmakefile`.
 
 On the other hand, if you have some interesting open-source C software
 (ideally, C99-compatible) that you are unable to parse and/or run with
@@ -121,30 +133,74 @@ when available. We also summarize the license of each directory below.
 - `2048`: MIT
 - `basic-cwe-examples`: see `LICENSE`
 - `bench-moerman2018`: MIT
+- `c-testsuite`: see `LICENSE` and `LICENSE-tests`
+- `c-utils` : MIT
+- `cerberus`: see `LICENSE`
 - `chrony`: GPL
 - `debie1`: distribution and use authorized by Patria Aviation Oy,
             Space Systems Finland Ltd. and Tidorum Ltd, see `README.txt`
             and `terms_of_use-2014-05.pdf`
+- `genann`: Zlib, see `LICENSE`
+- `gnugo`: GPL
 - `gzip124`: GPL
 - `hiredis`: Redis license (BSD-style), see `COPYING`
 - `icpc`: Unlicense
+- `ioccc`: Creative Commons Attribution-ShareAlike 3.0 Unported (CC BY-SA 3.0),
+           see `COPYING`
 - `itc-benchmarks`: BSD 2-clause, see `COPYING`
 - `jsmn`: MIT
+- `kgflags`: MIT, see `LICENSE`
 - `khash`: MIT
-- `kilo`: BSD 2-clause "Simplified"
-          (see https://github.com/antirez/kilo/blob/master/LICENSE)
+- `kilo`: BSD 2-clause "Simplified", see `LICENSE`
 - `libmodbus`: LGPL
 - `libspng`: BSD 2-clause, see `LICENSE`
-- `mibench`: several (see `LICENSE` file inside each subdirectory)
+- `libyaml`: MIT, see `License`
+- `line-following-robot`: MIT + modified BSD (for included `avr-libc`),
+                          see `LICENSE` and `avr-libc/include/LICENSE`
+- `mibench`: several, see `LICENSE` file inside each subdirectory
 - `mini-gmp`:  LGPL or GPL
 - `miniz`:  MIT
 - `microstrain`: GPL and others, see `LICENSE`
 - `monocypher`: see `README`
 - `papabench`: GPL
 - `polarssl`: GPL
+- `powerwindow`: GPL
 - `qlz`: GPL
 - `safestringlib`: MIT
 - `semver`: MIT
-- `solitaire`: public domain (see `solitaire.c`)
-- `tweetnacl-usable`: public domain (see `LICENSE.txt`)
-- `x509-parser` : GPLv2 / BSD (see `LICENSE`)
+- `solitaire`: public domain, see `solitaire.c`
+- `stmr`: MIT
+- `tsvc`: MIT, see `license.txt`
+- `tweetnacl-usable`: public domain, see `LICENSE.txt`
+- `verisec`: several, according to each app
+- `x509-parser` : GPLv2 / BSD, see `LICENSE`
+
+
+# Troubleshooting / Debugging
+
+(This section is mainly for Frama-C/plug-in developers who want to test OSCS
+with specific versions of Frama-C)
+
+OSCS can work in different modes:
+
+1. With a local Frama-C, installed via the Git submodule 'frama-c'
+   (after running `make framac`);
+2. With another, locally-installed Frama-C;
+3. With Frama-C installed in the PATH.
+
+This behavior is defined in `path.mk`. This file is included (as a symbolic
+link) in the `.frama-c` directory for each case study. Changing this file will
+change the behavior of all case studies.
+
+- Mode 1 (by default) is enabled as soon as `make framac` is executed.
+- To enable mode 2, modify the `FRAMAC_DIR=` line in `path.mk` to point to the
+  `bin` directory of your locally installed Frama-C.
+- To enable mode 3, simply comment the `FRAMAC_DIR=` line.
+
+If the value of `FRAMAC_DIR` is invalid (does not point to an existing
+directory), an error will be raised.
+
+If you need help debugging, consider adding messages such as
+`$(info FRAMAC_DIR is: $(FRAMAC_DIR))` to `path.mk`.
+When running one of the `make` targets, these messages might help understand
+if the path has been properly set.

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

@@ -4,54 +4,70 @@
 ### Prologue. Do not modify this block. #######################################
 -include path.mk
 FRAMAC ?= frama-c
-include $(shell $(FRAMAC)-config -scripts)/prologue.mk
+include $(shell $(FRAMAC)-config -print-lib-path)/analysis-scripts/prologue.mk
 ###############################################################################
 
-# Edit below as needed. MACHDEP is mandatory. Suggested flags are optional.
+# Edit below as needed. Suggested flags are optional.
 
-MACHDEP = x86_32
+MACHDEP = x86_64
 
 ## Preprocessing flags (for -cpp-extra-args)
 CPPFLAGS    += \
 
 ## General flags
 FCFLAGS     += \
-  -add-symbolic-path=.:.. \
+  -add-symbolic-path=..:. \
   -kernel-warn-key annot:missing-spec=abort \
   -kernel-warn-key typing:implicit-function-declaration=abort \
 
-# (Optional) Eva-specific flags
+## 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
+IMPRECISE_TARGETS = cwe20.eva cwe20-2.eva cwe119.eva cwe190.eva cwe416.eva cwe588.eva cwe761.eva cwe787.eva
 
 PRECISE_TARGETS = $(subst .eva,-precise.eva,$(IMPRECISE_TARGETS))
 
-TARGETS = $(IMPRECISE_TARGETS) $(PRECISE_TARGETS)
+OTHER_TARGETS = cwe190-unsigned.eva
+
+TARGETS = $(IMPRECISE_TARGETS) $(PRECISE_TARGETS) $(OTHER_TARGETS)
 
 ### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
 cwe20.parse:  ../cwe20.c
+cwe20-2.parse:  ../cwe20-2.c
 cwe119.parse: ../cwe119.c
 cwe190.parse: ../cwe190.c
 cwe416.parse: ../cwe416.c
+cwe588.parse: ../cwe588.c
+cwe761.parse: ../cwe761.c
 cwe787.parse: ../cwe787.c
 
 cwe20-precise.parse:  ../cwe20.c
+cwe20-2-precise.parse:  ../cwe20-2.c
 cwe119-precise.parse: ../cwe119.c
 cwe190-precise.parse: ../cwe190.c
 cwe416-precise.parse: ../cwe416.c
+cwe588-precise.parse: ../cwe588.c
+cwe761-precise.parse: ../cwe761.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
+cwe761-precise.parse: CPPFLAGS+=-DFC_EVA_PRECISE
+
+cwe190-unsigned.parse: ../cwe190-unsigned.c
+
+cwe20-precise.eva:   EVAFLAGS +=
+cwe20-2-precise.eva: EVAFLAGS += -eva-precision 5
+cwe119-precise.eva:  EVAFLAGS +=
+cwe190-precise.eva:  EVAFLAGS +=
+cwe416-precise.eva:  EVAFLAGS +=
+cwe588-precise.eva:  EVAFLAGS +=
+cwe761-precise.eva:  EVAFLAGS += -eva-precision 1
+cwe787-precise.eva:  EVAFLAGS += -eva-precision 2
+cwe190-unsigned.eva:  EVAFLAGS += -warn-unsigned-overflow
 
 ### Epilogue. Do not modify this block. #######################################
-include $(shell $(FRAMAC)-config -scripts)/epilogue.mk
+include $(shell $(FRAMAC)-config -print-lib-path)/analysis-scripts/epilogue.mk
 ###############################################################################
 
 # optional, for OSCS

basic-cwe-examples/.frama-c/cwe119-precise.eva/alarms.csv

 directory	file	line	function	property kind	status	property
-.	cwe119.c	62	host_lookup	precondition of strcpy	Unknown	room_string: \valid(dest + (0 .. strlen(src)))
-FRAMAC_SHARE/libc	string.h	352	strcpy	precondition	Unknown	room_string: \valid(dest + (0 .. strlen(src)))
+.	cwe119.c	28	my_strcmp	mem_access	Unknown	\valid_read(s1 + i)
+.	cwe119.c	28	my_strcmp	mem_access	Unknown	\valid_read(s2 + i)
+.	cwe119.c	65	host_lookup	precondition of strcpy	Invalid or unreachable	room_string: \valid(dest + (0 .. strlen(src)))
+FRAMAC_SHARE/libc	string.h	430	strcpy	precondition	Invalid or unreachable	room_string: \valid(dest + (0 .. strlen(src)))

basic-cwe-examples/.frama-c/cwe119-precise.eva/metrics.log

 [metrics] Eva coverage statistics
 =======================
-Syntactically reachable functions = 6 (out of 6)
-Semantically reached functions = 6
+Syntactically reachable functions = 7 (out of 7)
+Semantically reached functions = 7
 Coverage estimation = 100.0%
 [metrics] Statements analyzed by Eva
 --------------------------
-47 stmts in analyzed functions, 45 stmts analyzed (95.7%)
-host_lookup: 7 stmts out of 7 (100.0%)
-my_gethostbyaddr: 5 stmts out of 5 (100.0%)
+54 stmts in analyzed functions, 48 stmts analyzed (88.9%)
 my_inet_addr: 10 stmts out of 10 (100.0%)
 my_strcmp: 12 stmts out of 12 (100.0%)
+nonzero_uint32_t: 9 stmts out of 9 (100.0%)
 validate_addr_form: 7 stmts out of 7 (100.0%)
-main: 4 stmts out of 6 (66.7%)
+host_lookup: 4 stmts out of 5 (80.0%)
+my_gethostbyaddr: 4 stmts out of 5 (80.0%)
+main: 2 stmts out of 6 (33.3%)

basic-cwe-examples/.frama-c/cwe119-precise.eva/nonterm.log

-cwe119.c:62:[nonterm] warning: non-terminating function call
-stack: host_lookup :: cwe119.c:69 <- main
-cwe119.c:70:[nonterm] warning: unreachable return
+cwe119.c:65:[nonterm:stmt] warning: non-terminating function call
+stack: host_lookup :: cwe119.c:70 <- main
+cwe119.c:73:[nonterm:unreachable] warning: unreachable return