Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] New Version of "ACSL by Example" for Frama-C Fluorine

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>