Frama-C Bug Tracking System - Frama-C | ||||||||||
View Issue Details | ||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | |||||
0000832 | Frama-C | Kernel | public | 2011-05-24 08:24 | 2014-02-12 16:59 | |||||
Reporter | pascal | |||||||||
---|---|---|---|---|---|---|---|---|---|---|
Assigned To | virgile | |||||||||
Priority | normal | Severity | minor | Reproducibility | always | |||||
Status | closed | Resolution | fixed | |||||||
Platform | OS | OS Version | ||||||||
Product Version | Frama-C GIT, precise the release id | |||||||||
Target Version | Fixed in Version | Frama-C Nitrogen-20111001 | ||||||||
Summary | 0000832: r13586 Spurious "assert \separated(...)" (csmith) | |||||||||
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. | |||||||||
Tags | No tags attached. | |||||||||
Relationships |
| |||||||||
Attached Files |
Notes | |||||
|
|||||
|
|
Issue History | |||||
Date Modified | Username | Field | Change | ||
---|---|---|---|---|---|
2011-05-24 08:24 | pascal | New Issue | |||
2011-05-24 08:24 | pascal | Status | new => assigned | ||
2011-05-24 08:24 | pascal | Assigned To | => virgile | ||
2011-05-24 08:25 | pascal | Summary | Spurious "assert \separated(...)" => r13586 Spurious "assert \separated(...)" (csmith) | ||
2011-05-24 08:27 | pascal | Relationship added | related to 0000771 | ||
2011-05-24 08:53 | virgile | Status | assigned => acknowledged | ||
2011-05-24 18:25 | svn | ||||
2011-05-24 18:25 | svn | Status | acknowledged => resolved | ||
2011-05-24 18:25 | svn | Resolution | open => fixed | ||
2011-10-10 14:13 | signoles | Fixed in Version | => Frama-C Nitrogen-20111001 | ||
2011-10-10 14:14 | signoles | Status | resolved => closed | ||
2011-10-21 14:47 | pascal | Status | closed => feedback | ||
2011-10-21 14:47 | pascal | Resolution | fixed => reopened | ||
2011-10-21 14:47 | pascal | Category | Plug-in > value analysis => Kernel | ||
2011-10-21 14:48 | pascal | Status | feedback => closed | ||
2011-10-21 14:48 | pascal | Resolution | reopened => fixed | ||
2013-12-19 01:12 | Source_changeset_attached | => framac master 54758d8a | |||
2014-02-12 16:54 | Source_changeset_attached | => framac stable/neon 54758d8a | |||
2014-02-12 16:59 | Note Added: 0004783 | ||||
2014-02-12 16:59 | Status | closed => resolved |