--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on December 2013 ---
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