--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on September 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie - problem with an example



Hello Virgile,

it really solved the problem. Especially the indentation remark was a
helpful advice.
As indentation is not recognized but the mentioned ensures clause should be
valid for all behaviors I now placed it before the behavior clauses. 
 
Thank you,
Kerstin


> >     behavior yes:
> >       assumes data->a <= data->b + 10; 
> >       assigns data->b;
> >     ensures data->b <= data->a;
> >  */
> > void refresh(struct MyData* data)

> I guess your issue lies here: there is no post-condition saying that
> data->b is positive. We only know that it is less than or equal to
> data->a (By the way, your indentation is a bit misleading: the ensures
> relates only to the behavior 'yes', not to all behaviors).
> It is thus not possible to conclude that data->b is positive in the
> main loop after the call to refresh. Remember that function calls are
> seen as some kind of black box and that the only things which are known
> outside of the function body are the clauses of the contract.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/ms-tnef
Size: 3213 bytes
Desc: not available
Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090909/e048fd62/attachment.bin