Values of the counter-example

[Anubhav Sharma]

Hello,

How do I see the values of variables in a counterexample found by UFO?
For e.g. in the following program, for what values of x and n, the assertion fails?

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 = __VERIFIER_nondet_int(); 

   int n = __VERIFIER_nondet_int(); 

   __VERIFIER_assume(n>=0);

   __VERIFIER_assert(x+n>x);

   return 0;

}

Thanks,

Anubhav.

[Arie Gurfinkel]

There is no easy way to see the values of source variables.
UFO applies many transformations including compiler optimizations. The verification is done only at the lowest level.

The standard counterexample will include values of llvm registers. You can also look at the last bitcode file produced by the front-end.

This is usually enough for me to manually understand the counterexample. Unfortunately, there is no automation of this process at the moment.

One useful technique is to add extra tests in the source program and observe their results based on the path of the counterexample.

--
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.