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



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