Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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.