--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on December 2013 ---
Dear Boris, Thanks a lot. As I don't know whether result is depend on the environment. I will write assign \result \from \nothing; for value analysis for convenient. On 14 December 2013 19:26, Boris Yakobowski <boris at yakobowski.org> wrote: > Hi, > > There are no differences between form 2 and 3. In fact, the next > version of Frama-C will display them in the same way. > > Form 1 is however different. It is transformed into 2 clauses: > - an 'assigns' clause "assigns \result", that says that the function > does not modify the memory, except for the pseudo-location > corresponding to the return code > - a 'from' clause "assigns \result \from \nothing", that (roughly) > indicates that the value that is being returned does not depend on the > environment (global variables, or formal parameters). In fact, such a > clause implies that the return code is a constant. > > HTH, > > On Sat, Dec 14, 2013 at 2:52 PM, David Yang <abiao.yang at gmail.com> wrote: >> Dear all >> >> I have function "func" called by "main" function, In order to do value >> analysis : >> int func(void); >> >> What I want to know is whether there is any difference by assigns >> these two clauses for the function : >> 1. assigns \result \from \nothing; >> 2. assigns \nothing; >> 3. assigns \result; >> >> >> Thanks. >> >> -david >> >> _______________________________________________ >> 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 > > > > -- > Boris > > _______________________________________________ > 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