-
Andre Maroneze authoredAndre Maroneze authored
framac.ast 35.24 KiB
/* 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;
}