--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on October 2015 ---
Hello Claude, > On 05 Oct 2015, at 17:51, Claude Marche <Claude.Marche at inria.fr> wrote: > > Well, the post-condition would follow from the loop invariant, if the > other loop invariant start <= i < end was given. Ah, yes, thatâs definitely missing. > In any case, the loop invariant is not preserved, its preservation > should not be reported to hold by WP. > > I checked with Jessie, the loop invariant is not proved to be preserved. Thatâs what I would have expected, yes. > By the way, Christoph, are you sure your file contains nothing else than > what you sent in your first mail? Because if there is something > inconsistent in the context, then everything will be reported as valid > by the provers. Yes, I just double-checked. What I just noticed, though, is that the erroneous behaviour seems to be triggered only in the presence of `-wp-invariantsâ as a command line argument. Might this be the culprit and I shouldnât be using this switch at all? -- Christoph