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. |
| Steps To Reproduce | |
| Additional Information | |
| Tags | No tags attached. |
| Relationships | | related to | 0000771 | closed | virgile | r12436, unnecessary warning for side-effects (csmith) |
|
| Attached Files | |
|
| 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 | Checkin | |
| 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 |
| 2014-02-12 16:59 | | Note Added: 0004783 | |
| 2014-02-12 16:59 | | Status | closed => resolved |