--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on February 2009 ---
Le lun 16 f?v 2009 10:38:28 CET, "Christoph Weber" <Christoph.Weber at first.fraunhofer.de> a ?crit : > From what I understood of the recent mails, it is difficult to read and write on the same memory location and to prove something about it. > (Please correct me if I am wrong) This is not exactly true. the jessie plugin does not have any issue proving something about a location which is both read and written, as long as it knows precisely which locations are written and which aren't. Trouble arises when it (or the underlying theorem provers) can't decide if a given location has still its old value or has just been assigned a new one, for instance when you write to t[i] and read from t[k] without knowing whether i and k are equal or distinct. > /*@ > loop invariant 0 <= i <= length; > > loop invariant \forall integer k; 0 <= k < i ==> > (\at(a[k],Pre) == old_value ==> > a[k] == new_value); > */ > for (; i != length; ++i) > { > if (a[i] == old_value) > { > a[i] = new_value; > } > } > } You don't specify enough the effect of a loop step: from your invariant, we know what happens to the cell whose initial value is old_value, but nothing more. We have to tell the jessie plugin that the other cells are left untouched. There are two ways to do that - the simplest one is unfortunately not supported by the plugin yet: loop assigns a[i]; indicates in ACSL that at each step, only a[i] might be modified - we must thus add an invariant saying that all the cells beyond i still have their initial value: loop invariant \forall integer k; i <= k < length ==> a[k] == (\at[k],Pre); Best regards, -- E tutto per oggi, a la prossima volta. Virgile