--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on July 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C/Jessie: not_assigns and mutable parameter



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