.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

 # Common rules used by all subdirectories
 *.sav
-*.sav.crash
 *.o
 *~
 config.status
@@ -14,10 +13,16 @@ stats.txt
 flamegraph.txt
 
 *.error
+*.break
+*#
 
 benchs-value.csv
 bench_clone
 
-# .sarif reports are produced as CI artifacts, but we do not want to version
-# them, due to their size and the redundancy w.r.t. Eva logs.
+.vscode/
+
+.ivette
+
+# SARIF files are currently not versioned
 *.sarif
+*.reparse

.gitlab-ci.yml

 default:
   image: framac/frama-c:dev
 
-build:
+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 -B all >/dev/null
-    - git diff --exit-code
-    - make sarif
+    - 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:
-    - "*/.frama-c/*.sarif"
+    - "$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,7 +4,7 @@
 ### Prologue. Do not modify this block. #######################################
 -include path.mk
 FRAMAC ?= frama-c
-include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/prologue.mk
+include $(shell $(FRAMAC)-config -print-lib-path)/analysis-scripts/prologue.mk
 ###############################################################################
 
 # Edit below as needed. Suggested flags are optional.
@@ -36,7 +36,7 @@ TARGETS = 2048.eva
   ../2048.c \
 
 ### Epilogue. Do not modify this block. #######################################
-include $(shell $(FRAMAC)-config -print-share-path)/analysis-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,32 +42,31 @@ 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 \
@@ -67,17 +75,22 @@ TARGETS=\
   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::
@@ -85,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
@@ -108,11 +126,6 @@ clean: $(addsuffix .clean,$(TARGETS))
 
 parse: $(addsuffix .parse,$(TARGETS))
 
-%.stats:
-	$(MAKE) -C $*/.frama-c stats
-
-stats: $(addsuffix .stats,$(TARGETS))
-
 %.sarif:
 	$(MAKE) -C $*/.frama-c sarif
 
@@ -123,12 +136,33 @@ display-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

@@ -3,9 +3,9 @@
 # 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
+# '-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 $@
+	$(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

@@ -14,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
 
@@ -22,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;
@@ -51,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
 
@@ -100,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
@@ -123,32 +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`
 - `libyaml`: MIT, see `License`
-- `mibench`: several (see `LICENSE` file inside each subdirectory)
+- `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,7 +4,7 @@
 ### Prologue. Do not modify this block. #######################################
 -include path.mk
 FRAMAC ?= frama-c
-include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/prologue.mk
+include $(shell $(FRAMAC)-config -print-lib-path)/analysis-scripts/prologue.mk
 ###############################################################################
 
 # Edit below as needed. Suggested flags are optional.
@@ -25,11 +25,13 @@ EVAFLAGS    += \
   -eva-warn-key builtins:missing-spec=abort \
 
 ## Analysis targets (suffixed with .eva)
-IMPRECISE_TARGETS = cwe20.eva cwe20-2.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
@@ -37,6 +39,8 @@ 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
@@ -44,17 +48,26 @@ 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
 
+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 += -warn-unsigned-overflow
+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 -print-share-path)/analysis-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

@@ -2,4 +2,4 @@ directory	file	line	function	property kind	status	property
 .	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	352	strcpy	precondition	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/nonterm.log

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

basic-cwe-examples/.frama-c/cwe119-precise.parse/framac.ast

@@ -39,7 +39,7 @@ uint32_t nonzero_uint32_t(void)
       \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
             (indirect: *(format + (0 ..)));
  */
-int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
+int fprintf_va_1(FILE * restrict stream, char const * restrict format);
 
 static void validate_addr_form(char *v)
 {
@@ -59,13 +59,13 @@ static int my_strcmp(char const *s1, char const *s2)
 {
   int __retres;
   size_t i;
-  i = (unsigned long)0;
+  i = (size_t)0;
   while ((int)*(s1 + i) == (int)*(s2 + i)) {
     if ((int)*(s1 + i) == 0) {
       __retres = 0;
       goto return_label;
     }
-    i += (size_t)1;
+    i ++;
   }
   __retres = (int)*((unsigned char *)s1 + i) - (int)*((unsigned char *)s2 + i);
   return_label: return __retres;
@@ -77,7 +77,7 @@ static in_addr_t my_inet_addr(char const *cp)
   int tmp_0;
   tmp_0 = my_strcmp(cp,"127.0.0.1");
   if (tmp_0 == 0) {
-    __retres = (unsigned int)0;
+    __retres = (in_addr_t)0;
     goto return_label;
   }
   else {
@@ -108,7 +108,7 @@ void host_lookup(char *user_supplied_addr)
   validate_addr_form(user_supplied_addr);
   addr = my_inet_addr((char const *)user_supplied_addr);
   hp = my_gethostbyaddr((void const *)(& addr),
-                        (unsigned int)sizeof(struct in_addr),2);
+                        (socklen_t)sizeof(struct in_addr),2);
   strcpy(hostname,(char const *)hp->h_name);
   return;
 }