Project

General

Profile

Download (591 Bytes)

Bug #330 » latt2.c

small example of a driver thta causes bug - Pavel Shved, 09/21/2010 06:09 PM

 
void error()
{
ERROR: goto ERROR;
}

int nondet();
int call();
int some();
int useless();
int functions();
int to();
int make();
int other();
int branches();
int proceed();

int main()
{
int a,b,z;
if (nondet()){
a=10; b=1;
}else{
if (nondet()){
a=1; b=10;
}else{
a=1; b=1;
call(); //due to DFS traversal, this branch may be at z=10 before the other!
some();
useless();
functions();
to();
make();
other();
branches();
proceed();
}
}
z = 10; // coverage error happens here
if (a==1 && b==1) error(); // and leads to missing this error!
}
(1-1/12)