--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on February 2014 ---
On 10/02/2014 23:49, Dharmalingam Ganesan wrote: > 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. For elaborating on what Patrick Baudin said. WP says valid because the call to the duplicate connect is invalid. Indeed if you remove the duplicate connect, the call to the duplicate disconnect becomes orange. > > 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... I'm going to suppose that violated means there is a trace that doesn't verify the precondition and invalid means any trace doesn't verify the precondition. It is not always the case. WP always add the precondition of preceding calls in the hypothesis of proof obligation. But in this particular case the hypothesis is invalid and then any subsequent proof obligation is valid. You can see that in the po of the duplicate disconnect and the previous disconnect the hypothesis is false (-wp-no-let will show you the context not simplified). You can remove the ensures in order to see that all the call except the first are orange. To sum up, it is because there is _no_ trace that verify the preconditions and postconditions that all the subsequent calls, which are dead code, are proved. -- Fran?ois Bobot