--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on October 2014 ---
Hi, I have a problem with assigns clause. Assume the following code: /*@ ensures \result != \null; @ assigns \nothing; @*/ extern int *new_value(); //@ assigns *p; void f(int* p){ *p = 8; } //@ assigns \nothing; int main(void){ int *p = new_value(); f(p); } The prover is unable to prove that main assigns \nothing, which makes sense, as main assigns to *p through function f. However, how should I state that in \assigns clause, since p is local variable and can not be accessed within annotation? Ivan p.s. I repeat the question posted on SO - http://stackoverflow.com/questions/26591694/assigns-clause-for-local-variables-in-frama-c