--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on April 2014 ---
Le 27/04/2014 20:58, Frank Dordowsky a ?crit : > When I try to prove this with the wp plugin, all assertions are > proven, but not the post conditions of the two ensure clauses in the > behavior clauses. What is the reason for that? I think it is because the 'assumes' properties refer to the pre-state, and we don't know anything about the initial value of 'inp', while your assertions refer to 'inp' at the end of the function. What about a post-condition like : ((inp >= 0 ) && (\result == 'p')) || ((inp < 0 ) && (\result == 'n')); Hope this helps, Anne.