Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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