--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on October 2014 ---
The only way to handle your situation, is to make the result of new_value accessible from the logic space. For instance : //@ logic int * R ; //@ ensures \result == R && \valid(R) ; assigns \nothing ; extern int *new_value(); //@ assigns *p; void f(int * p) { ? } //@ assigns *R ; int main(void) { ? } A more general solution would be to have a set if pointer for R, instead of a unique one. L. Le 31 oct. 2014 ? 16:09, gavran at mpi-sws.org a ?crit : > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss