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>
- Follow-Ups:
- [Frama-c-discuss] Question about assigns-clauses and calling function
- From: loic.correnson at cea.fr (Loïc Correnson)
- [Frama-c-discuss] Question about assigns-clauses and calling function
- Prev by Date: [Frama-c-discuss] Announce: simple concurrency analysis plugin
- Next by Date: [Frama-c-discuss] Set global variables uninitialized at Value analysis start
- Previous by thread: [Frama-c-discuss] Fix for inductive predicate
- Next by thread: [Frama-c-discuss] Question about assigns-clauses and calling function
- Index(es):