Project

General

Profile

Download (526 Bytes)

Bug #5720 » getchar1.c

C code - Sepideh Asadi, 20/10/2017 02:39

 
#define SIZE 256
#define EOF -1
#define ERROR -1

int lookup[SIZE];

int nondet_int();

int getchar() {
int x = nondet_int();

__CPROVER_assume(x <= 255);
__CPROVER_assume(x >= -1);
return x;
}

int choice(int a, int b) {
if (a < 0 || a >= SIZE)
return ERROR;
if (b < 0 || b >= SIZE)
return ERROR;

int av = getchar();
int bv = getchar();

if (av >= bv)
return a;
return b;
}


int main() {
int x, y, t;

t = choice(10, 20);
assert (t == 10 || t == 20);
}
(1-1/2)