2021-01-15 15:18 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001729Frama-CKernelpublic2015-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 Files
  • c file icon aaa.c (89 bytes) 2014-04-03 16:25 -
    static void elem_size(void) {
    	//@ assert \valid_read((char const * const *)0);
    }
    
    
    c file icon aaa.c (89 bytes) 2014-04-03 16:25 +

-Relationships
+Relationships

-Notes

~0005026

Jochen (reporter)

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)

Fix committed to feature/bugfix-1729 branch.

~0005040

virgile (developer)

Fix committed to feature/bugfix-1729 branch.

~0005041

virgile (developer)

Fix committed to feature/bugfix-1729 branch.

~0005099

virgile (developer)

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