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
- Subject: [Frama-c-discuss] question about a simple example and jessie
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- Date: Fri, 14 May 2010 02:26:17 +0200
- In-reply-to: <4BEC90E9.6050100@cslabs.com>
- References: <4BDF2C15.5010201@cslabs.com> <x2xb15d09071005031421v51333b13ma27dc52ec76a51dc@mail.gmail.com> <4BEC6D3B.8060105@cslabs.com> <AANLkTinfmjfgLL7ywzAXtoyJs3MQ4hxRoc3eFcvRCTOt@mail.gmail.com> <4BEC90E9.6050100@cslabs.com>
> 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
- Follow-Ups:
- [Frama-c-discuss] question about a simple example and jessie
- From: naghmeh.ghafari at cslabs.com (Naghmeh Ghafari)
- [Frama-c-discuss] question about a simple example and jessie
- References:
- [Frama-c-discuss] question about a simple example and jessie
- From: naghmeh.ghafari at cslabs.com (Naghmeh Ghafari)
- [Frama-c-discuss] question about a simple example and jessie
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] question about a simple example and jessie
- From: naghmeh.ghafari at cslabs.com (Naghmeh Ghafari)
- [Frama-c-discuss] question about a simple example and jessie
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] question about a simple example and jessie
- From: naghmeh.ghafari at cslabs.com (Naghmeh Ghafari)
- [Frama-c-discuss] question about a simple example and jessie
- Prev by Date: [Frama-c-discuss] question about a simple example and jessie
- Next by Date: [Frama-c-discuss] question about a simple example and jessie
- Previous by thread: [Frama-c-discuss] question about a simple example and jessie
- Next by thread: [Frama-c-discuss] question about a simple example and jessie
- Index(es):