--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on December 2013 ---
Hello, Jens and authors of ?ACSL by Example?. I am a little bit surprised by a recent (according to the changelog) change in the contract of function swap(): /*@ requires \valid(p); requires \valid(q); assigns *p; assigns *q; ensures \valid(p); ensures \valid(q); // HERE ensures *p == \old(*q); ensures *q == \old(*p); */ void swap(int* p, int* q); This ?ensures? clause should never be useful (see below). If you found that it helped in order to prove properties about callers of swap(), that would arguably be a bug in Frama-C or a serious misfeature in the automatic prover(s) involved. Someone, somewhere either in the developers of Frama-C or the developers of these automatic provers would be interested in the reasons that lead you to add this postcondition. Pascal ____________ The clause ?\valid(p);? (p being a formal parameter) should not be useful for a couple of reasons: - Even if p and w were, say, global variables, the requires clauses says that the pointers are valid, and the assigns clause says that they are not modified. Well, not modified-ish. If p and q were global variables, you would be in trouble if one pointed to the other, but the weakest precondition plug-in you are using is probably implicitly assuming that this does not happen anyway. As written in ACSL by Example's section 6.2.2, the swap() function does not implement the contract without this assumption. A C function that implements the contract in all cases is trivial to write (left as exercise to the reader), or the contract could be augmented with something like ?requires \separated(*p, q) && \separated(p, *q);? - Regardless, p and q are formal arguments to the function swap() here, so the C piece of code that could make one point to the other does not exist. Similarly, any change that the function swap() itself could make to p or q would be invisible to the caller, because variables p an q go out of scope before the caller could observe any change to them. - for this reason, formal parameters in post-conditions, such as p and q in all of swap()'s preconditions, are desugared by Frama-C's front-end into \old(p) and \old(q). This is the only thing that the author can possibly have meant: $ cat /tmp/t.c /*@ requires \valid(p); requires \valid(q); assigns *p; assigns *q; ensures \valid(p); ensures \valid(q); ensures *p == \old(*q); ensures *q == \old(*p); */ void swap(int* p, int* q); $ frama-c -print /tmp/t.c [kernel] preprocessing with "gcc -C -E -I. /tmp/t.c" /* Generated by Frama-C */ /*@ requires \valid(p); requires \valid(q); ensures \valid(\old(p)); ensures \valid(\old(q)); ensures *\old(p) ? \old(*q); ensures *\old(q) ? \old(*p); assigns *p, *q; */ extern void swap(int *p, int *q); Note that on the other hand, *p in a precondition is desugared in *\old(p) and that \old(*p) is not automatically the same as *\old(p). -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131214/bf73d7a7/attachment-0001.html>