Commit 63b59078 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

Initial commit

parents
# Common rules used by all subdirectories
*.sav
*.o
*~
.frama-c
config.status
lia.cache
running
command
parse.log
eva.log
stats.txt
flamegraph.txt
# ignore timestamped versions
*_20*-*.eva
*_20*-*.parse
*.error
benchs-value.csv
bench_clone
[submodule "frama-c"]
path = frama-c
url = https://git.frama-c.com/pub/frama-c.git
/*
============================================================================
Name : 2048.c
Author : Maurits van der Schee
Description : Console version of the game "2048" for GNU/Linux
============================================================================
*/
#define _XOPEN_SOURCE 500
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <unistd.h>
#include <termios.h>
#include <stdbool.h>
#include <stdint.h>
#include <time.h>
#include <signal.h>
#define SIZE 4
uint32_t score=0;
uint8_t scheme=0;
void getColor(uint8_t value, char *color, size_t length) {
uint8_t original[] = {8,255,1,255,2,255,3,255,4,255,5,255,6,255,7,255,9,0,10,0,11,0,12,0,13,0,14,0,255,0,255,0};
uint8_t blackwhite[] = {232,255,234,255,236,255,238,255,240,255,242,255,244,255,246,0,248,0,249,0,250,0,251,0,252,0,253,0,254,0,255,0};
uint8_t bluered[] = {235,255,63,255,57,255,93,255,129,255,165,255,201,255,200,255,199,255,198,255,197,255,196,255,196,255,196,255,196,255,196,255};
uint8_t *schemes[] = {original,blackwhite,bluered};
uint8_t *background = schemes[scheme]+0;
uint8_t *foreground = schemes[scheme]+1;
if (value > 0) while (value--) {
if (background+2<schemes[scheme]+sizeof(original)) {
background+=2;
foreground+=2;
}
}
snprintf(color,length,"\033[38;5;%d;48;5;%dm",*foreground,*background);
}
void drawBoard(uint8_t board[SIZE][SIZE]) {
uint8_t x,y;
char c;
char color[40], reset[] = "\033[m";
printf("\033[H");
printf("2048.c %17d pts\n\n",score);
for (y=0;y<SIZE;y++) {
for (x=0;x<SIZE;x++) {
getColor(board[x][y],color,40);
printf("%s",color);
printf(" ");
printf("%s",reset);
}
printf("\n");
for (x=0;x<SIZE;x++) {
getColor(board[x][y],color,40);
printf("%s",color);
if (board[x][y]!=0) {
char s[8];
snprintf(s,8,"%u",(uint32_t)1<<board[x][y]);
uint8_t t = 7-strlen(s);
printf("%*s%s%*s",t-t/2,"",s,t/2,"");
} else {
printf(" · ");
}
printf("%s",reset);
}
printf("\n");
for (x=0;x<SIZE;x++) {
getColor(board[x][y],color,40);
printf("%s",color);
printf(" ");
printf("%s",reset);
}
printf("\n");
}
printf("\n");
printf(" ←,↑,→,↓ or q \n");
printf("\033[A"); // one line up
}
uint8_t findTarget(uint8_t array[SIZE],uint8_t x,uint8_t stop) {
uint8_t t;
// if the position is already on the first, don't evaluate
if (x==0) {
return x;
}
for(t=x-1;t>=0;t--) {
if (array[t]!=0) {
if (array[t]!=array[x]) {
// merge is not possible, take next position
return t+1;
}
return t;
} else {
// we should not slide further, return this one
if (t==stop) {
return t;
}
}
}
// we did not find a
return x;
}
bool slideArray(uint8_t array[SIZE]) {
bool success = false;
uint8_t x,t,stop=0;
for (x=0;x<SIZE;x++) {
if (array[x]!=0) {
t = findTarget(array,x,stop);
// if target is not original position, then move or merge
if (t!=x) {
// if target is zero, this is a move
if (array[t]==0) {
array[t]=array[x];
} else if (array[t]==array[x]) {
// merge (increase power of two)
array[t]++;
// increase score
score+=(uint32_t)1<<array[t];
// set stop to avoid double merge
stop = t+1;
}
array[x]=0;
success = true;
}
}
}
return success;
}
void rotateBoard(uint8_t board[SIZE][SIZE]) {
uint8_t i,j,n=SIZE;
uint8_t tmp;
for (i=0; i<n/2; i++) {
for (j=i; j<n-i-1; j++) {
tmp = board[i][j];
board[i][j] = board[j][n-i-1];
board[j][n-i-1] = board[n-i-1][n-j-1];
board[n-i-1][n-j-1] = board[n-j-1][i];
board[n-j-1][i] = tmp;
}
}
}
bool moveUp(uint8_t board[SIZE][SIZE]) {
bool success = false;
uint8_t x;
for (x=0;x<SIZE;x++) {
success |= slideArray(board[x]);
}
return success;
}
bool moveLeft(uint8_t board[SIZE][SIZE]) {
bool success;
rotateBoard(board);
success = moveUp(board);
rotateBoard(board);
rotateBoard(board);
rotateBoard(board);
return success;
}
bool moveDown(uint8_t board[SIZE][SIZE]) {
bool success;
rotateBoard(board);
rotateBoard(board);
success = moveUp(board);
rotateBoard(board);
rotateBoard(board);
return success;
}
bool moveRight(uint8_t board[SIZE][SIZE]) {
bool success;
rotateBoard(board);
rotateBoard(board);
rotateBoard(board);
success = moveUp(board);
rotateBoard(board);
return success;
}
bool findPairDown(uint8_t board[SIZE][SIZE]) {
bool success = false;
uint8_t x,y;
for (x=0;x<SIZE;x++) {
for (y=0;y<SIZE-1;y++) {
if (board[x][y]==board[x][y+1]) return true;
}
}
return success;
}
uint8_t countEmpty(uint8_t board[SIZE][SIZE]) {
uint8_t x,y;
uint8_t count=0;
for (x=0;x<SIZE;x++) {
for (y=0;y<SIZE;y++) {
if (board[x][y]==0) {
count++;
}
}
}
return count;
}
bool gameEnded(uint8_t board[SIZE][SIZE]) {
bool ended = true;
if (countEmpty(board)>0) return false;
if (findPairDown(board)) return false;
rotateBoard(board);
if (findPairDown(board)) ended = false;
rotateBoard(board);
rotateBoard(board);
rotateBoard(board);
return ended;
}
void addRandom(uint8_t board[SIZE][SIZE]) {
static bool initialized = false;
uint8_t x,y;
uint8_t r,len=0;
uint8_t n,list[SIZE*SIZE][2];
if (!initialized) {
srand(time(NULL));
initialized = true;
}
//@ loop unroll SIZE;
for (x=0;x<SIZE;x++) {
//@ loop unroll SIZE;
for (y=0;y<SIZE;y++) {
if (board[x][y]==0) {
list[len][0]=x;
list[len][1]=y;
len++;
}
}
}
if (len>0) {
r = rand()%len;
x = list[r][0];
y = list[r][1];
n = (rand()%10)/9+1;
board[x][y]=n;
}
}
void initBoard(uint8_t board[SIZE][SIZE]) {
uint8_t x,y;
//@ loop unroll SIZE;
for (x=0;x<SIZE;x++) {
//@ loop unroll SIZE;
for (y=0;y<SIZE;y++) {
board[x][y]=0;
}
}
addRandom(board);
addRandom(board);
drawBoard(board);
score = 0;
}
void setBufferedInput(bool enable) {
static bool enabled = true;
static struct termios old;
struct termios new;
if (enable && !enabled) {
// restore the former settings
tcsetattr(STDIN_FILENO,TCSANOW,&old);
// set the new state
enabled = true;
} else if (!enable && enabled) {
// get the terminal settings for standard input
tcgetattr(STDIN_FILENO,&new);
// we want to keep the old setting to restore them at the end
old = new;
// disable canonical mode (buffered i/o) and local echo
new.c_lflag &=(~ICANON & ~ECHO);
// set the new settings immediately
tcsetattr(STDIN_FILENO,TCSANOW,&new);
// set the new state
enabled = false;
}
}
int test() {
uint8_t array[SIZE];
// these are exponents with base 2 (1=2 2=4 3=8)
uint8_t data[] = {
0,0,0,1, 1,0,0,0,
0,0,1,1, 2,0,0,0,
0,1,0,1, 2,0,0,0,
1,0,0,1, 2,0,0,0,
1,0,1,0, 2,0,0,0,
1,1,1,0, 2,1,0,0,
1,0,1,1, 2,1,0,0,
1,1,0,1, 2,1,0,0,
1,1,1,1, 2,2,0,0,
2,2,1,1, 3,2,0,0,
1,1,2,2, 2,3,0,0,
3,0,1,1, 3,2,0,0,
2,0,1,1, 2,2,0,0
};
uint8_t *in,*out;
uint8_t t,tests;
uint8_t i;
bool success = true;
tests = (sizeof(data)/sizeof(data[0]))/(2*SIZE);
for (t=0;t<tests;t++) {
in = data+t*2*SIZE;
out = in + SIZE;
for (i=0;i<SIZE;i++) {
array[i] = in[i];
}
slideArray(array);
//@ loop unroll SIZE;
for (i=0;i<SIZE;i++) {
if (array[i] != out[i]) {
success = false;
}
}
if (success==false) {
for (i=0;i<SIZE;i++) {
printf("%d ",in[i]);
}
printf("=> ");
for (i=0;i<SIZE;i++) {
printf("%d ",array[i]);
}
printf("expected ");
for (i=0;i<SIZE;i++) {
printf("%d ",in[i]);
}
printf("=> ");
for (i=0;i<SIZE;i++) {
printf("%d ",out[i]);
}
printf("\n");
break;
}
}
if (success) {
printf("All %hhu tests executed successfully\n",tests);
}
return !success;
}
void signal_callback_handler(int signum) {
printf(" TERMINATED \n");
setBufferedInput(true);
printf("\033[?25h\033[m");
exit(signum);
}
int main(int argc, char *argv[]) {
uint8_t board[SIZE][SIZE];
char c;
bool success;
/*if (argc == 2 && strcmp(argv[1],"test")==0) {
return test();
}
if (argc == 2 && strcmp(argv[1],"blackwhite")==0) {
scheme = 1;
}
if (argc == 2 && strcmp(argv[1],"bluered")==0) {
scheme = 2;
}*/
printf("\033[?25l\033[2J");
// register signal handler for when ctrl-c is pressed
signal(SIGINT, signal_callback_handler);
initBoard(board);
setBufferedInput(false);
while (true) {
c=getchar();
switch(c) {
case 97: // 'a' key
case 104: // 'h' key
case 68: // left arrow
success = moveLeft(board); break;
case 100: // 'd' key
case 108: // 'l' key
case 67: // right arrow
success = moveRight(board); break;
case 119: // 'w' key
case 107: // 'k' key
case 65: // up arrow
success = moveUp(board); break;
case 115: // 's' key
case 106: // 'j' key
case 66: // down arrow
success = moveDown(board); break;
default: success = false;
}
if (success) {
drawBoard(board);
usleep(150000);
addRandom(board);
drawBoard(board);
if (gameEnded(board)) {
printf(" GAME OVER \n");
break;
}
}
if (c=='q') {
printf(" QUIT? (y/n) \n");
c=getchar();
if (c=='y') {
break;
}
drawBoard(board);
}
if (c=='r') {
printf(" RESTART? (y/n) \n");
c=getchar();
if (c=='y') {
initBoard(board);
}
drawBoard(board);
}
}
setBufferedInput(true);
printf("\033[?25h\033[m");
return EXIT_SUCCESS;
}
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)
[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%)
This diff is collapsed.
[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.c:46:[variadic] warning: Incorrect type for argument 2. The argument will be cast from uint32_t to int.
# 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,