--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on October 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP plugin report incorrect



Hello,

The option -wp-invariants is an experimental feature of WP trying to 
prove ACSL "invariant" clause holding inside a loop body as "loop 
invariant" clause.
It seems that there is something wrong with that option.
Since you have no such "invariant" clause, don't use it.

Patrick.

Le 05/10/2015 18:31, Christoph Rauch a écrit :
> Hi David,
>
>> On 05 Oct 2015, at 18:02, David MENTRE <dmentre at linux-france.org> wrote:
>>
>> Le 05/10/2015 17:56, Christoph Rauch a écrit :
>>> If I completely remove the loop and thus the invariant, it doesn’t verify. How can it possibly prove the loop invariant?
>> Which prover are you using? I tried with Alt-Ergo and CVC3 and the loop invariant in not proved, for both your first code and the code not calling swap().
> Using `-wp-invariants’, which seems to be the cause for the troubles, every prover I tried yields positive (i.e. wrong) results: Alt-Ergo, CVC4, and Z3.
>
> Best,
> Christoph
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss


-- 
Patrick Baudin, DILS/LSL, Bât. 862,
Point Courrier n° 174
Institut CARNOT CEA LIST,
CEA Saclay Nano-INNOV,
91191 Gif-sur-Yvette cedex, France.
tel: +33 (0)1 6908 2072