--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on October 2015 ---
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