--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on February 2014 ---
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>