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: requires doubt
- Subject: [Frama-c-discuss] WP: requires doubt
- From: francois.bobot at cea.fr (François Bobot)
- Date: Tue, 11 Feb 2014 10:31:53 +0100
- In-reply-to: <B517F47C2F6D914AA8121201F9EBEE6701C7660449BC@Mail1.FCMD.local>
- References: <B517F47C2F6D914AA8121201F9EBEE6701C7660449BC@Mail1.FCMD.local>
On 10/02/2014 23:49, Dharmalingam Ganesan wrote: > Hi, > > For this attached simple program that captures connect and disconnect, I wonder why the client function has all green except for the duplicate connect. > > The requires for disconnect is indeed violated in the client function but WP says valid. For elaborating on what Patrick Baudin said. WP says valid because the call to the duplicate connect is invalid. Indeed if you remove the duplicate connect, the call to the duplicate disconnect becomes orange. > > Is it the case that if one of the preconditions is violated the rest of the validation is considered valid by default, little strange. I'm missing something... I'm going to suppose that violated means there is a trace that doesn't verify the precondition and invalid means any trace doesn't verify the precondition. It is not always the case. WP always add the precondition of preceding calls in the hypothesis of proof obligation. But in this particular case the hypothesis is invalid and then any subsequent proof obligation is valid. You can see that in the po of the duplicate disconnect and the previous disconnect the hypothesis is false (-wp-no-let will show you the context not simplified). You can remove the ensures in order to see that all the call except the first are orange. To sum up, it is because there is _no_ trace that verify the preconditions and postconditions that all the subsequent calls, which are dead code, are proved. -- Fran?ois Bobot
- Follow-Ups:
- [Frama-c-discuss] verification of enum safety
- From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
- [Frama-c-discuss] verification of enum safety
- References:
- [Frama-c-discuss] WP: requires doubt
- From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
- [Frama-c-discuss] WP: requires doubt
- Prev by Date: [Frama-c-discuss] WP: requires doubt
- Next by Date: [Frama-c-discuss] How to re-run command-line analyses?
- Previous by thread: [Frama-c-discuss] WP: requires doubt
- Next by thread: [Frama-c-discuss] verification of enum safety
- Index(es):