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"

  • Subject: [Frama-c-discuss] Frama-C can't detect "Undefined side-effects in expressions"
  • From: eric.liu at uniquesoft.com (Eric Liu)
  • Date: Mon, 12 Jul 2010 18:23:15 +0800
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