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: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
  • Date: Mon, 10 Feb 2014 17:49:19 -0500
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>