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