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