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] Frama-C/Jessie: not_assigns and mutable parameter
- Subject: [Frama-c-discuss] Frama-C/Jessie: not_assigns and mutable parameter
- From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
- Date: Wed, 15 Jul 2009 17:05:31 +0200
Hello, Please, what is wrong with this annotated code for which the default behavior post-condition PO can not be discharged by Jessie/Why/ATPs (a mutable_p var seems to be unexploitable in the hypotheses): /*@ requires \valid(p) && \valid(q); assigns *\at(p,Post),p; */ int main1(int* p,int* q) { p = q; *p = 1; return 1; } For information, a previous example of the same kind but with a structure field was totally discharged (after a change in Jessie to take into account Post label): typedef struct { int * rc; } S; /*@ requires \valid(p) && \valid(p->rc) && \valid(r); assigns *\at(p->rc,Post),p->rc; */ int main2(S* p,int* r) { p->rc = r; *(p->rc) = 1; return 1;} Is there any trouble with basic C types in assigns clause? Thanks in advance for your help, Dillon
- Follow-Ups:
- [Frama-c-discuss] Frama-C/Jessie: not_assigns and mutable parameter
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] Frama-C/Jessie: not_assigns and mutable parameter
- Prev by Date: [Frama-c-discuss] How to compil Frama-C with an existing Why installation
- Next by Date: [Frama-c-discuss] Frama-C/Jessie: not_assigns and mutable parameter
- Previous by thread: [Frama-c-discuss] How to compil Frama-C with an existing Why installation
- Next by thread: [Frama-c-discuss] Frama-C/Jessie: not_assigns and mutable parameter
- Index(es):