--- layout: fc_discuss_archives title: Message 85 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



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