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] question about a simple example and jessie

> Maybe the prover cannot prove the invariant is wrong, but cannot
> prove it right either.

Previously I meant, as one possible explanation for the post-condition
being proved as well as its negation, for the invariant to be equivalent to
the logical formula "false", that is, to be self-contradictory (I should
have mentioned the possibility that the invariant contradicts the
loop's exit condition, which is another possibility).

This is different from having the wrong invariant, which can prevent
establishing the invariant, or prevent proving a post-condition that should
hold, or allow to prove a post-condition that does not hold, but which
should never, as far as I reckon, allow to prove both a post-condition and
its negation.

Now that I think about it, the invariants on the slides I referenced earlier
do not look like they are contradictory, although it is always hard to be sure
that they are the right invariants.

>> Could you clarify what the diagnostic of each of alt-ergo and CVC3 is
>>
>
> Where can I find this? Is this in the jessie log file? If I run CVC3 and Alt
> Ergo back to back, does it include both results in the log file?

I was only asking whether alt-ergo and CVC3 were both proving the
post-condition, and whether they were both proving its negation.
If they are, we should look in a bug in Frama-C/Jessie/Why. If only
one of them is proving the property and its negation, we'll start
by suspecting a bug in that theorem prover. If you are using
Why's graphical interface, that would be the contents of the
row that corresponds to the post-condition.

Pascal