r13586 Spurious "assert \separated(...)" (csmith)

ID0000832: This issue was created automatically from Mantis Issue 832. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000832	Frama-C	Kernel	public	2011-05-24	2014-02-12

Reporter	pascal	Assigned To	virgile	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C GIT, precise the release id	Target Version	-	Fixed in Version	Frama-C Nitrogen-20111001

Description :

file t.c:

int a, *G;

int g(int x, int y) { return x + y; }

main(int c, char **v){ G = &a; *G = (a < (g((0U || (((a ^ a) <= a) < ((*G) || a))), 5)));

return a; }

$ ~/ppc/bin/toplevel.byte -val -unspecified-access t.c t.c:13:[kernel] warning: Unspecified sequence with side effect: /* <- a G *G */ if (G) { tmp = 1; } else { if (a) { tmp = 1; } else { tmp = 0; } } / <- a a a */

              /*  <-  */
              tmp_0 = g((((a ^ a) <= a) < tmp) != 0,5);
              /* *G <- G a */
              *G = a < tmp_0;

... t.c:13:[kernel] warning: undefined multiple accesses in expression. assert \separated(G,& a); t.c:13:[kernel] warning: undefined multiple accesses in expression. assert \separated(G,G); ...

The program is completely defined, g has no side-effects.