--- layout: fc_discuss_archives title: Message 79 from Frama-C-discuss on November 2013 ---
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