.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/framac.ast

+/* Generated by Frama-C */
+#include "errno.h"
+#include "fcntl.h"
+#include "signal.h"
+#include "stdarg.h"
+#include "stddef.h"
+#include "stdint.h"
+#include "stdio.h"
+#include "stdlib.h"
+#include "string.h"
+#include "strings.h"
+#include "termios.h"
+#include "time.h"
+#include "unistd.h"
+uint32_t score = (uint32_t)0;
+uint8_t scheme = (uint8_t)0;
+/*@ requires valid_read_string(format);
+    requires
+      \valid(s + (0 .. n - 1)) ∨
+      \valid(s + (0 .. format_length(format) - 1));
+    assigns \result, *(s + (0 ..));
+    assigns \result
+      \from (indirect: n), (indirect: *(format + (0 ..))),
+            (indirect: param1), (indirect: param0);
+    assigns *(s + (0 ..))
+      \from (indirect: n), (indirect: *(format + (0 ..))), param1, param0;
+ */
+int snprintf_va_1(char * restrict s, size_t n, char const * restrict format,
+                  int param0, int param1);
+
+void getColor(uint8_t value, char *color, size_t length)
+{
+  uint8_t original[32] =
+    {(uint8_t)8,
+     (uint8_t)255,
+     (uint8_t)1,
+     (uint8_t)255,
+     (uint8_t)2,
+     (uint8_t)255,
+     (uint8_t)3,
+     (uint8_t)255,
+     (uint8_t)4,
+     (uint8_t)255,
+     (uint8_t)5,
+     (uint8_t)255,
+     (uint8_t)6,
+     (uint8_t)255,
+     (uint8_t)7,
+     (uint8_t)255,
+     (uint8_t)9,
+     (uint8_t)0,
+     (uint8_t)10,
+     (uint8_t)0,
+     (uint8_t)11,
+     (uint8_t)0,
+     (uint8_t)12,
+     (uint8_t)0,
+     (uint8_t)13,
+     (uint8_t)0,
+     (uint8_t)14,
+     (uint8_t)0,
+     (uint8_t)255,
+     (uint8_t)0,
+     (uint8_t)255,
+     (uint8_t)0};
+  uint8_t blackwhite[32] =
+    {(uint8_t)232,
+     (uint8_t)255,
+     (uint8_t)234,
+     (uint8_t)255,
+     (uint8_t)236,
+     (uint8_t)255,
+     (uint8_t)238,
+     (uint8_t)255,
+     (uint8_t)240,
+     (uint8_t)255,
+     (uint8_t)242,
+     (uint8_t)255,
+     (uint8_t)244,
+     (uint8_t)255,
+     (uint8_t)246,
+     (uint8_t)0,
+     (uint8_t)248,
+     (uint8_t)0,
+     (uint8_t)249,
+     (uint8_t)0,
+     (uint8_t)250,
+     (uint8_t)0,
+     (uint8_t)251,
+     (uint8_t)0,
+     (uint8_t)252,
+     (uint8_t)0,
+     (uint8_t)253,
+     (uint8_t)0,
+     (uint8_t)254,
+     (uint8_t)0,
+     (uint8_t)255,
+     (uint8_t)0};
+  uint8_t bluered[32] =
+    {(uint8_t)235,
+     (uint8_t)255,
+     (uint8_t)63,
+     (uint8_t)255,
+     (uint8_t)57,
+     (uint8_t)255,
+     (uint8_t)93,
+     (uint8_t)255,
+     (uint8_t)129,
+     (uint8_t)255,
+     (uint8_t)165,
+     (uint8_t)255,
+     (uint8_t)201,
+     (uint8_t)255,
+     (uint8_t)200,
+     (uint8_t)255,
+     (uint8_t)199,
+     (uint8_t)255,
+     (uint8_t)198,
+     (uint8_t)255,
+     (uint8_t)197,
+     (uint8_t)255,
+     (uint8_t)196,
+     (uint8_t)255,
+     (uint8_t)196,
+     (uint8_t)255,
+     (uint8_t)196,
+     (uint8_t)255,
+     (uint8_t)196,
+     (uint8_t)255,
+     (uint8_t)196,
+     (uint8_t)255};
+  uint8_t *schemes[3] = {original, blackwhite, bluered};
+  uint8_t *background = schemes[scheme] + 0;
+  uint8_t *foreground = schemes[scheme] + 1;
+  if ((int)value > 0) 
+    while (1) {
+      uint8_t tmp;
+      tmp = value;
+      value = (uint8_t)((int)value - 1);
+      ;
+      if (! tmp) break;
+      if (background + 2 < schemes[scheme] + sizeof(original)) {
+        background += 2;
+        foreground += 2;
+      }
+    }
+  snprintf(color,length,"\033[38;5;%d;48;5;%dm",(int)*foreground,
+           (int)*background); /* snprintf_va_1 */
+  return;
+}
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_1(char const * restrict format);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: param0);
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+            param0;
+ */
+int printf_va_2(char const * restrict format, int 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),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: *(param0 + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+            *(param0 + (0 ..));
+ */
+int printf_va_3(char const * restrict format, char *param0);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_4(char const * restrict format);
+
+/*@ 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),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: *(param0 + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+            *(param0 + (0 ..));
+ */
+int printf_va_5(char const * restrict format, char *param0);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_6(char const * restrict format);
+
+/*@ 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),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: *(param0 + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+            *(param0 + (0 ..));
+ */
+int printf_va_7(char const * restrict format, char *param0);
+
+/*@ requires valid_read_string(format);
+    requires
+      \valid(s + (0 .. n - 1)) ∨
+      \valid(s + (0 .. format_length(format) - 1));
+    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, char const * restrict format,
+                  unsigned int param0);
+
+/*@ requires valid_read_string(param1);
+    requires valid_read_string(param2);
+    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),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: *(param4 + (0 ..))),
+            (indirect: param3), (indirect: *(param2 + (0 ..))),
+            (indirect: *(param1 + (0 ..))), (indirect: param0);
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+            *(param4 + (0 ..)), param3, *(param2 + (0 ..)),
+            *(param1 + (0 ..)), param0;
+ */
+int printf_va_8(char const * restrict format, int param0, char *param1,
+                char *param2, int param3, char *param4);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_9(char const * restrict format);
+
+/*@ 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),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: *(param0 + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+            *(param0 + (0 ..));
+ */
+int printf_va_10(char const * restrict format, char *param0);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_11(char const * restrict format);
+
+/*@ 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),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: *(param0 + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+            *(param0 + (0 ..));
+ */
+int printf_va_12(char const * restrict format, char *param0);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_13(char const * restrict format);
+
+/*@ 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),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: *(param0 + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+            *(param0 + (0 ..));
+ */
+int printf_va_14(char const * restrict format, char *param0);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_15(char const * restrict format);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_16(char const * restrict format);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_17(char const * restrict format);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_18(char const * restrict format);
+
+void drawBoard(uint8_t board[4][4])
+{
+  uint8_t x;
+  uint8_t y;
+  char c;
+  char color[40];
+  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 = (uint8_t)0;
+  while ((int)y < 4) {
+    x = (uint8_t)0;
+    while ((int)x < 4) {
+      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 = (uint8_t)((int)x + 1);
+    }
+    printf("\n"); /* printf_va_6 */
+    x = (uint8_t)0;
+    while ((int)x < 4) {
+      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,(size_t)8,"%u",(uint32_t)1 << (int)(*(board + x))[y]); /* snprintf_va_2 */
+        tmp = strlen((char const *)(s));
+        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 = (uint8_t)((int)x + 1);
+    }
+    printf("\n"); /* printf_va_11 */
+    x = (uint8_t)0;
+    while ((int)x < 4) {
+      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 = (uint8_t)((int)x + 1);
+    }
+    printf("\n"); /* printf_va_15 */
+    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 */
+  printf("\033[A"); /* printf_va_18 */
+  return;
+}
+
+uint8_t findTarget(uint8_t array[4], uint8_t x, uint8_t stop)
+{
+  uint8_t __retres;
+  uint8_t t;
+  if ((int)x == 0) {
+    __retres = x;
+    goto return_label;
+  }
+  t = (uint8_t)((int)x - 1);
+  while ((int)t >= 0) {
+    if ((int)*(array + t) != 0) {
+      if ((int)*(array + t) != (int)*(array + x)) {
+        __retres = (uint8_t)((int)t + 1);
+        goto return_label;
+      }
+      __retres = t;
+      goto return_label;
+    }
+    else 
+      if ((int)t == (int)stop) {
+        __retres = t;
+        goto return_label;
+      }
+    t = (uint8_t)((int)t - 1);
+  }
+  __retres = x;
+  return_label: return __retres;
+}
+
+_Bool slideArray(uint8_t array[4])
+{
+  uint8_t x;
+  uint8_t t;
+  _Bool success = (_Bool)0;
+  uint8_t stop = (uint8_t)0;
+  x = (uint8_t)0;
+  while ((int)x < 4) {
+    if ((int)*(array + x) != 0) {
+      t = findTarget(array,x,stop);
+      if ((int)t != (int)x) {
+        if ((int)*(array + t) == 0) *(array + t) = *(array + x);
+        else 
+          if ((int)*(array + t) == (int)*(array + x)) {
+            *(array + t) = (uint8_t)((int)*(array + t) + 1);
+            score += (uint32_t)1 << (int)*(array + t);
+            stop = (uint8_t)((int)t + 1);
+          }
+        *(array + x) = (uint8_t)0;
+        success = (_Bool)1;
+      }
+    }
+    x = (uint8_t)((int)x + 1);
+  }
+  return success;
+}
+
+void rotateBoard(uint8_t board[4][4])
+{
+  uint8_t i;
+  uint8_t j;
+  uint8_t tmp;
+  uint8_t n = (uint8_t)4;
+  i = (uint8_t)0;
+  while ((int)i < (int)n / 2) {
+    j = i;
+    while ((int)j < ((int)n - (int)i) - 1) {
+      tmp = (*(board + i))[j];
+      (*(board + i))[j] = (*(board + j))[((int)n - (int)i) - 1];
+      (*(board + j))[((int)n - (int)i) - 1] = (*(board + (((int)n - (int)i) - 1)))[
+      ((int)n - (int)j) - 1];
+      (*(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 = (uint8_t)((int)j + 1);
+    }
+    i = (uint8_t)((int)i + 1);
+  }
+  return;
+}
+
+_Bool moveUp(uint8_t board[4][4])
+{
+  uint8_t x;
+  _Bool success = (_Bool)0;
+  x = (uint8_t)0;
+  while ((int)x < 4) {
+    {
+      _Bool tmp;
+      tmp = slideArray(*(board + x));
+      success = (_Bool)(((int)success | (int)tmp) != 0);
+    }
+    x = (uint8_t)((int)x + 1);
+  }
+  return success;
+}
+
+_Bool moveLeft(uint8_t board[4][4])
+{
+  _Bool success;
+  rotateBoard(board);
+  success = moveUp(board);
+  rotateBoard(board);
+  rotateBoard(board);
+  rotateBoard(board);
+  return success;
+}
+
+_Bool moveDown(uint8_t board[4][4])
+{
+  _Bool success;
+  rotateBoard(board);
+  rotateBoard(board);
+  success = moveUp(board);
+  rotateBoard(board);
+  rotateBoard(board);
+  return success;
+}
+
+_Bool moveRight(uint8_t board[4][4])
+{
+  _Bool success;
+  rotateBoard(board);
+  rotateBoard(board);
+  rotateBoard(board);
+  success = moveUp(board);
+  rotateBoard(board);
+  return success;
+}
+
+_Bool findPairDown(uint8_t board[4][4])
+{
+  _Bool __retres;
+  uint8_t x;
+  uint8_t y;
+  _Bool success = (_Bool)0;
+  x = (uint8_t)0;
+  while ((int)x < 4) {
+    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 = (uint8_t)((int)y + 1);
+    }
+    x = (uint8_t)((int)x + 1);
+  }
+  __retres = success;
+  return_label: return __retres;
+}
+
+uint8_t countEmpty(uint8_t board[4][4])
+{
+  uint8_t x;
+  uint8_t y;
+  uint8_t count = (uint8_t)0;
+  x = (uint8_t)0;
+  while ((int)x < 4) {
+    y = (uint8_t)0;
+    while ((int)y < 4) {
+      if ((int)(*(board + x))[y] == 0) count = (uint8_t)((int)count + 1);
+      y = (uint8_t)((int)y + 1);
+    }
+    x = (uint8_t)((int)x + 1);
+  }
+  return count;
+}
+
+_Bool gameEnded(uint8_t board[4][4])
+{
+  _Bool __retres;
+  uint8_t tmp;
+  _Bool tmp_0;
+  _Bool tmp_1;
+  _Bool ended = (_Bool)1;
+  tmp = countEmpty(board);
+  if ((int)tmp > 0) {
+    __retres = (_Bool)0;
+    goto return_label;
+  }
+  tmp_0 = findPairDown(board);
+  if (tmp_0) {
+    __retres = (_Bool)0;
+    goto return_label;
+  }
+  rotateBoard(board);
+  tmp_1 = findPairDown(board);
+  if (tmp_1) ended = (_Bool)0;
+  rotateBoard(board);
+  rotateBoard(board);
+  rotateBoard(board);
+  __retres = ended;
+  return_label: return __retres;
+}
+
+void addRandom(uint8_t board[4][4]);
+
+static _Bool addRandom_initialized = (_Bool)0;
+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 = (uint8_t)0;
+  if (! addRandom_initialized) {
+    time_t tmp;
+    tmp = time((time_t *)0);
+    srand((unsigned int)tmp);
+    addRandom_initialized = (_Bool)1;
+  }
+  x = (uint8_t)0;
+  /*@ loop \eva::unroll 4; */
+  while ((int)x < 4) {
+    y = (uint8_t)0;
+    /*@ loop \eva::unroll 4; */
+    while ((int)y < 4) {
+      if ((int)(*(board + x))[y] == 0) {
+        list[len][0] = x;
+        list[len][1] = y;
+        len = (uint8_t)((int)len + 1);
+      }
+      y = (uint8_t)((int)y + 1);
+    }
+    x = (uint8_t)((int)x + 1);
+  }
+  if ((int)len > 0) {
+    int tmp_0;
+    int tmp_1;
+    tmp_0 = rand();
+    r = (uint8_t)(tmp_0 % (int)len);
+    x = list[r][0];
+    y = list[r][1];
+    tmp_1 = rand();
+    n = (uint8_t)((tmp_1 % 10) / 9 + 1);
+    (*(board + x))[y] = n;
+  }
+  return;
+}
+
+void initBoard(uint8_t board[4][4])
+{
+  uint8_t x;
+  uint8_t y;
+  x = (uint8_t)0;
+  /*@ loop \eva::unroll 4; */
+  while ((int)x < 4) {
+    y = (uint8_t)0;
+    /*@ loop \eva::unroll 4; */
+    while ((int)y < 4) {
+      (*(board + x))[y] = (uint8_t)0;
+      y = (uint8_t)((int)y + 1);
+    }
+    x = (uint8_t)((int)x + 1);
+  }
+  addRandom(board);
+  addRandom(board);
+  drawBoard(board);
+  score = (uint32_t)0;
+  return;
+}
+
+void setBufferedInput(_Bool enable);
+
+static _Bool setBufferedInput_enabled = (_Bool)1;
+static struct termios setBufferedInput_old;
+void setBufferedInput(_Bool enable)
+{
+  struct termios new;
+  if (enable) {
+    if (! setBufferedInput_enabled) {
+      tcsetattr(0,0,& setBufferedInput_old);
+      setBufferedInput_enabled = (_Bool)1;
+    }
+    else goto _LAND;
+  }
+  else 
+    _LAND:
+    if (! enable) 
+      if (setBufferedInput_enabled) {
+        tcgetattr(0,& new);
+        setBufferedInput_old = new;
+        new.c_lflag &= (unsigned int)(~ 0000002 & ~ 0000010);
+        tcsetattr(0,0,& new);
+        setBufferedInput_enabled = (_Bool)0;
+      }
+  return;
+}
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: param0);
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+            param0;
+ */
+int printf_va_19(char const * restrict format, int param0);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_20(char const * restrict format);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: param0);
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+            param0;
+ */
+int printf_va_21(char const * restrict format, int param0);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_22(char const * restrict format);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: param0);
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+            param0;
+ */
+int printf_va_23(char const * restrict format, int param0);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_24(char const * restrict format);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: param0);
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+            param0;
+ */
+int printf_va_25(char const * restrict format, int param0);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_26(char const * restrict format);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: param0);
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+            param0;
+ */
+int printf_va_27(char const * restrict format, int param0);
+
+int test(void)
+{
+  int __retres;
+  uint8_t array[4];
+  uint8_t *in;
+  uint8_t *out;
+  uint8_t t;
+  uint8_t tests;
+  uint8_t i;
+  uint8_t data[104] =
+    {(uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)1,
+     (uint8_t)1,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)1,
+     (uint8_t)1,
+     (uint8_t)2,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)1,
+     (uint8_t)0,
+     (uint8_t)1,
+     (uint8_t)2,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)1,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)1,
+     (uint8_t)2,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)1,
+     (uint8_t)0,
+     (uint8_t)1,
+     (uint8_t)0,
+     (uint8_t)2,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)1,
+     (uint8_t)1,
+     (uint8_t)1,
+     (uint8_t)0,
+     (uint8_t)2,
+     (uint8_t)1,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)1,
+     (uint8_t)0,
+     (uint8_t)1,
+     (uint8_t)1,
+     (uint8_t)2,
+     (uint8_t)1,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)1,
+     (uint8_t)1,
+     (uint8_t)0,
+     (uint8_t)1,
+     (uint8_t)2,
+     (uint8_t)1,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)1,
+     (uint8_t)1,
+     (uint8_t)1,
+     (uint8_t)1,
+     (uint8_t)2,
+     (uint8_t)2,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)2,
+     (uint8_t)2,
+     (uint8_t)1,
+     (uint8_t)1,
+     (uint8_t)3,
+     (uint8_t)2,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)1,
+     (uint8_t)1,
+     (uint8_t)2,
+     (uint8_t)2,
+     (uint8_t)2,
+     (uint8_t)3,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)3,
+     (uint8_t)0,
+     (uint8_t)1,
+     (uint8_t)1,
+     (uint8_t)3,
+     (uint8_t)2,
+     (uint8_t)0,
+     (uint8_t)0,
+     (uint8_t)2,
+     (uint8_t)0,
+     (uint8_t)1,
+     (uint8_t)1,
+     (uint8_t)2,
+     (uint8_t)2,
+     (uint8_t)0,
+     (uint8_t)0};
+  _Bool success = (_Bool)1;
+  tests = (uint8_t)((sizeof(data) / sizeof(data[0])) / (unsigned int)(2 * 4));
+  t = (uint8_t)0;
+  while ((int)t < (int)tests) {
+    in = & data[((int)t * 2) * 4];
+    out = in + 4;
+    i = (uint8_t)0;
+    while ((int)i < 4) {
+      array[i] = *(in + i);
+      i = (uint8_t)((int)i + 1);
+    }
+    slideArray(array);
+    i = (uint8_t)0;
+    /*@ loop \eva::unroll 4; */
+    while ((int)i < 4) {
+      if ((int)array[i] != (int)*(out + i)) success = (_Bool)0;
+      i = (uint8_t)((int)i + 1);
+    }
+    if ((int)success == 0) {
+      i = (uint8_t)0;
+      while ((int)i < 4) {
+        printf("%d ",(int)*(in + i)); /* printf_va_19 */
+        i = (uint8_t)((int)i + 1);
+      }
+      printf("=> "); /* printf_va_20 */
+      i = (uint8_t)0;
+      while ((int)i < 4) {
+        printf("%d ",(int)array[i]); /* printf_va_21 */
+        i = (uint8_t)((int)i + 1);
+      }
+      printf("expected "); /* printf_va_22 */
+      i = (uint8_t)0;
+      while ((int)i < 4) {
+        printf("%d ",(int)*(in + i)); /* printf_va_23 */
+        i = (uint8_t)((int)i + 1);
+      }
+      printf("=> "); /* printf_va_24 */
+      i = (uint8_t)0;
+      while ((int)i < 4) {
+        printf("%d ",(int)*(out + i)); /* printf_va_25 */
+        i = (uint8_t)((int)i + 1);
+      }
+      printf("\n"); /* printf_va_26 */
+      break;
+    }
+    t = (uint8_t)((int)t + 1);
+  }
+  if (success) printf("All %hhu tests executed successfully\n",(int)tests); /* printf_va_27 */
+  __retres = ! success;
+  return __retres;
+}
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_28(char const * restrict format);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_29(char const * restrict format);
+
+void signal_callback_handler(int signum)
+{
+  printf("         TERMINATED         \n"); /* printf_va_28 */
+  setBufferedInput((_Bool)1);
+  printf("\033[?25h\033[m"); /* printf_va_29 */
+  exit(signum);
+  return;
+}
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_30(char const * restrict format);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_31(char const * restrict format);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_32(char const * restrict format);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_33(char const * restrict format);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_34(char const * restrict format);
+
+int main(int argc, char **argv)
+{
+  int __retres;
+  uint8_t board[4][4];
+  char c;
+  _Bool success;
+  printf("\033[?25l\033[2J"); /* printf_va_30 */
+  signal(2,& signal_callback_handler);
+  initBoard(board);
+  setBufferedInput((_Bool)0);
+  while (1) {
+    int tmp;
+    tmp = getchar();
+    c = (char)tmp;
+    switch ((int)c) {
+      case 97: case 104: case 68: success = moveLeft(board);
+      break;
+      case 100: case 108: case 67: success = moveRight(board);
+      break;
+      case 119: case 107: case 65: success = moveUp(board);
+      break;
+      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;
+      }
+    }
+    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 */
+  __retres = 0;
+  return __retres;
+}
+
+

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/framac.ast

-/* Generated by Frama-C */
-#include "errno.h"
-#include "signal.h"
-#include "stdarg.h"
-#include "stddef.h"
-#include "stdint.h"
-#include "stdio.h"
-#include "stdlib.h"
-#include "string.h"
-#include "strings.h"
-#include "termios.h"
-#include "time.h"
-#include "unistd.h"
-uint32_t score = (unsigned int)0;
-uint8_t scheme = (unsigned char)0;
-/*@ 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: param1), (indirect: param0);
-    assigns *(s + (0 ..))
-      \from (indirect: n), (indirect: *(format + (0 ..))), param1, param0;
- */
-int snprintf_va_1(char * __restrict s, size_t n,
-                  char const * __restrict format, int param0, int param1);
-
-void getColor(uint8_t value, char *color, size_t length)
-{
-  uint8_t original[32] =
-    {(unsigned char)8,
-     (unsigned char)255,
-     (unsigned char)1,
-     (unsigned char)255,
-     (unsigned char)2,
-     (unsigned char)255,
-     (unsigned char)3,
-     (unsigned char)255,
-     (unsigned char)4,
-     (unsigned char)255,
-     (unsigned char)5,
-     (unsigned char)255,
-     (unsigned char)6,
-     (unsigned char)255,
-     (unsigned char)7,
-     (unsigned char)255,
-     (unsigned char)9,
-     (unsigned char)0,
-     (unsigned char)10,
-     (unsigned char)0,
-     (unsigned char)11,
-     (unsigned char)0,
-     (unsigned char)12,
-     (unsigned char)0,
-     (unsigned char)13,
-     (unsigned char)0,
-     (unsigned char)14,
-     (unsigned char)0,
-     (unsigned char)255,
-     (unsigned char)0,
-     (unsigned char)255,
-     (unsigned char)0};
-  uint8_t blackwhite[32] =
-    {(unsigned char)232,
-     (unsigned char)255,
-     (unsigned char)234,
-     (unsigned char)255,
-     (unsigned char)236,
-     (unsigned char)255,
-     (unsigned char)238,
-     (unsigned char)255,
-     (unsigned char)240,
-     (unsigned char)255,
-     (unsigned char)242,
-     (unsigned char)255,
-     (unsigned char)244,
-     (unsigned char)255,
-     (unsigned char)246,
-     (unsigned char)0,
-     (unsigned char)248,
-     (unsigned char)0,
-     (unsigned char)249,
-     (unsigned char)0,
-     (unsigned char)250,
-     (unsigned char)0,
-     (unsigned char)251,
-     (unsigned char)0,
-     (unsigned char)252,
-     (unsigned char)0,
-     (unsigned char)253,
-     (unsigned char)0,
-     (unsigned char)254,
-     (unsigned char)0,
-     (unsigned char)255,
-     (unsigned char)0};
-  uint8_t bluered[32] =
-    {(unsigned char)235,
-     (unsigned char)255,
-     (unsigned char)63,
-     (unsigned char)255,
-     (unsigned char)57,
-     (unsigned char)255,
-     (unsigned char)93,
-     (unsigned char)255,
-     (unsigned char)129,
-     (unsigned char)255,
-     (unsigned char)165,
-     (unsigned char)255,
-     (unsigned char)201,
-     (unsigned char)255,
-     (unsigned char)200,
-     (unsigned char)255,
-     (unsigned char)199,
-     (unsigned char)255,
-     (unsigned char)198,
-     (unsigned char)255,
-     (unsigned char)197,
-     (unsigned char)255,
-     (unsigned char)196,
-     (unsigned char)255,
-     (unsigned char)196,
-     (unsigned char)255,
-     (unsigned char)196,
-     (unsigned char)255,
-     (unsigned char)196,
-     (unsigned char)255,
-     (unsigned char)196,
-     (unsigned char)255};
-  uint8_t *schemes[3] = {original, blackwhite, bluered};
-  uint8_t *background = schemes[scheme] + 0;
-  uint8_t *foreground = schemes[scheme] + 1;
-  if ((int)value > 0) 
-    while (1) {
-      uint8_t tmp;
-      tmp = value;
-      value = (uint8_t)((int)value - 1);
-      ;
-      if (! tmp) break;
-      if (background + 2 < schemes[scheme] + sizeof(original)) {
-        background += 2;
-        foreground += 2;
-      }
-    }
-  snprintf_va_1(color,length,"\033[38;5;%d;48;5;%dm",(int)*foreground,
-                (int)*background);
-  return;
-}
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_1(char const * __restrict format);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..))), (indirect: param0);
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
-            param0;
- */
-int printf_va_2(char const * __restrict format, int param0);
-
-/*@ requires valid_read_string(format);
-    requires valid_read_string(param0);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..))), (indirect: *(param0 + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
-            *(param0 + (0 ..));
- */
-int printf_va_3(char const * __restrict format, char *param0);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_4(char const * __restrict format);
-
-/*@ requires valid_read_string(format);
-    requires valid_read_string(param0);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..))), (indirect: *(param0 + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
-            *(param0 + (0 ..));
- */
-int printf_va_5(char const * __restrict format, char *param0);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_6(char const * __restrict format);
-
-/*@ requires valid_read_string(format);
-    requires valid_read_string(param0);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..))), (indirect: *(param0 + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
-            *(param0 + (0 ..));
- */
-int printf_va_7(char const * __restrict format, char *param0);
-
-/*@ 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,
-                  char const * __restrict format, unsigned int param0);
-
-/*@ requires valid_read_string(format);
-    requires valid_read_string(param4);
-    requires valid_read_string(param2);
-    requires valid_read_string(param1);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..))), (indirect: *(param4 + (0 ..))),
-            (indirect: param3), (indirect: *(param2 + (0 ..))),
-            (indirect: *(param1 + (0 ..))), (indirect: param0);
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
-            *(param4 + (0 ..)), param3, *(param2 + (0 ..)),
-            *(param1 + (0 ..)), param0;
- */
-int printf_va_8(char const * __restrict format, int param0, char *param1,
-                char *param2, int param3, char *param4);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_9(char const * __restrict format);
-
-/*@ requires valid_read_string(format);
-    requires valid_read_string(param0);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..))), (indirect: *(param0 + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
-            *(param0 + (0 ..));
- */
-int printf_va_10(char const * __restrict format, char *param0);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_11(char const * __restrict format);
-
-/*@ requires valid_read_string(format);
-    requires valid_read_string(param0);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..))), (indirect: *(param0 + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
-            *(param0 + (0 ..));
- */
-int printf_va_12(char const * __restrict format, char *param0);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_13(char const * __restrict format);
-
-/*@ requires valid_read_string(format);
-    requires valid_read_string(param0);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..))), (indirect: *(param0 + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
-            *(param0 + (0 ..));
- */
-int printf_va_14(char const * __restrict format, char *param0);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_15(char const * __restrict format);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_16(char const * __restrict format);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_17(char const * __restrict format);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_18(char const * __restrict format);
-
-void drawBoard(uint8_t (* /*[4]*/ board)[4])
-{
-  uint8_t x;
-  uint8_t y;
-  char c;
-  char color[40];
-  char reset[4] = {(char)'\033', (char)'[', (char)'m', (char)'\000'};
-  printf_va_1("\033[H");
-  printf_va_2("2048.c %17d pts\n\n",(int)score);
-  y = (unsigned char)0;
-  while ((int)y < 4) {
-    x = (unsigned char)0;
-    while ((int)x < 4) {
-      getColor((*(board + x))[y],color,(unsigned int)40);
-      printf_va_3("%s",color);
-      printf_va_4("       ");
-      printf_va_5("%s",reset);
-      x = (uint8_t)((int)x + 1);
-    }
-    printf_va_6("\n");
-    x = (unsigned char)0;
-    while ((int)x < 4) {
-      getColor((*(board + x))[y],color,(unsigned int)40);
-      printf_va_7("%s",color);
-      if ((int)(*(board + x))[y] != 0) {
-        char s[8];
-        size_t tmp;
-        snprintf_va_2(s,(unsigned int)8,"%u",
-                      (unsigned int)1 << (int)(*(board + x))[y]);
-        tmp = strlen((char const *)(s));
-        uint8_t t = (unsigned char)((size_t)7 - tmp);
-        printf_va_8("%*s%s%*s",(int)t - (int)t / 2,(char *)"",s,(int)t / 2,
-                    (char *)"");
-      }
-      else printf_va_9("   \302\267   ");
-      printf_va_10("%s",reset);
-      x = (uint8_t)((int)x + 1);
-    }
-    printf_va_11("\n");
-    x = (unsigned char)0;
-    while ((int)x < 4) {
-      getColor((*(board + x))[y],color,(unsigned int)40);
-      printf_va_12("%s",color);
-      printf_va_13("       ");
-      printf_va_14("%s",reset);
-      x = (uint8_t)((int)x + 1);
-    }
-    printf_va_15("\n");
-    y = (uint8_t)((int)y + 1);
-  }
-  printf_va_16("\n");
-  printf_va_17("        \342\206\220,\342\206\221,\342\206\222,\342\206\223 or q        \n");
-  printf_va_18("\033[A");
-  return;
-}
-
-uint8_t findTarget(uint8_t * /*[4]*/ array, uint8_t x, uint8_t stop)
-{
-  uint8_t __retres;
-  uint8_t t;
-  if ((int)x == 0) {
-    __retres = x;
-    goto return_label;
-  }
-  t = (unsigned char)((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);
-        goto return_label;
-      }
-      __retres = t;
-      goto return_label;
-    }
-    else 
-      if ((int)t == (int)stop) {
-        __retres = t;
-        goto return_label;
-      }
-    t = (uint8_t)((int)t - 1);
-  }
-  __retres = x;
-  return_label: return __retres;
-}
-
-_Bool slideArray(uint8_t * /*[4]*/ array)
-{
-  uint8_t x;
-  uint8_t t;
-  _Bool success = (_Bool)0;
-  uint8_t stop = (unsigned char)0;
-  x = (unsigned char)0;
-  while ((int)x < 4) {
-    if ((int)*(array + x) != 0) {
-      t = findTarget(array,x,stop);
-      if ((int)t != (int)x) {
-        if ((int)*(array + t) == 0) *(array + t) = *(array + x);
-        else 
-          if ((int)*(array + t) == (int)*(array + x)) {
-            *(array + t) = (uint8_t)((int)*(array + t) + 1);
-            score += (unsigned int)1 << (int)*(array + t);
-            stop = (unsigned char)((int)t + 1);
-          }
-        *(array + x) = (unsigned char)0;
-        success = (_Bool)1;
-      }
-    }
-    x = (uint8_t)((int)x + 1);
-  }
-  return success;
-}
-
-void rotateBoard(uint8_t (* /*[4]*/ board)[4])
-{
-  uint8_t i;
-  uint8_t j;
-  uint8_t tmp;
-  uint8_t n = (unsigned char)4;
-  i = (unsigned char)0;
-  while ((int)i < (int)n / 2) {
-    j = i;
-    while ((int)j < ((int)n - (int)i) - 1) {
-      tmp = (*(board + i))[j];
-      (*(board + i))[j] = (*(board + j))[((int)n - (int)i) - 1];
-      (*(board + j))[((int)n - (int)i) - 1] = (*(board + (((int)n - (int)i) - 1)))[
-      ((int)n - (int)j) - 1];
-      (*(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 = (uint8_t)((int)j + 1);
-    }
-    i = (uint8_t)((int)i + 1);
-  }
-  return;
-}
-
-_Bool moveUp(uint8_t (* /*[4]*/ board)[4])
-{
-  uint8_t x;
-  _Bool success = (_Bool)0;
-  x = (unsigned char)0;
-  while ((int)x < 4) {
-    {
-      _Bool tmp;
-      tmp = slideArray(*(board + x));
-      success = (_Bool)(((int)success | (int)tmp) != 0);
-    }
-    x = (uint8_t)((int)x + 1);
-  }
-  return success;
-}
-
-_Bool moveLeft(uint8_t (* /*[4]*/ board)[4])
-{
-  _Bool success;
-  rotateBoard(board);
-  success = moveUp(board);
-  rotateBoard(board);
-  rotateBoard(board);
-  rotateBoard(board);
-  return success;
-}
-
-_Bool moveDown(uint8_t (* /*[4]*/ board)[4])
-{
-  _Bool success;
-  rotateBoard(board);
-  rotateBoard(board);
-  success = moveUp(board);
-  rotateBoard(board);
-  rotateBoard(board);
-  return success;
-}
-
-_Bool moveRight(uint8_t (* /*[4]*/ board)[4])
-{
-  _Bool success;
-  rotateBoard(board);
-  rotateBoard(board);
-  rotateBoard(board);
-  success = moveUp(board);
-  rotateBoard(board);
-  return success;
-}
-
-_Bool findPairDown(uint8_t (* /*[4]*/ board)[4])
-{
-  _Bool __retres;
-  uint8_t x;
-  uint8_t y;
-  _Bool success = (_Bool)0;
-  x = (unsigned char)0;
-  while ((int)x < 4) {
-    y = (unsigned char)0;
-    while ((int)y < 4 - 1) {
-      if ((int)(*(board + x))[y] == (int)(*(board + x))[(int)y + 1]) {
-        __retres = (_Bool)1;
-        goto return_label;
-      }
-      y = (uint8_t)((int)y + 1);
-    }
-    x = (uint8_t)((int)x + 1);
-  }
-  __retres = success;
-  return_label: return __retres;
-}
-
-uint8_t countEmpty(uint8_t (* /*[4]*/ board)[4])
-{
-  uint8_t x;
-  uint8_t y;
-  uint8_t count = (unsigned char)0;
-  x = (unsigned char)0;
-  while ((int)x < 4) {
-    y = (unsigned char)0;
-    while ((int)y < 4) {
-      if ((int)(*(board + x))[y] == 0) count = (uint8_t)((int)count + 1);
-      y = (uint8_t)((int)y + 1);
-    }
-    x = (uint8_t)((int)x + 1);
-  }
-  return count;
-}
-
-_Bool gameEnded(uint8_t (* /*[4]*/ board)[4])
-{
-  _Bool __retres;
-  uint8_t tmp;
-  _Bool tmp_0;
-  _Bool tmp_1;
-  _Bool ended = (_Bool)1;
-  tmp = countEmpty(board);
-  if ((int)tmp > 0) {
-    __retres = (_Bool)0;
-    goto return_label;
-  }
-  tmp_0 = findPairDown(board);
-  if (tmp_0) {
-    __retres = (_Bool)0;
-    goto return_label;
-  }
-  rotateBoard(board);
-  tmp_1 = findPairDown(board);
-  if (tmp_1) ended = (_Bool)0;
-  rotateBoard(board);
-  rotateBoard(board);
-  rotateBoard(board);
-  __retres = ended;
-  return_label: return __retres;
-}
-
-void addRandom(uint8_t (* /*[4]*/ board)[4]);
-
-static _Bool addRandom_initialized = (_Bool)0;
-void addRandom(uint8_t (* /*[4]*/ board)[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;
-  if (! addRandom_initialized) {
-    time_t tmp;
-    tmp = time((time_t *)0);
-    srand((unsigned int)tmp);
-    addRandom_initialized = (_Bool)1;
-  }
-  x = (unsigned char)0;
-  /*@ loop unroll 4; */
-  while ((int)x < 4) {
-    y = (unsigned char)0;
-    /*@ loop unroll 4; */
-    while ((int)y < 4) {
-      if ((int)(*(board + x))[y] == 0) {
-        list[len][0] = x;
-        list[len][1] = y;
-        len = (uint8_t)((int)len + 1);
-      }
-      y = (uint8_t)((int)y + 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);
-    x = list[r][0];
-    y = list[r][1];
-    tmp_1 = rand();
-    n = (unsigned char)((tmp_1 % 10) / 9 + 1);
-    (*(board + x))[y] = n;
-  }
-  return;
-}
-
-void initBoard(uint8_t (* /*[4]*/ board)[4])
-{
-  uint8_t x;
-  uint8_t y;
-  x = (unsigned char)0;
-  /*@ loop unroll 4; */
-  while ((int)x < 4) {
-    y = (unsigned char)0;
-    /*@ loop unroll 4; */
-    while ((int)y < 4) {
-      (*(board + x))[y] = (unsigned char)0;
-      y = (uint8_t)((int)y + 1);
-    }
-    x = (uint8_t)((int)x + 1);
-  }
-  addRandom(board);
-  addRandom(board);
-  drawBoard(board);
-  score = (unsigned int)0;
-  return;
-}
-
-void setBufferedInput(_Bool enable);
-
-static _Bool setBufferedInput_enabled = (_Bool)1;
-static struct termios setBufferedInput_old;
-void setBufferedInput(_Bool enable)
-{
-  struct termios new;
-  if (enable) {
-    if (! setBufferedInput_enabled) {
-      tcsetattr(0,0,& setBufferedInput_old);
-      setBufferedInput_enabled = (_Bool)1;
-    }
-    else goto _LAND;
-  }
-  else 
-    _LAND:
-    if (! enable) 
-      if (setBufferedInput_enabled) {
-        tcgetattr(0,& new);
-        setBufferedInput_old = new;
-        new.c_lflag &= (unsigned int)(~ 0000002 & ~ 0000010);
-        tcsetattr(0,0,& new);
-        setBufferedInput_enabled = (_Bool)0;
-      }
-  return;
-}
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..))), (indirect: param0);
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
-            param0;
- */
-int printf_va_19(char const * __restrict format, int param0);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_20(char const * __restrict format);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..))), (indirect: param0);
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
-            param0;
- */
-int printf_va_21(char const * __restrict format, int param0);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_22(char const * __restrict format);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..))), (indirect: param0);
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
-            param0;
- */
-int printf_va_23(char const * __restrict format, int param0);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_24(char const * __restrict format);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..))), (indirect: param0);
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
-            param0;
- */
-int printf_va_25(char const * __restrict format, int param0);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_26(char const * __restrict format);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..))), (indirect: param0);
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
-            param0;
- */
-int printf_va_27(char const * __restrict format, int param0);
-
-int test(void)
-{
-  int __retres;
-  uint8_t array[4];
-  uint8_t *in;
-  uint8_t *out;
-  uint8_t t;
-  uint8_t tests;
-  uint8_t i;
-  uint8_t data[104] =
-    {(unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)1,
-     (unsigned char)1,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)1,
-     (unsigned char)1,
-     (unsigned char)2,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)1,
-     (unsigned char)0,
-     (unsigned char)1,
-     (unsigned char)2,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)1,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)1,
-     (unsigned char)2,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)1,
-     (unsigned char)0,
-     (unsigned char)1,
-     (unsigned char)0,
-     (unsigned char)2,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)1,
-     (unsigned char)1,
-     (unsigned char)1,
-     (unsigned char)0,
-     (unsigned char)2,
-     (unsigned char)1,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)1,
-     (unsigned char)0,
-     (unsigned char)1,
-     (unsigned char)1,
-     (unsigned char)2,
-     (unsigned char)1,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)1,
-     (unsigned char)1,
-     (unsigned char)0,
-     (unsigned char)1,
-     (unsigned char)2,
-     (unsigned char)1,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)1,
-     (unsigned char)1,
-     (unsigned char)1,
-     (unsigned char)1,
-     (unsigned char)2,
-     (unsigned char)2,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)2,
-     (unsigned char)2,
-     (unsigned char)1,
-     (unsigned char)1,
-     (unsigned char)3,
-     (unsigned char)2,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)1,
-     (unsigned char)1,
-     (unsigned char)2,
-     (unsigned char)2,
-     (unsigned char)2,
-     (unsigned char)3,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)3,
-     (unsigned char)0,
-     (unsigned char)1,
-     (unsigned char)1,
-     (unsigned char)3,
-     (unsigned char)2,
-     (unsigned char)0,
-     (unsigned char)0,
-     (unsigned char)2,
-     (unsigned char)0,
-     (unsigned char)1,
-     (unsigned char)1,
-     (unsigned char)2,
-     (unsigned char)2,
-     (unsigned char)0,
-     (unsigned char)0};
-  _Bool success = (_Bool)1;
-  tests = (unsigned char)((sizeof(data) / sizeof(data[0])) / (unsigned int)(
-                          2 * 4));
-  t = (unsigned char)0;
-  while ((int)t < (int)tests) {
-    in = & data[((int)t * 2) * 4];
-    out = in + 4;
-    i = (unsigned char)0;
-    while ((int)i < 4) {
-      array[i] = *(in + i);
-      i = (uint8_t)((int)i + 1);
-    }
-    slideArray(array);
-    i = (unsigned char)0;
-    /*@ loop unroll 4; */
-    while ((int)i < 4) {
-      if ((int)array[i] != (int)*(out + i)) success = (_Bool)0;
-      i = (uint8_t)((int)i + 1);
-    }
-    if ((int)success == 0) {
-      i = (unsigned char)0;
-      while ((int)i < 4) {
-        printf_va_19("%d ",(int)*(in + i));
-        i = (uint8_t)((int)i + 1);
-      }
-      printf_va_20("=> ");
-      i = (unsigned char)0;
-      while ((int)i < 4) {
-        printf_va_21("%d ",(int)array[i]);
-        i = (uint8_t)((int)i + 1);
-      }
-      printf_va_22("expected ");
-      i = (unsigned char)0;
-      while ((int)i < 4) {
-        printf_va_23("%d ",(int)*(in + i));
-        i = (uint8_t)((int)i + 1);
-      }
-      printf_va_24("=> ");
-      i = (unsigned char)0;
-      while ((int)i < 4) {
-        printf_va_25("%d ",(int)*(out + i));
-        i = (uint8_t)((int)i + 1);
-      }
-      printf_va_26("\n");
-      break;
-    }
-    t = (uint8_t)((int)t + 1);
-  }
-  if (success) printf_va_27("All %hhu tests executed successfully\n",
-                            (int)tests);
-  __retres = ! success;
-  return __retres;
-}
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_28(char const * __restrict format);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_29(char const * __restrict format);
-
-void signal_callback_handler(int signum)
-{
-  printf_va_28("         TERMINATED         \n");
-  setBufferedInput((_Bool)1);
-  printf_va_29("\033[?25h\033[m");
-  exit(signum);
-  return;
-}
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_30(char const * __restrict format);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_31(char const * __restrict format);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_32(char const * __restrict format);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_33(char const * __restrict format);
-
-/*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_34(char const * __restrict format);
-
-int main(int argc, char **argv)
-{
-  int __retres;
-  uint8_t board[4][4];
-  char c;
-  _Bool success;
-  printf_va_30("\033[?25l\033[2J");
-  signal(2,& signal_callback_handler);
-  initBoard(board);
-  setBufferedInput((_Bool)0);
-  while (1) {
-    {
-      int tmp;
-      tmp = getchar();
-      c = (char)tmp;
-      switch ((int)c) {
-        case 97: case 104: case 68: success = moveLeft(board);
-        break;
-        case 100: case 108: case 67: success = moveRight(board);
-        break;
-        case 119: case 107: case 65: success = moveUp(board);
-        break;
-        case 115: case 106: case 66: success = moveDown(board);
-        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_va_31("         GAME OVER          \n");
-          break;
-        }
-      }
-      if ((int)c == 'q') {
-        int tmp_1;
-        printf_va_32("        QUIT? (y/n)         \n");
-        tmp_1 = getchar();
-        c = (char)tmp_1;
-        if ((int)c == 'y') break;
-        drawBoard(board);
-      }
-      if ((int)c == 'r') {
-        int tmp_2;
-        printf_va_33("       RESTART? (y/n)       \n");
-        tmp_2 = getchar();
-        c = (char)tmp_2;
-        if ((int)c == 'y') initBoard(board);
-        drawBoard(board);
-      }
-    }
-  }
-  setBufferedInput((_Bool)1);
-  printf_va_34("\033[?25h\033[m");
-  __retres = 0;
-  return __retres;
-}
-
-

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