--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on October 2014 ---
As said others before, your contract on main() is not valid. As the name "new_value" suggests, do you expect that this function returns a freshly allocated pointer? In that case, your contract should reflect this. Here is a possible specification. Notice also that your initial ensures "\result != \null" is not enough to guarantee that the resulting pointer is \valid /*@ assigns \nothing; @ allocates \result; @ ensures \valid(\result) && \fresh(\result,sizeof(int*)); @*/ extern int *new_value(); /*@ requires \valid(p); @ assigns *p; @*/ void f(int* p){ *p = 8; } /*@ assigns \nothing; @*/ int main(void){ int *p = new_value(); f(p); } Side note: the allocates clause might not be well supported by plugins WP and Jessie. With Jessie, such a code triggers an error, unless you add the pragma #pragma SeparationPolicy(none) (this is a known bug of the separation analysis in presence of dynamic allocation) - Claude On 10/31/2014 04:09 PM, gavran at mpi-sws.org wrote: > 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 >