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