--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on April 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Internal state represented by ghost variable not provable



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.