| 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 |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
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. |
| Notes |
| Issue History |
|||
| 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 |
| Issue History |