Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

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 - 2019 MantisBT Team
Powered by Mantis Bugtracker