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: Patrick.Baudin at cea.fr (BAUDIN Patrick)
  • Date: Tue, 11 Feb 2014 08:33:51 +0100
  • In-reply-to: <B517F47C2F6D914AA8121201F9EBEE6701C7660449BC@Mail1.FCMD.local>
  • References: <B517F47C2F6D914AA8121201F9EBEE6701C7660449BC@Mail1.FCMD.local>
Hi,
Yes, when a property isn't proved, the validation of the others is not 
sure because their proof can rely on the validity of that property.
Patrick.

Le 10/02/2014 23:49, Dharmalingam Ganesan a ?crit :
> 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.
>
> 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...
>
> Any comments?
>
> frama-c-gui -pp-annot -lib-entry -wp -wp-rte conn_disconn_2.c
>
>
> Thanks,
> Dharma
>