--- layout: fc_discuss_archives title: Message 18 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,

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


-------------- next part --------------
A non-text attachment was scrubbed...
Name: conn_disconn_2.c
Type: text/x-csrc
Size: 522 bytes
Desc: conn_disconn_2.c
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140210/f744cd9a/attachment-0001.c>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: disconnect_all_green
Type: application/octet-stream
Size: 83424 bytes
Desc: disconnect_all_green
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140210/f744cd9a/attachment-0001.obj>