--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on April 2014 ---
Hi, The problem is that you want for instance to prove: ensures no_btn_press == \old(no_btn_press) + 1; \old(no_btn_press) refers to no_btn_press when calling the function. Then, you immediately do : //@ ghost no_btn_press = presscnt; So now, there is no relation between \old(no_btn_press) and the current value of no_btn_press. I think that what you want is rather : //@ assert no_btn_press == presscnt; at that point. With this assertion, you will be able to prove everything, but this assertion since it depend on the calling context (nothing tells that no_btn_press is not modified elsewhere...). Hope this helps, Anne.