--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on September 2009 ---
Hello Kerstin, Le mer. 09 sept. 2009 10:31:23 CEST, "Kerstin Hartig" <kerstin.hartig at first.fraunhofer.de> a ?crit : > 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. -- Virgile Prevosto Ing?nieur-Chercheur, CEA, LIST Laboratoire de S?ret? des Logiciels +33/0 1 69 08 71 83