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

> 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