.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

@@ -2,7 +2,6 @@
 *.sav
 *.o
 *~
-.frama-c
 config.status
 lia.cache
 
@@ -13,10 +12,17 @@ eva.log
 stats.txt
 flamegraph.txt
 
-# ignore timestamped versions
-*_20*-*.eva
-*_20*-*.parse
 *.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	58	drawBoard	precondition of printf_va_7	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	72	drawBoard	precondition of printf_va_12	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	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

+[metrics] Eva coverage statistics
+=======================
+Syntactically reachable functions = 17 (out of 18)
+Semantically reached functions = 16
+Coverage estimation = 94.1% 
+
+Unreached functions (1) =
+  <2048.c>: signal_callback_handler;
+[metrics] References to non-analyzed functions
+------------------------------------
+Function main references signal_callback_handler (at 2048.c:383)
+[metrics] Statements analyzed by Eva
+--------------------------
+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%)
+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: 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%)
+moveUp: 11 stmts out of 11 (100.0%)
+rotateBoard: 19 stmts out of 19 (100.0%)
+slideArray: 20 stmts out of 20 (100.0%)
+setBufferedInput: 12 stmts out of 13 (92.3%)
+findTarget: 22 stmts out of 24 (91.7%)

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

+[metrics] Defined functions (18)
+======================
+ addRandom (3 calls); countEmpty (1 call); drawBoard (5 calls);
+ findPairDown (2 calls); findTarget (1 call); gameEnded (1 call);
+ getColor (3 calls); initBoard (2 calls); main (0 call); moveDown (1 call);
+ moveLeft (1 call); moveRight (1 call); moveUp (4 calls);
+ rotateBoard (16 calls); setBufferedInput (3 calls);
+ signal_callback_handler (address taken) (0 call); slideArray (2 calls);
+ test (0 call); 
+
+Specified-only functions (0)
+============================
+ 
+
+Undefined and unspecified functions (0)
+=======================================
+ 
+
+'Extern' global variables (0)
+=============================
+ 
+
+Potential entry points (2)
+==========================
+ main; test; 
+
+Global metrics
+============== 
+Sloc = 398
+Decision point = 61
+Global variables = 5
+If = 57
+Loop = 26
+Goto = 8
+Assignment = 140
+Exit point = 18
+Function = 18
+Function call = 96
+Pointer dereferencing = 40
+Cyclomatic complexity = 79

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

+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

+# 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 -print-lib-path)/analysis-scripts/prologue.mk
+###############################################################################
+
+# Edit below as needed. 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 += \
+
+## 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 -print-lib-path)/analysis-scripts/epilogue.mk
+###############################################################################
+
+# optional, for OSCS
+-include ../../Makefile.common

2048/.frama-c/path.mk

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

2048/.gitignore

+2048

2048/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)

2048/2048.eva/metrics.log

-[metrics] Eva coverage statistics
-=======================
-Syntactically reachable functions = 17 (out of 18)
-Semantically reached functions = 16
-Coverage estimation = 94.1% 
-
-Unreached functions (1) =
-  <2048.c>: signal_callback_handler;
-[metrics] References to non-analyzed functions
-------------------------------------
-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%)
-addRandom: 32 stmts out of 32 (100.0%)
-countEmpty: 16 stmts out of 16 (100.0%)
-drawBoard: 51 stmts out of 51 (100.0%)
-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%)
-moveDown: 6 stmts out of 6 (100.0%)
-moveLeft: 6 stmts out of 6 (100.0%)
-moveRight: 6 stmts out of 6 (100.0%)
-moveUp: 11 stmts out of 11 (100.0%)
-rotateBoard: 19 stmts out of 19 (100.0%)
-slideArray: 20 stmts out of 20 (100.0%)
-setBufferedInput: 12 stmts out of 13 (92.3%)
-findTarget: 22 stmts out of 24 (91.7%)

2048/2048.parse/metrics.log

-[metrics] Defined functions (18)
-======================
- addRandom (3 calls); countEmpty (1 call); drawBoard (5 calls);
- findPairDown (2 calls); findTarget (1 call); gameEnded (1 call);
- getColor (3 calls); initBoard (2 calls); main (0 call); moveDown (1 call);
- moveLeft (1 call); moveRight (1 call); moveUp (4 calls);
- rotateBoard (16 calls); setBufferedInput (3 calls);
- signal_callback_handler (address taken) (0 call); slideArray (2 calls);
- test (0 call); 
-
-Undefined functions (0)
-=======================
- 
-
-'Extern' global variables (0)
-=============================
- 
-
-Potential entry points (2)
-==========================
- main; test; 
-
-Global metrics
-============== 
-Sloc = 399
-Decision point = 61
-Global variables = 5
-If = 57
-Loop = 26
-Goto = 8
-Assignment = 140
-Exit point = 18
-Function = 18
-Function call = 96
-Pointer dereferencing = 40
-Cyclomatic complexity = 79

2048/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/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/Makefile

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