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