--- layout: fc_discuss_archives title: Message 89 from Frama-C-discuss on November 2013 ---
Hello, > 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. For now, Alt-Ergo does not provide explicit counterexamples. This feature is on our "todo list" as many users are interested in it. Regards, Mohamed Iguernelala. Senior R&D Engineer, OCamlPro Research Associate, VALS team, LRI. http://www.iguer.info Le 12/11/2013 16:03, David Cok a ?crit : > 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 > > > _______________________________________________ > 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