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