Basic usage - verifying simple C programs

[Anubhav Sharma]

Hello,

I've ufo and ufofe installed on my machine. I've been trying to figure out how to use the front end to verify C programs with assume statements, assert statements and loops.

For example, how do I verify a program like the following:

extern int __VERIFIER_nondet_int(void);

extern int __VERIFIER_assert(int);

extern int __VERIFIER_assume(int);

int main(){

   int x=__VERIFIER_nondet_int();

   int y=__VERIFIER_nondet_int();

   __VERIFIER_assume(x!=y);

   __VERIFIER_assert(x==y);

   return 0;

}

Running ./ufo.py prog.c gives the output ERROR unreachable. Can anyone please tell me what am I doing wrong over here?

Thanks and Regards,

Anubhav Sharma.

[Arie Gurfinkel]

I am not sure to what degree UFO supports asserts. In SV_COMP, asserts are explicitly declared as 
void __VERIFIER_assert (int c) { if (!c) ERROR: goto ERROR; }

Depending on the version you are using, assumes might not be supported directly as well. You can implement an assume by

void __VERIFIER_assume (int c) { while (!c) ; }

Note that in both cases, the return type is void.

cheers,

arie

--
You received this message because you are subscribed to the Google Groups "UFO General Discussion Group" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ufo-discuss...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Arie Gurfinkel]

One more thing, you should run ufo-svcomp-par.py NAME.c  . ufo.py is used internally by ufo-svcomp-par.py and requires a number of options to be effective.

cheers,

arie

To unsubscribe from this group and stop receiving emails from it, send an email to ufo-discuss+unsubscribe@googlegroups.com.

[Anubhav Sharma]

Thanks a lot Arie. :)

I have another question. While verifying the following program, I'm not getting any solid answer from ufo. The output says Assertion `!boost::indeterminate(res)' failed. I've attached the output trace along with the program source code.

extern int __VERIFIER_nondet_int(); 

void __VERIFIER_assert (int c) { if (!c) ERROR: goto ERROR; }

void __VERIFIER_assume (int c) { while (!c) ; }

int main(){

   int x;

   int X;

   int sum;

   int SUM;

   __VERIFIER_assume(x==X);

   __VERIFIER_assume(sum==SUM);

   

   int T = X+13;  

   int n = __VERIFIER_nondet_int();

   

   for(int i=0; i<n; i++){

      sum += x+13;

      SUM += T;

   }

   __VERIFIER_assert(sum==SUM);

   return 0;   

}

However, in the above program if I change the initial value of n from a non-deterministic one to a constant, ufo correctly says that ERROR is unreachable. 

What is happening over here?

Thanks and Regards,
Anubhav Sharma