0001729: "char const * const *" causes syntax error

(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

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.

Relationships