Compare revisions

b119465b · b503aa14 · fef53ef7 · 6d7560d3 · 401b56fc · f1fc0193
--- a/.githooks/pre-commit
+++ b/.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
--- a/.gitignore
+++ b/.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
+.vscode/
-# them, due to their size and the redundancy w.r.t. Eva logs.
+.ivette
+# SARIF files are currently not versioned
 *.sarif
+*.reparse
--- a/.gitlab-ci.yml
+++ b/.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
+    - make -C $TARGET/.frama-c clean
-    - git diff --exit-code
+    - make $TARGET
-    - make sarif
+    # 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
--- a/2048/.frama-c/2048.eva/alarms.csv
+++ b/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)
--- a/2048/.frama-c/2048.eva/metrics.log
+++ b/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%)

--- a/2048/.frama-c/2048.parse/framac.ast
+++ b/2048/.frama-c/2048.parse/framac.ast
 /* Generated by Frama-C */
 #include "errno.h"
+#include "fcntl.h"
 #include "signal.h"
 #include "stdarg.h"
 #include "stddef.h"
@@ -11,12 +12,12 @@
 #include "termios.h"
 #include "time.h"
 #include "unistd.h"
-uint32_t score = (unsigned int)0;
+uint32_t score = (uint32_t)0;
-uint8_t scheme = (unsigned char)0;
+uint8_t scheme = (uint8_t)0;
-/*@ requires
+/*@ requires valid_read_string(format);
+    requires
      \valid(s + (0 .. n - 1)) ∨
      \valid(s + (0 .. format_length(format) - 1));
-    requires valid_read_string(format);
    assigns \result, *(s + (0 ..));
    assigns \result
      \from (indirect: n), (indirect: *(format + (0 ..))),
@@ -24,110 +25,110 @@ uint8_t scheme = (unsigned char)0;
    assigns *(s + (0 ..))
      \from (indirect: n), (indirect: *(format + (0 ..))), param1, param0;
 */
-int snprintf_va_1(char * __restrict s, size_t n,
+int snprintf_va_1(char * restrict s, size_t n, char const * restrict format,
-                  char const * __restrict format, int param0, int param1);
+                  int param0, int param1);
 void getColor(uint8_t value, char *color, size_t length)
 {
  uint8_t original[32] =
-    {(unsigned char)8,
+    {(uint8_t)8,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)2,
+     (uint8_t)2,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)3,
+     (uint8_t)3,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)4,
+     (uint8_t)4,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)5,
+     (uint8_t)5,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)6,
+     (uint8_t)6,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)7,
+     (uint8_t)7,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)9,
+     (uint8_t)9,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)10,
+     (uint8_t)10,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)11,
+     (uint8_t)11,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)12,
+     (uint8_t)12,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)13,
+     (uint8_t)13,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)14,
+     (uint8_t)14,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)0};
+     (uint8_t)0};
  uint8_t blackwhite[32] =
-    {(unsigned char)232,
+    {(uint8_t)232,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)234,
+     (uint8_t)234,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)236,
+     (uint8_t)236,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)238,
+     (uint8_t)238,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)240,
+     (uint8_t)240,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)242,
+     (uint8_t)242,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)244,
+     (uint8_t)244,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)246,
+     (uint8_t)246,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)248,
+     (uint8_t)248,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)249,
+     (uint8_t)249,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)250,
+     (uint8_t)250,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)251,
+     (uint8_t)251,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)252,
+     (uint8_t)252,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)253,
+     (uint8_t)253,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)254,
+     (uint8_t)254,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)0};
+     (uint8_t)0};
  uint8_t bluered[32] =
-    {(unsigned char)235,
+    {(uint8_t)235,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)63,
+     (uint8_t)63,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)57,
+     (uint8_t)57,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)93,
+     (uint8_t)93,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)129,
+     (uint8_t)129,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)165,
+     (uint8_t)165,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)201,
+     (uint8_t)201,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)200,
+     (uint8_t)200,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)199,
+     (uint8_t)199,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)198,
+     (uint8_t)198,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)197,
+     (uint8_t)197,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)196,
+     (uint8_t)196,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)196,
+     (uint8_t)196,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)196,
+     (uint8_t)196,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)196,
+     (uint8_t)196,
-     (unsigned char)255,
+     (uint8_t)255,
-     (unsigned char)196,
+     (uint8_t)196,
-     (unsigned char)255};
+     (uint8_t)255};
  uint8_t *schemes[3] = {original, blackwhite, bluered};
  uint8_t *background = schemes[scheme] + 0;
  uint8_t *foreground = schemes[scheme] + 1;
@@ -135,7 +136,7 @@ void getColor(uint8_t value, char *color, size_t length)
    while (1) {
      uint8_t tmp;
      tmp = value;
-      value = (unsigned char)((int)value - 1);
+      value = (uint8_t)((int)value - 1);
      ;
      if (! tmp) break;
      if (background + 2 < schemes[scheme] + sizeof(original)) {
@@ -158,7 +159,7 @@ void getColor(uint8_t value, char *color, size_t length)
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_1(char const * __restrict format);
+int printf_va_1(char const * restrict format);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -171,10 +172,10 @@ int printf_va_1(char const * __restrict format);
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
-int printf_va_2(char const * __restrict format, int param0);
+int printf_va_2(char const * restrict format, int param0);
-/*@ requires valid_read_string(format);
+/*@ requires valid_read_string(param0);
-    requires valid_read_string(param0);
+    requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
@@ -185,7 +186,7 @@ int printf_va_2(char const * __restrict format, int param0);
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            *(param0 + (0 ..));
 */
-int printf_va_3(char const * __restrict format, char *param0);
+int printf_va_3(char const * restrict format, char *param0);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -197,10 +198,10 @@ int printf_va_3(char const * __restrict format, char *param0);
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_4(char const * __restrict format);
+int printf_va_4(char const * restrict format);
-/*@ requires valid_read_string(format);
+/*@ requires valid_read_string(param0);
-    requires valid_read_string(param0);
+    requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
@@ -211,7 +212,7 @@ int printf_va_4(char const * __restrict format);
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            *(param0 + (0 ..));
 */
-int printf_va_5(char const * __restrict format, char *param0);
+int printf_va_5(char const * restrict format, char *param0);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -223,10 +224,10 @@ int printf_va_5(char const * __restrict format, char *param0);
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_6(char const * __restrict format);
+int printf_va_6(char const * restrict format);
-/*@ requires valid_read_string(format);
+/*@ requires valid_read_string(param0);
-    requires valid_read_string(param0);
+    requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
@@ -237,25 +238,25 @@ int printf_va_6(char const * __restrict format);
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            *(param0 + (0 ..));
 */
-int printf_va_7(char const * __restrict format, char *param0);
+int printf_va_7(char const * restrict format, char *param0);
-/*@ requires
+/*@ requires valid_read_string(format);
+    requires
      \valid(s + (0 .. n - 1)) ∨
      \valid(s + (0 .. format_length(format) - 1));
-    requires valid_read_string(format);
    assigns \result, *(s + (0 ..));
    assigns \result
      \from (indirect: n), (indirect: *(format + (0 ..))), (indirect: param0);
    assigns *(s + (0 ..))
      \from (indirect: n), (indirect: *(format + (0 ..))), param0;
 */
-int snprintf_va_2(char * __restrict s, size_t n,
+int snprintf_va_2(char * restrict s, size_t n, char const * restrict format,
-                  char const * __restrict format, unsigned int param0);
+                  unsigned int param0);
-/*@ requires valid_read_string(format);
+/*@ requires valid_read_string(param1);
-    requires valid_read_string(param4);
    requires valid_read_string(param2);
-    requires valid_read_string(param1);
+    requires valid_read_string(param4);
+    requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
@@ -269,7 +270,7 @@ int snprintf_va_2(char * __restrict s, size_t n,
            *(param4 + (0 ..)), param3, *(param2 + (0 ..)),
            *(param1 + (0 ..)), param0;
 */
-int printf_va_8(char const * __restrict format, int param0, char *param1,
+int printf_va_8(char const * restrict format, int param0, char *param1,
                char *param2, int param3, char *param4);
 /*@ requires valid_read_string(format);
@@ -282,10 +283,10 @@ int printf_va_8(char const * __restrict format, int param0, char *param1,
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_9(char const * __restrict format);
+int printf_va_9(char const * restrict format);
-/*@ requires valid_read_string(format);
+/*@ requires valid_read_string(param0);
-    requires valid_read_string(param0);
+    requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
@@ -296,7 +297,7 @@ int printf_va_9(char const * __restrict format);
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            *(param0 + (0 ..));
 */
-int printf_va_10(char const * __restrict format, char *param0);
+int printf_va_10(char const * restrict format, char *param0);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -308,10 +309,10 @@ int printf_va_10(char const * __restrict format, char *param0);
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_11(char const * __restrict format);
+int printf_va_11(char const * restrict format);
-/*@ requires valid_read_string(format);
+/*@ requires valid_read_string(param0);
-    requires valid_read_string(param0);
+    requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
@@ -322,7 +323,7 @@ int printf_va_11(char const * __restrict format);
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            *(param0 + (0 ..));
 */
-int printf_va_12(char const * __restrict format, char *param0);
+int printf_va_12(char const * restrict format, char *param0);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -334,10 +335,10 @@ int printf_va_12(char const * __restrict format, char *param0);
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_13(char const * __restrict format);
+int printf_va_13(char const * restrict format);
-/*@ requires valid_read_string(format);
+/*@ requires valid_read_string(param0);
-    requires valid_read_string(param0);
+    requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
@@ -348,7 +349,7 @@ int printf_va_13(char const * __restrict format);
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            *(param0 + (0 ..));
 */
-int printf_va_14(char const * __restrict format, char *param0);
+int printf_va_14(char const * restrict format, char *param0);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -360,7 +361,7 @@ int printf_va_14(char const * __restrict format, char *param0);
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_15(char const * __restrict format);
+int printf_va_15(char const * restrict format);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -372,7 +373,7 @@ int printf_va_15(char const * __restrict format);
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_16(char const * __restrict format);
+int printf_va_16(char const * restrict format);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -384,7 +385,7 @@ int printf_va_16(char const * __restrict format);
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_17(char const * __restrict format);
+int printf_va_17(char const * restrict format);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -396,9 +397,9 @@ int printf_va_17(char const * __restrict format);
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_18(char const * __restrict format);
+int printf_va_18(char const * restrict format);
-void drawBoard(uint8_t (* /*[4]*/ board)[4])
+void drawBoard(uint8_t board[4][4])
 {
  uint8_t x;
  uint8_t y;
@@ -407,46 +408,45 @@ void drawBoard(uint8_t (* /*[4]*/ board)[4])
  char reset[4] = {(char)'\033', (char)'[', (char)'m', (char)'\000'};
  printf("\033[H"); /* printf_va_1 */
  printf("2048.c %17d pts\n\n",(int)score); /* printf_va_2 */
-  y = (unsigned char)0;
+  y = (uint8_t)0;
  while ((int)y < 4) {
-    x = (unsigned char)0;
+    x = (uint8_t)0;
    while ((int)x < 4) {
-      getColor((*(board + x))[y],color,(unsigned int)40);
+      getColor((*(board + x))[y],color,(size_t)40);
      printf("%s",color); /* printf_va_3 */
      printf("       "); /* printf_va_4 */
      printf("%s",reset); /* printf_va_5 */
-      x = (unsigned char)((int)x + 1);
+      x = (uint8_t)((int)x + 1);
    }
    printf("\n"); /* printf_va_6 */
-    x = (unsigned char)0;
+    x = (uint8_t)0;
    while ((int)x < 4) {
-      getColor((*(board + x))[y],color,(unsigned int)40);
+      getColor((*(board + x))[y],color,(size_t)40);
      printf("%s",color); /* printf_va_7 */
      if ((int)(*(board + x))[y] != 0) {
        char s[8];
        size_t tmp;
-        snprintf(s,(unsigned int)8,"%u",
+        snprintf(s,(size_t)8,"%u",(uint32_t)1 << (int)(*(board + x))[y]); /* snprintf_va_2 */
-                 (unsigned int)1 << (int)(*(board + x))[y]); /* snprintf_va_2 */
        tmp = strlen((char const *)(s));
-        uint8_t t = (unsigned char)((size_t)7 - tmp);
+        uint8_t t = (uint8_t)((size_t)7 - tmp);
        printf("%*s%s%*s",(int)t - (int)t / 2,(char *)"",s,(int)t / 2,
               (char *)""); /* printf_va_8 */
      }
      else printf("   \302\267   "); /* printf_va_9 */
      printf("%s",reset); /* printf_va_10 */
-      x = (unsigned char)((int)x + 1);
+      x = (uint8_t)((int)x + 1);
    }
    printf("\n"); /* printf_va_11 */
-    x = (unsigned char)0;
+    x = (uint8_t)0;
    while ((int)x < 4) {
-      getColor((*(board + x))[y],color,(unsigned int)40);
+      getColor((*(board + x))[y],color,(size_t)40);
      printf("%s",color); /* printf_va_12 */
      printf("       "); /* printf_va_13 */
      printf("%s",reset); /* printf_va_14 */
-      x = (unsigned char)((int)x + 1);
+      x = (uint8_t)((int)x + 1);
    }
    printf("\n"); /* printf_va_15 */
-    y = (unsigned char)((int)y + 1);
+    y = (uint8_t)((int)y + 1);
  }
  printf("\n"); /* printf_va_16 */
  printf("        \342\206\220,\342\206\221,\342\206\222,\342\206\223 or q        \n"); /* printf_va_17 */
@@ -454,7 +454,7 @@ void drawBoard(uint8_t (* /*[4]*/ board)[4])
  return;
 }
-uint8_t findTarget(uint8_t * /*[4]*/ array, uint8_t x, uint8_t stop)
+uint8_t findTarget(uint8_t array[4], uint8_t x, uint8_t stop)
 {
  uint8_t __retres;
  uint8_t t;
@@ -462,11 +462,11 @@ uint8_t findTarget(uint8_t * /*[4]*/ array, uint8_t x, uint8_t stop)
    __retres = x;
    goto return_label;
  }
-  t = (unsigned char)((int)x - 1);
+  t = (uint8_t)((int)x - 1);
  while ((int)t >= 0) {
    if ((int)*(array + t) != 0) {
      if ((int)*(array + t) != (int)*(array + x)) {
-        __retres = (unsigned char)((int)t + 1);
+        __retres = (uint8_t)((int)t + 1);
        goto return_label;
      }
      __retres = t;
@@ -477,19 +477,19 @@ uint8_t findTarget(uint8_t * /*[4]*/ array, uint8_t x, uint8_t stop)
        __retres = t;
        goto return_label;
      }
-    t = (unsigned char)((int)t - 1);
+    t = (uint8_t)((int)t - 1);
  }
  __retres = x;
  return_label: return __retres;
 }
-_Bool slideArray(uint8_t * /*[4]*/ array)
+_Bool slideArray(uint8_t array[4])
 {
  uint8_t x;
  uint8_t t;
  _Bool success = (_Bool)0;
-  uint8_t stop = (unsigned char)0;
+  uint8_t stop = (uint8_t)0;
-  x = (unsigned char)0;
+  x = (uint8_t)0;
  while ((int)x < 4) {
    if ((int)*(array + x) != 0) {
      t = findTarget(array,x,stop);
@@ -497,26 +497,26 @@ _Bool slideArray(uint8_t * /*[4]*/ array)
        if ((int)*(array + t) == 0) *(array + t) = *(array + x);
        else 
          if ((int)*(array + t) == (int)*(array + x)) {
-            *(array + t) = (unsigned char)((int)*(array + t) + 1);
+            *(array + t) = (uint8_t)((int)*(array + t) + 1);
-            score += (unsigned int)1 << (int)*(array + t);
+            score += (uint32_t)1 << (int)*(array + t);
-            stop = (unsigned char)((int)t + 1);
+            stop = (uint8_t)((int)t + 1);
          }
-        *(array + x) = (unsigned char)0;
+        *(array + x) = (uint8_t)0;
        success = (_Bool)1;
      }
    }
-    x = (unsigned char)((int)x + 1);
+    x = (uint8_t)((int)x + 1);
  }
  return success;
 }
-void rotateBoard(uint8_t (* /*[4]*/ board)[4])
+void rotateBoard(uint8_t board[4][4])
 {
  uint8_t i;
  uint8_t j;
  uint8_t tmp;
-  uint8_t n = (unsigned char)4;
+  uint8_t n = (uint8_t)4;
-  i = (unsigned char)0;
+  i = (uint8_t)0;
  while ((int)i < (int)n / 2) {
    j = i;
    while ((int)j < ((int)n - (int)i) - 1) {
@@ -527,30 +527,30 @@ void rotateBoard(uint8_t (* /*[4]*/ board)[4])
      (*(board + (((int)n - (int)i) - 1)))[((int)n - (int)j) - 1] = (*(
      board + (((int)n - (int)j) - 1)))[i];
      (*(board + (((int)n - (int)j) - 1)))[i] = tmp;
-      j = (unsigned char)((int)j + 1);
+      j = (uint8_t)((int)j + 1);
    }
-    i = (unsigned char)((int)i + 1);
+    i = (uint8_t)((int)i + 1);
  }
  return;
 }
-_Bool moveUp(uint8_t (* /*[4]*/ board)[4])
+_Bool moveUp(uint8_t board[4][4])
 {
  uint8_t x;
  _Bool success = (_Bool)0;
-  x = (unsigned char)0;
+  x = (uint8_t)0;
  while ((int)x < 4) {
    {
      _Bool tmp;
      tmp = slideArray(*(board + x));
      success = (_Bool)(((int)success | (int)tmp) != 0);
    }
-    x = (unsigned char)((int)x + 1);
+    x = (uint8_t)((int)x + 1);
  }
  return success;
 }
-_Bool moveLeft(uint8_t (* /*[4]*/ board)[4])
+_Bool moveLeft(uint8_t board[4][4])
 {
  _Bool success;
  rotateBoard(board);
@@ -561,7 +561,7 @@ _Bool moveLeft(uint8_t (* /*[4]*/ board)[4])
  return success;
 }
-_Bool moveDown(uint8_t (* /*[4]*/ board)[4])
+_Bool moveDown(uint8_t board[4][4])
 {
  _Bool success;
  rotateBoard(board);
@@ -572,7 +572,7 @@ _Bool moveDown(uint8_t (* /*[4]*/ board)[4])
  return success;
 }
-_Bool moveRight(uint8_t (* /*[4]*/ board)[4])
+_Bool moveRight(uint8_t board[4][4])
 {
  _Bool success;
  rotateBoard(board);
@@ -583,46 +583,46 @@ _Bool moveRight(uint8_t (* /*[4]*/ board)[4])
  return success;
 }
-_Bool findPairDown(uint8_t (* /*[4]*/ board)[4])
+_Bool findPairDown(uint8_t board[4][4])
 {
  _Bool __retres;
  uint8_t x;
  uint8_t y;
  _Bool success = (_Bool)0;
-  x = (unsigned char)0;
+  x = (uint8_t)0;
  while ((int)x < 4) {
-    y = (unsigned char)0;
+    y = (uint8_t)0;
    while ((int)y < 4 - 1) {
      if ((int)(*(board + x))[y] == (int)(*(board + x))[(int)y + 1]) {
        __retres = (_Bool)1;
        goto return_label;
      }
-      y = (unsigned char)((int)y + 1);
+      y = (uint8_t)((int)y + 1);
    }
-    x = (unsigned char)((int)x + 1);
+    x = (uint8_t)((int)x + 1);
  }
  __retres = success;
  return_label: return __retres;
 }
-uint8_t countEmpty(uint8_t (* /*[4]*/ board)[4])
+uint8_t countEmpty(uint8_t board[4][4])
 {
  uint8_t x;
  uint8_t y;
-  uint8_t count = (unsigned char)0;
+  uint8_t count = (uint8_t)0;
-  x = (unsigned char)0;
+  x = (uint8_t)0;
  while ((int)x < 4) {
-    y = (unsigned char)0;
+    y = (uint8_t)0;
    while ((int)y < 4) {
-      if ((int)(*(board + x))[y] == 0) count = (unsigned char)((int)count + 1);
+      if ((int)(*(board + x))[y] == 0) count = (uint8_t)((int)count + 1);
-      y = (unsigned char)((int)y + 1);
+      y = (uint8_t)((int)y + 1);
    }
-    x = (unsigned char)((int)x + 1);
+    x = (uint8_t)((int)x + 1);
  }
  return count;
 }
-_Bool gameEnded(uint8_t (* /*[4]*/ board)[4])
+_Bool gameEnded(uint8_t board[4][4])
 {
  _Bool __retres;
  uint8_t tmp;
@@ -649,71 +649,71 @@ _Bool gameEnded(uint8_t (* /*[4]*/ board)[4])
  return_label: return __retres;
 }
-void addRandom(uint8_t (* /*[4]*/ board)[4]);
+void addRandom(uint8_t board[4][4]);
 static _Bool addRandom_initialized = (_Bool)0;
-void addRandom(uint8_t (* /*[4]*/ board)[4])
+void addRandom(uint8_t board[4][4])
 {
  uint8_t x;
  uint8_t y;
  uint8_t r;
  uint8_t n;
  uint8_t list[4 * 4][2];
-  uint8_t len = (unsigned char)0;
+  uint8_t len = (uint8_t)0;
  if (! addRandom_initialized) {
    time_t tmp;
    tmp = time((time_t *)0);
    srand((unsigned int)tmp);
    addRandom_initialized = (_Bool)1;
  }
-  x = (unsigned char)0;
+  x = (uint8_t)0;
-  /*@ loop unroll 4; */
+  /*@ loop \eva::unroll 4; */
  while ((int)x < 4) {
-    y = (unsigned char)0;
+    y = (uint8_t)0;
-    /*@ loop unroll 4; */
+    /*@ loop \eva::unroll 4; */
    while ((int)y < 4) {
      if ((int)(*(board + x))[y] == 0) {
        list[len][0] = x;
        list[len][1] = y;
-        len = (unsigned char)((int)len + 1);
+        len = (uint8_t)((int)len + 1);
      }
-      y = (unsigned char)((int)y + 1);
+      y = (uint8_t)((int)y + 1);
    }
-    x = (unsigned char)((int)x + 1);
+    x = (uint8_t)((int)x + 1);
  }
  if ((int)len > 0) {
    int tmp_0;
    int tmp_1;
    tmp_0 = rand();
-    r = (unsigned char)(tmp_0 % (int)len);
+    r = (uint8_t)(tmp_0 % (int)len);
    x = list[r][0];
    y = list[r][1];
    tmp_1 = rand();
-    n = (unsigned char)((tmp_1 % 10) / 9 + 1);
+    n = (uint8_t)((tmp_1 % 10) / 9 + 1);
    (*(board + x))[y] = n;
  }
  return;
 }
-void initBoard(uint8_t (* /*[4]*/ board)[4])
+void initBoard(uint8_t board[4][4])
 {
  uint8_t x;
  uint8_t y;
-  x = (unsigned char)0;
+  x = (uint8_t)0;
-  /*@ loop unroll 4; */
+  /*@ loop \eva::unroll 4; */
  while ((int)x < 4) {
-    y = (unsigned char)0;
+    y = (uint8_t)0;
-    /*@ loop unroll 4; */
+    /*@ loop \eva::unroll 4; */
    while ((int)y < 4) {
-      (*(board + x))[y] = (unsigned char)0;
+      (*(board + x))[y] = (uint8_t)0;
-      y = (unsigned char)((int)y + 1);
+      y = (uint8_t)((int)y + 1);
    }
-    x = (unsigned char)((int)x + 1);
+    x = (uint8_t)((int)x + 1);
  }
  addRandom(board);
  addRandom(board);
  drawBoard(board);
-  score = (unsigned int)0;
+  score = (uint32_t)0;
  return;
 }
@@ -755,7 +755,7 @@ void setBufferedInput(_Bool enable)
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
-int printf_va_19(char const * __restrict format, int param0);
+int printf_va_19(char const * restrict format, int param0);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -767,7 +767,7 @@ int printf_va_19(char const * __restrict format, int param0);
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_20(char const * __restrict format);
+int printf_va_20(char const * restrict format);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -780,7 +780,7 @@ int printf_va_20(char const * __restrict format);
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
-int printf_va_21(char const * __restrict format, int param0);
+int printf_va_21(char const * restrict format, int param0);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -792,7 +792,7 @@ int printf_va_21(char const * __restrict format, int param0);
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_22(char const * __restrict format);
+int printf_va_22(char const * restrict format);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -805,7 +805,7 @@ int printf_va_22(char const * __restrict format);
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
-int printf_va_23(char const * __restrict format, int param0);
+int printf_va_23(char const * restrict format, int param0);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -817,7 +817,7 @@ int printf_va_23(char const * __restrict format, int param0);
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_24(char const * __restrict format);
+int printf_va_24(char const * restrict format);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -830,7 +830,7 @@ int printf_va_24(char const * __restrict format);
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
-int printf_va_25(char const * __restrict format, int param0);
+int printf_va_25(char const * restrict format, int param0);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -842,7 +842,7 @@ int printf_va_25(char const * __restrict format, int param0);
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_26(char const * __restrict format);
+int printf_va_26(char const * restrict format);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -855,7 +855,7 @@ int printf_va_26(char const * __restrict format);
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
-int printf_va_27(char const * __restrict format, int param0);
+int printf_va_27(char const * restrict format, int param0);
 int test(void)
 {
@@ -867,157 +867,156 @@ int test(void)
  uint8_t tests;
  uint8_t i;
  uint8_t data[104] =
-    {(unsigned char)0,
+    {(uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)2,
+     (uint8_t)2,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)2,
+     (uint8_t)2,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)2,
+     (uint8_t)2,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)2,
+     (uint8_t)2,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)2,
+     (uint8_t)2,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)2,
+     (uint8_t)2,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)2,
+     (uint8_t)2,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)2,
+     (uint8_t)2,
-     (unsigned char)2,
+     (uint8_t)2,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)2,
+     (uint8_t)2,
-     (unsigned char)2,
+     (uint8_t)2,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)3,
+     (uint8_t)3,
-     (unsigned char)2,
+     (uint8_t)2,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)2,
+     (uint8_t)2,
-     (unsigned char)2,
+     (uint8_t)2,
-     (unsigned char)2,
+     (uint8_t)2,
-     (unsigned char)3,
+     (uint8_t)3,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)3,
+     (uint8_t)3,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)3,
+     (uint8_t)3,
-     (unsigned char)2,
+     (uint8_t)2,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)2,
+     (uint8_t)2,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)1,
+     (uint8_t)1,
-     (unsigned char)2,
+     (uint8_t)2,
-     (unsigned char)2,
+     (uint8_t)2,
-     (unsigned char)0,
+     (uint8_t)0,
-     (unsigned char)0};
+     (uint8_t)0};
  _Bool success = (_Bool)1;
-  tests = (unsigned char)((sizeof(data) / sizeof(data[0])) / (unsigned int)(
+  tests = (uint8_t)((sizeof(data) / sizeof(data[0])) / (unsigned int)(2 * 4));
-                          2 * 4));
+  t = (uint8_t)0;
-  t = (unsigned char)0;
  while ((int)t < (int)tests) {
    in = & data[((int)t * 2) * 4];
    out = in + 4;
-    i = (unsigned char)0;
+    i = (uint8_t)0;
    while ((int)i < 4) {
      array[i] = *(in + i);
-      i = (unsigned char)((int)i + 1);
+      i = (uint8_t)((int)i + 1);
    }
    slideArray(array);
-    i = (unsigned char)0;
+    i = (uint8_t)0;
-    /*@ loop unroll 4; */
+    /*@ loop \eva::unroll 4; */
    while ((int)i < 4) {
      if ((int)array[i] != (int)*(out + i)) success = (_Bool)0;
-      i = (unsigned char)((int)i + 1);
+      i = (uint8_t)((int)i + 1);
    }
    if ((int)success == 0) {
-      i = (unsigned char)0;
+      i = (uint8_t)0;
      while ((int)i < 4) {
        printf("%d ",(int)*(in + i)); /* printf_va_19 */
-        i = (unsigned char)((int)i + 1);
+        i = (uint8_t)((int)i + 1);
      }
      printf("=> "); /* printf_va_20 */
-      i = (unsigned char)0;
+      i = (uint8_t)0;
      while ((int)i < 4) {
        printf("%d ",(int)array[i]); /* printf_va_21 */
-        i = (unsigned char)((int)i + 1);
+        i = (uint8_t)((int)i + 1);
      }
      printf("expected "); /* printf_va_22 */
-      i = (unsigned char)0;
+      i = (uint8_t)0;
      while ((int)i < 4) {
        printf("%d ",(int)*(in + i)); /* printf_va_23 */
-        i = (unsigned char)((int)i + 1);
+        i = (uint8_t)((int)i + 1);
      }
      printf("=> "); /* printf_va_24 */
-      i = (unsigned char)0;
+      i = (uint8_t)0;
      while ((int)i < 4) {
        printf("%d ",(int)*(out + i)); /* printf_va_25 */
-        i = (unsigned char)((int)i + 1);
+        i = (uint8_t)((int)i + 1);
      }
      printf("\n"); /* printf_va_26 */
      break;
    }
-    t = (unsigned char)((int)t + 1);
+    t = (uint8_t)((int)t + 1);
  }
  if (success) printf("All %hhu tests executed successfully\n",(int)tests); /* printf_va_27 */
  __retres = ! success;
@@ -1034,7 +1033,7 @@ int test(void)
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_28(char const * __restrict format);
+int printf_va_28(char const * restrict format);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1046,7 +1045,7 @@ int printf_va_28(char const * __restrict format);
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_29(char const * __restrict format);
+int printf_va_29(char const * restrict format);
 void signal_callback_handler(int signum)
 {
@@ -1067,7 +1066,7 @@ void signal_callback_handler(int signum)
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_30(char const * __restrict format);
+int printf_va_30(char const * restrict format);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1079,7 +1078,7 @@ int printf_va_30(char const * __restrict format);
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_31(char const * __restrict format);
+int printf_va_31(char const * restrict format);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1091,7 +1090,7 @@ int printf_va_31(char const * __restrict format);
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_32(char const * __restrict format);
+int printf_va_32(char const * restrict format);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1103,7 +1102,7 @@ int printf_va_32(char const * __restrict format);
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_33(char const * __restrict format);
+int printf_va_33(char const * restrict format);
 /*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1115,7 +1114,7 @@ int printf_va_33(char const * __restrict format);
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
-int printf_va_34(char const * __restrict format);
+int printf_va_34(char const * restrict format);
 int main(int argc, char **argv)
 {
@@ -1128,50 +1127,48 @@ int main(int argc, char **argv)
  initBoard(board);
  setBufferedInput((_Bool)0);
  while (1) {
-    {
+    int tmp;
-      int tmp;
+    tmp = getchar();
-      tmp = getchar();
+    c = (char)tmp;
-      c = (char)tmp;
+    switch ((int)c) {
-      switch ((int)c) {
+      case 97: case 104: case 68: success = moveLeft(board);
-        case 97: case 104: case 68: success = moveLeft(board);
+      break;
-        break;
+      case 100: case 108: case 67: success = moveRight(board);
-        case 100: case 108: case 67: success = moveRight(board);
+      break;
-        break;
+      case 119: case 107: case 65: success = moveUp(board);
-        case 119: case 107: case 65: success = moveUp(board);
+      break;
-        break;
+      case 115: case 106: case 66: success = moveDown(board);
-        case 115: case 106: case 66: success = moveDown(board);
+      break;
+      default: success = (_Bool)0;
+    }
+    if (success) {
+      _Bool tmp_0;
+      drawBoard(board);
+      usleep((useconds_t)150000);
+      addRandom(board);
+      drawBoard(board);
+      tmp_0 = gameEnded(board);
+      if (tmp_0) {
+        printf("         GAME OVER          \n"); /* printf_va_31 */
        break;
-        default: success = (_Bool)0;
-      }
-      if (success) {
-        _Bool tmp_0;
-        drawBoard(board);
-        usleep((unsigned int)150000);
-        addRandom(board);
-        drawBoard(board);
-        tmp_0 = gameEnded(board);
-        if (tmp_0) {
-          printf("         GAME OVER          \n"); /* printf_va_31 */
-          break;
-        }
-      }
-      if ((int)c == 'q') {
-        int tmp_1;
-        printf("        QUIT? (y/n)         \n"); /* printf_va_32 */
-        tmp_1 = getchar();
-        c = (char)tmp_1;
-        if ((int)c == 'y') break;
-        drawBoard(board);
-      }
-      if ((int)c == 'r') {
-        int tmp_2;
-        printf("       RESTART? (y/n)       \n"); /* printf_va_33 */
-        tmp_2 = getchar();
-        c = (char)tmp_2;
-        if ((int)c == 'y') initBoard(board);
-        drawBoard(board);
      }
    }
+    if ((int)c == 'q') {
+      int tmp_1;
+      printf("        QUIT? (y/n)         \n"); /* printf_va_32 */
+      tmp_1 = getchar();
+      c = (char)tmp_1;
+      if ((int)c == 'y') break;
+      drawBoard(board);
+    }
+    if ((int)c == 'r') {
+      int tmp_2;
+      printf("       RESTART? (y/n)       \n"); /* printf_va_33 */
+      tmp_2 = getchar();
+      c = (char)tmp_2;
+      if ((int)c == 'y') initBoard(board);
+      drawBoard(board);
+    }
  }
  setBufferedInput((_Bool)1);
  printf("\033[?25h\033[m"); /* printf_va_34 */

--- a/2048/.frama-c/2048.parse/metrics.log
+++ b/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

--- a/2048/.frama-c/2048.parse/warnings.log
+++ b/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.
--- a/2048/.frama-c/GNUmakefile
+++ b/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

--- a/2048/.gitignore
+++ b/2048/.gitignore
+2048
--- a/2048/Makefile
+++ b/2048/Makefile
+../Makefile.single-target
\ No newline at end of file
--- a/2048/OSCS-README.txt
+++ b/2048/OSCS-README.txt
+Console version of the game 2048
+https://github.com/mevdschee/2048.c
+NO_DYN_ALLOC, NO_RECURSION, NO_FLOAT
--- a/Makefile
+++ b/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
-	{
+	echo "*** cleaning previous builds..."
-	  cd frama-c
+	$(MAKE) -C frama-c clean >/dev/null
-	  echo "*** running autoconf..."
+	echo "*** running make..."
-	  autoconf -f >/dev/null 2>/dev/null
+	$(MAKE) -C frama-c -j --quiet >/dev/null
-	  echo "*** running configure..."
+	echo "*** running make install..."
-	  ./configure --prefix=`pwd`/build --quiet >/dev/null
+	$(MAKE) -C frama-c install PREFIX=$(ROOT_DIR)/frama-c/build >/dev/null
-	  $(MAKE) clean >/dev/null
-	  echo "*** running make..."
-	  $(MAKE) -j --quiet >/dev/null
-	  echo "*** running make install..."
-	  $(MAKE) install >/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
+# Targets sorted by "longest-running first"
-QUICK_TARGETS=$(filter-out polarssl gzip124 libmodbus monocypher chrony,$(TARGETS))
+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
+.FORCE:
-# git diff to check for unexpected differences
-ci-tests: all stats-all
-	git status --porcelain
-	git diff --exit-code
-ci-tests: export FCFLAGS=-value-verbose 0 -kernel-verbose 0
+.PHONY: $(TARGETS) frama-c/build/bin/frama-c help
--- a/Makefile.common
+++ b/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)
--- a/Makefile.single-target
+++ b/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
--- a/README.md
+++ b/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
+- The result of the analysis is stored inside `.frama-c`, in subdirectories
-  and Frama-C save files; successive runs are copied into timestamped
+  `t.parse` for parsing and `t.eva` for the Eva analysis.
-  directories, to allow comparing them (e.g. via `meld`);
+  Each subdirectory contains a few log files.
 - To try other parametrizations, simply edit variables
-  `CPPFLAGS/FCFLAGS/EVAFLAGS` in `GNUmakefile` and re-run `make`.
+  `CPPFLAGS/FCFLAGS/EVAFLAGS` in `.frama-c/GNUmakefile` and re-run `fcmake`.
- 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`).
 # 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:
+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:
- File `GNUmakefile` is added to each case study, with Frama-C/Eva-specific
-  rules for parsing and running the analysis;
+- A `.frama-c` directory is added, with a `GNUmakefile` which defines the
- When necessary, syntactic modifications were performed to ensure better
+  Frama-C targets and parameters;
-  C99-compliance and/or the inclusion of stubs to allow Frama-C to parse the
+- Some stubs file (e.g. `stubs.c`) are added to the `.frama-c` directory,
-  files;
+  either to emulate an initial state with command-line arguments, or to provide
- In some cases, an `eva_main` function was added to provide a better initial
+  code/specifications for library functions, missing code, non-portable
-  context for the analysis;
+  features, etc.
- When recursive calls are present, the functions containing them need to be
+- When code modifications are needed (and cannot be moved to the stubs file,
-  replaced with specifications;
+  e.g. when adding a specification to a `static` functions), we often
- Some ACSL annotations were added to the sources
+  protect them by `#ifdef __FRAMAC__` guards, to ensure the code compiles
-  (to illustrate their usage, or to improve the analysis);
+  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"
+- `kilo`: BSD 2-clause "Simplified", see `LICENSE`
-          (see https://github.com/antirez/kilo/blob/master/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`)
+- `solitaire`: public domain, see `solitaire.c`
- `tweetnacl-usable`: public domain (see `LICENSE.txt`)
+- `stmr`: MIT
- `x509-parser` : GPLv2 / BSD (see `LICENSE`)
+- `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.
--- a/basic-cwe-examples/.frama-c/GNUmakefile
+++ b/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

--- a/basic-cwe-examples/.frama-c/cwe119-precise.eva/alarms.csv
+++ b/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)))
--- a/basic-cwe-examples/.frama-c/cwe119-precise.eva/nonterm.log
+++ b/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
--- a/basic-cwe-examples/.frama-c/cwe119-precise.parse/framac.ast
+++ b/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;
 }
No results found