--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on July 2010 ---
Hi, Frama-C folks: I am using Frama-C Boron-20100401 on Ubuntu 10.04. When I am trying "Undefined side-effects in expressions" feature, I find Frama-C does not complain it. 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); Here is my test code, called with parameter c = 1. void UnspecifiedSideEffectInExpression(int c) { int x = 0, y = 0, z = 20, t = 30, *p, *q; if (c & 1) { x = c; y = (x++) + (x++); } printf("x = %d, y = %d\n", x, y); p = c&2 ? &x : &t; printf("*p = %d\n", *p); y = *p + x++; printf("y = %d\n", y); q = c&4 ? &z : &t; printf("*q = %d\n", *q); y = *q + x++; printf("x= %d, y = %d, z = %d, t = %d\n", x, y, z, t); } int main() { UnspecifiedSideEffectInExpression(1); return 0; } Can anyone point me out why I can't get the warning message. My command line is "frama-c -val myfile.c". Thanks Eric