--- layout: fc_discuss_archives title: Message 85 from Frama-C-discuss on November 2013 ---
Thanks - I did know about this option. As your example shows, it provides a model for when the postcondition (in this case) is false, which is definitely useful in some contexts. I was looking for a concrete counterexample (specific values for all relevant variables) of when it is false, which would require solving these inequalities for specific values. - David On 11/12/2013 3:44 AM, David MENTRE wrote: > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss