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] RE : New Version of "ACSL by Example" for Frama-C Fluorine

Hi,

I don't know why these two ensures of validity are present in the specification.
But here are few remarks about these questions.

Actually, the ensures clause for pointer validity in swap are proved by WP. So it is not incorrect to add them in the spec. The separation of p and *p, or from p and &p, or any such weird separations are implied by the memory model of WP, and the WP checks that all pointers remain well-typed in a program, unless you choose a weaker (but unsafe) memory model.

Moreover, the two validity ensures are also not necessary to prove, for instance, this short program:

/*@
  requires \valid(x) && \valid(y);
*/
void foo(int *x,int *y)
{
  swap(x,y);
  swap(x,y);
  //@ assert VALID: \valid(x);
}

During the second call to swap, the requires pre-conditions are obtained from the requires of [foo] even after the side effects of the first call to swap.

However, it is sometimes useful, in larger example, to have additional ensures, for SMT solvers to not re-invent facts that are provable as consequences of callee. This can be seen as short cuts or additional lemmas.

A similar situation occurs for assigns. Even if an assigns clause imply some equalities, it is often necessary to add them explicitly in ensure clauses to help SMT solvers at call sites. Of course, these topics are subject to continuous improvements in WP.

Another tip, for the function [foo] above, in current version of WP, it is not possible to prove the expected specification "assigns \nothing;" because of the WP strategy used to prove assigns (it is sound, but incomplete). Instead, you should specify side-effects of function [foo] above with :
/*@
  ensures *x == \old(*x);
  ensures *y == \old(*y);
  assigns *x,*y ;
*/
Which is semantically equivalent to "assigns \nothing;", but remains provable by WP.
I agree, we may improve a bit user experience in such cases for future versions.

L.



________________________________
De : frama-c-discuss-bounces at lists.gforge.inria.fr [frama-c-discuss-bounces at lists.gforge.inria.fr] de la part de Pascal Cuoq [pascal.cuoq at gmail.com]
Date d'envoi : samedi 14 d?cembre 2013 11:34
? : Frama-C public discussion
Objet : Re: [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/20131216/090207f1/attachment.html>