Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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