--- layout: fc_discuss_archives title: Message 42 from Frama-C-discuss on May 2013 ---
Hi Kim, First of all, I should point out that the example is fully verified with Fluorine-2 (may be also in Fluorine-1). However, there are several issues with this example. 1. Assigns & Behavior Yes, WP never takes benefit from separate assigns clause when calling functions. Instead, WP consider the assigns clause from default behavior, or the union of all assigns clauses. In your case, you have a default assigns clause, which is taken for reference. 2. Assigns of Invalid l-values In your example, the default assigns is x->a[i], which is potentially not valid when i exceeds the range [0..n-1]. Hopefully, this is not a problem *in theory*, since assigns clause only relates to valid pointers. The meaning of "assigns A" is : "forall all l-value L, is L is valid and separated from A, then value of L is unchanged" Then, whenever 'A' is invalid, "assigns A" has the same meaning as "assigns \nothing". 3. Comparing (x->a) to (y->a) Those values are pointers, not arrays. Actually, the function "foo" never modifies the value of field "a" (nor the value of field "n") of "x". Hence, since you stated that (x->a[...]) is separated from (x), writing to (x->a[i]) never modifies the value of (x->a). The proof should come from the fact that (&(x->a)) is included in the region pointed by (x). Something like : @assert \separated(x,x->a[0..n]) ==> \separated(&(x->a),x->a[0..n]) ; This assertion is easily discharged by Alt-Ergo with Fluorine-2. I don't know how it is handled by Oxygen. 4. Getting rid of assigns in behaviors A general solution is to put an over-approximated assigns clause in the default behavior ; then add ensures clauses to refine case-by-case in behaviors. For instance : { behavior A : assigns x ; behavior B : assigns y ; } Can be translated into : { assigns x,y ; behavior A : ensures y == \old(y) ; behavior B : ensures x == \old(x) ; } ======================================================================== Regards, L. Le 27 mai 2013 ? 15:49, V?llinger, Kim a ?crit : > struct A > { > int n; > int* a; > }; > > typedef struct A A; > > /*@ > requires \valid(x); > requires (x->n >= 0) && \valid(x->a+(0..x->n-1)); > > assigns x->a[i]; > > behavior assign_sth: > assumes 0 <= i < x->n; > assigns x->a[i]; > > behavior assign_nth: > assumes i < 0 || i >= x->n; > assigns \nothing; > > complete behaviors; > disjoint behaviors; > */ > void foo(A* x, int i) > { > if (i >= 0 && i < x->n) > x->a[i] = 0; > } > > /*@ > requires \valid(x); > requires \valid(y); > requires (x->n >= 0) && \valid(x->a+(0..x->n-1)); > requires (y->n >= 0) && \valid(y->a+(0..y->n-1)); > requires \separated(x, y, x->a + (0..x->n-1), y->a + (0..y->n-1)); > */ > void bar(A* x, A* y, int i) > { > foo(x, i); > //@ assert y->a == \at(y->a, Pre); > } -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130528/d551d3eb/attachment.html>