--- layout: fc_discuss_archives title: Message 44 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"



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