Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001729Frama-CKernelpublic2014-04-03 16:252015-03-17 22:17
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Platformxubuntu-cfe13.10OSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in VersionFrama-C Sodium 
Summary0001729: "char const * const *" causes syntax error
Descriptionaaa.c:3:[kernel] user error: unexpected token '*'
TagsNo tags attached.
Attached Filesc file icon aaa.c [^] (89 bytes) 2014-04-03 16:25 [Show Content]

- Relationships

-  Notes
(0005026)
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));
(0005039)
virgile (developer)
2014-04-10 11:46

Fix committed to feature/bugfix-1729 branch.
(0005040)
virgile (developer)
2014-04-10 11:47

Fix committed to feature/bugfix-1729 branch.
(0005041)
virgile (developer)
2014-04-10 12:01

Fix committed to feature/bugfix-1729 branch.
(0005099)
virgile (developer)
2014-05-16 10:23

Fix committed to master branch.

- 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 Note Added: 0005039
2014-04-10 11:46 virgile Resolution open => fixed
2014-04-10 11:47 virgile Note Added: 0005040
2014-04-10 12:01 virgile Note Added: 0005041
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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker