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>
- Follow-Ups:
- [Frama-c-discuss] WP: requires doubt
- From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
- [Frama-c-discuss] WP: requires doubt
- From: francois.bobot at cea.fr (François Bobot)
- [Frama-c-discuss] WP: requires doubt
- Prev by Date: [Frama-c-discuss] WP: Predicate not taking constraints from requires?
- Next by Date: [Frama-c-discuss] WP: Predicate not taking constraints from requires?
- Previous by thread: [Frama-c-discuss] WP: Predicate not taking constraints from requires?
- Next by thread: [Frama-c-discuss] WP: requires doubt
- Index(es):