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] Question about assigns-clauses and calling function

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>