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



Dear all,

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

I am using "-val-use-spec f"  to do the value analysis.

Is there any difference while doing value analysis by specifying the
side effects with these two different ways?

Thank you very much.

All the best.
-david