--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on July 2009 ---
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