--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on July 2010 ---
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