View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001729 | Frama-C | Kernel | public | 2014-04-03 16:25 | 2015-03-17 22:17 | ||||
Reporter | Jochen | ||||||||
Assigned To | virgile | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Platform | xubuntu-cfe13.10 | OS | OS Version | ||||||
Product Version | Frama-C Neon-20140301 | ||||||||
Target Version | Fixed in Version | Frama-C Sodium | |||||||
Summary | 0001729: "char const * const *" causes syntax error | ||||||||
Description | aaa.c:3:[kernel] user error: unexpected token '*' | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
Jochen (reporter) 2014-04-03 16:46 |
The original code seemed to stem from FRAMA-C normalization before value-analysis of some C program: 12343 /*@ assert 12344 Value: mem_access: 12345 \valid_read((char const * const *)namespaces->elts+i); 12346 */ 12347 /*@ assert 12348 Value: initialisation: 12349 \initialized((char const * const *)namespaces->elts+i); 12350 */ 12351 tmp_8_unroll_1579 = strlen(*((char const * const *)namespaces->elts + i)); |
virgile (developer) 2014-04-10 11:46 |
Fix committed to feature/bugfix-1729 branch. |
virgile (developer) 2014-04-10 11:47 |
Fix committed to feature/bugfix-1729 branch. |
virgile (developer) 2014-04-10 12:01 |
Fix committed to feature/bugfix-1729 branch. |
virgile (developer) 2014-05-16 10:23 |
Fix committed to master branch. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2014-04-03 16:25 | Jochen | New Issue | |
2014-04-03 16:25 | Jochen | File Added: aaa.c | |
2014-04-03 16:46 | Jochen | Note Added: 0005026 | |
2014-04-07 13:46 | signoles | Assigned To | => virgile |
2014-04-07 13:46 | signoles | Status | new => assigned |
2014-04-10 09:44 | virgile | Status | assigned => acknowledged |
2014-04-10 11:46 | virgile | Source_changeset_attached | => framac feature/bugfix-1729 b37133ed |
2014-04-10 11:46 | virgile | Note Added: 0005039 | |
2014-04-10 11:46 | virgile | Resolution | open => fixed |
2014-04-10 11:47 | virgile | Source_changeset_attached | => framac feature/bugfix-1729 38012497 |
2014-04-10 11:47 | virgile | Note Added: 0005040 | |
2014-04-10 12:01 | virgile | Source_changeset_attached | => framac feature/bugfix-1729 e8f6892b |
2014-04-10 12:01 | virgile | Note Added: 0005041 | |
2014-05-16 10:23 | virgile | Source_changeset_attached | => framac master e8f6892b |
2014-05-16 10:23 | virgile | Note Added: 0005099 | |
2014-05-16 10:27 | virgile | Status | acknowledged => resolved |
2015-03-17 22:17 | signoles | Fixed in Version | => Frama-C Sodium |
2015-03-17 22:17 | signoles | Status | resolved => closed |