--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on September 2009 ---
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