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

[Frama-c-discuss] difference between specifying side effects for value analysis in two different ways



On Sun, Dec 08, 2013 at 11:26:58PM +0000, David Yang wrote:
> For function:
> int f(int *p);
> 
> specifying the side effects of function f by two different ways:
> 
> 1. /*@ assings *p; */ only assign *p
> 2. /*@ assigns *p; assigns p;*/ assign the address p would also be
> changed at the same time

p is a local variable of f;
if the implementation of f assigns p, this is not
a side effect visible to the caller.
(The actual parameter of f might not even be a variable,
 as for example in  f(q + 1).
)


Wolfram