--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on November 2014 ---
Thanks for the answer. However, upon verifying it, I get wp failure: Address of logic value (L_R). Which plugin did you use to prove it? Ivan off question: what is prefered way communication? Should I continue discussion on the mailing list or on Stack Overflow? > 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 > > _______________________________________________ > 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 >