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.