Frama-C Bug Tracking System - Frama-C
View Issue Details
0001837Frama-CPlug-in > E-ACSLpublic2014-07-16 16:582015-06-08 14:22
arvidj 
signoles 
normalminorhave not tried
closedfixed 
 
Frama-C Sodium 
0001837: Literal strings can be added multiple times in memory
Consider the following example: int i = 4; while (i--) { char *s = "toto"; /@ assert \valid(s) ; */ printf(s); } Each time the body of the while-loop is executed, the block corresponding to "toto" is added to the memory store, however this string has always the same address.
No tags attached.
related to 0001636closed signoles E-ACSL: executes "__store_block()" but never "__delete_block()"! 
c bug-1837-literal-strings.c (149) 2014-07-16 18:08
https://bts.frama-c.com/file_download.php?file_id=797&type=bug
Issue History
2014-07-16 16:58arvidjNew Issue
2014-07-16 16:58arvidjStatusnew => assigned
2014-07-16 16:58arvidjAssigned To => signoles
2014-07-16 18:05signolesRelationship addedrelated to 0001636
2014-07-16 18:06signolesStatusassigned => confirmed
2014-07-16 18:08arvidjFile Added: bug-1837-literal-strings.gen.c.out
2014-07-16 18:08arvidjFile Added: bug-1837-literal-strings.c
2014-07-17 00:21yakobowskiFile Deleted: bug-1837-literal-strings.gen.c.out
2015-06-04 18:00signolesNote Added: 0005931
2015-06-04 18:00signolesStatusconfirmed => resolved
2015-06-04 18:00signolesFixed in Version => Frama-C Sodium
2015-06-04 18:00signolesResolutionopen => fixed
2015-06-04 18:01signolesNote Edited: 0005931View Revisions
2015-06-08 14:22signolesStatusresolved => closed

Notes
(0005931)
signoles   
2015-06-04 18:00   
(edited on: 2015-06-04 18:01)
Fixed in upcoming E-ACSL 0.5.