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

  • Subject: [Frama-c-discuss] Question about assigns-clauses and calling function
  • From: kim.voellinger at fokus.fraunhofer.de (Völlinger, Kim)
  • Date: Mon, 27 May 2013 13:49:34 +0000
Dear all,

the following example simplifies an issue we have encountered while verifying
a simple stack data structure with WP/Alt-Ergo/Coq under Oxygen.

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);
}

The example consists of a struct A,
a function foo and a function bar which calls foo.
The struct A contains an array and its length.

If i is a valid index, then the function foo sets the ith element of the
array to 0. Otherwise foo does nothing.
The specification of foo expresses this in two named behaviors.

The bar function is called on two pointers to A-objects
for which we require separateness.
For bar we want to verify that after calling foo on the A-pointer x,
the array address y->a remains unchanged.
The corresponding assertion is neither proven automatically
nor can we discharge it with Coq.

We assume the problem is that the function bar only sees the
assigns-clause outside of the two named behaviors of foo.
Thus, when exploiting in Coq the separation-clause we are unable to use
the more specific assigns-clauses of the named behaviors.

Do you have any suggestions how to verify this assertion or
to reformulate the contract of foo?
Do you recommend to also report this issue on Frama-C BTS?

Best regards,
Kim
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130527/cd4f80c2/attachment.html>