--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on November 2014 ---
Thank you for the answer, Clauude. Yes, "new_value" is my attempt to mimic malloc (I abstracted the details out). Reason why I started doing it in the first place was that WP displayed the warning: "warning: Allocable, Freeable, Valid_read, Fresh and Initialized not yet implemented". As it is under "experimental" section in ACSL documentation, I concluded it is just not yet implemented. (I have problems with Jessie, it crashes and I still don't get why, so I couldn't try with it.). Which prover do you use? (that supports those "experimental" features) > > 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 >> > _______________________________________________ > 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 >