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

[Frama-c-discuss] Behavior specification with ghost variables




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.