--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on February 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP: requires doubt



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
>