--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on December 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Is there any difference between "assigns \result \from \nothing" and "assigns \nothing"



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