--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on July 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C can't detect "Undefined side-effects in expressions"



Hello,

On Mon, Jul 12, 2010 at 12:23 PM, Eric Liu <eric.liu at uniquesoft.com> wrote:

> However, the user manual says Frama-C will produce such
> warning message.
> se.c :5: ... undefined multiple accesses in expression . assert \ s e p
> a r a t e d (& x ,& x);
> se.c :7: ... undefined multiple accesses in expression . assert \ s e p
> a r a t e d (& x,p);

Because the feature is not complete yet, you have to activate it with
the -unspecified-access option. See the caveat in the documentation
regarding function calls and function arguments.

> Here is my test code, called with parameter c = 1.

Note that the second warning that could be emitted (for x and *p) is
not emitted with c=1, because the value of the argument is propagated
inside the function ("context-sensitive" analysis). It is emitted only
when it appears to the analysis that the second bit of c could be set.

With your code and the command-line

frama-c -val myfile.c -unspecified-access

I get:
...
t.c:8:[kernel] warning: undefined multiple accesses in expression.
assert \separated(& x,& x);
...

and if I change the file so that the value of c is not precisely known, I get:

...
t.c:8:[kernel] warning: undefined multiple accesses in expression.
assert \separated(& x,& x);
...
t.c:14:[kernel] warning: undefined multiple accesses in expression.
assert \separated(& x,p);
...

Note that "\separated(& x,& x)" is logically equivalent to "false".
The value analysis could stop the propagation right after emitting
this alarm if it wanted to, and keep propagating only the else branch
of if(c&1). It currently does not detect that.

Similarly, if could reduce p's set of values to {‌{ &t }‌} after line
14, and even reduce the values of c to indicate that c's second bit
must not be set. Again, it currently does not do such sophisticated
reasoning.

Pascal