--- layout: fc_discuss_archives title: Message 79 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] counterexamples through Frama-C WP



Hello,

2013/11/11 David Cok <dcok at grammatech.com>:
> Just in  case I'm missing something, can someone more familiar with WP point
> me to the appropriate options or confirm that reporting counterexample
> information is a feature yet to be implemented?

That should be -wp-unsat-model (see WP manual, p. 21).

On following C code:
"""
/*@ ensures \result <= 10;
 */
int main(int c)
{
  return c + 1;
}
"""

"frama-c -wp -wp-unsat-model q16_counter-example.c" gives:

"""
------------------------------------------------------------
--- Model for Post-condition (file q16_counter-example.c, line 1) in 'main' :
------------------------------------------------------------
File "/tmp/wpdffc13.dir/typed/main_post_Alt-Ergo.mlw", line 230,
characters 1-89:I don't know

Model

Propositional:
  is_sint32(main_0) = true
  main_0 > 10
  main_0 <= (2147483648 - 1)
  -2147483648 <= main_0

Theory:
 is_sint32(main_0) = FT:[true]

Relation:
 main_0 ? [11;2147483647]
"""

I'm not sure how to correctly interpret Alt-Ergo output though. ;-)

Best regards,
david