Project

General

Profile

Download (927 Bytes)

Bug #330 » stateful.c

example which should be unsafe with lattice - Vadim Mutilin, 12/08/2010 07:50 PM

 
void error()
{
ERROR: goto ERROR;
}

int nondet_int(void);
int open_called = 0;
int misc_nondet_int(void);

int f1() {
if(misc_nondet_int()) {
//open was not correctly finished
return 1;
} else {
open_called = 1;
return 0;
}
}

void f2() {};
void f3() {};
void f4() {};

void f5() {
//release should be after open
//verdict should be safe
if(open_called) {
//safe
open_called = 0;
} else {
//unsafe
error();
}
return 0;
};

int main(void) {
int seq = 0;

while(nondet_int()) {

switch(nondet_int()) {
case 0:
if(seq==0) {
f1();
seq++;
}
break;
case 1:
if(seq==1) {
f2();
seq++;
}
break;
case 2:
if(seq==2) {
f3();
seq++;
}
break;
case 3:
if(seq==3) {
f4();
seq++;
}
break;
case 4:
if(seq==4) {
f5();
seq++;
}
break;

break;
default: break;
}
}

return 0;

}
(3-3/12)