2021-03-03 03:50 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001837Frama-CPlug-in > E-ACSLpublic2015-06-08 14:22
Reporterarvidj 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
Product Version 
Target VersionFixed in VersionFrama-C Sodium 
Summary0001837: Literal strings can be added multiple times in memory
DescriptionConsider 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.
TagsNo tags attached.
Attached Files

-Relationships
related to 0001636closedsignoles E-ACSL: executes "__store_block()" but never "__delete_block()"! 
+Relationships

-Notes

~0005931

signoles (manager)

Last edited: 2015-06-04 18:01

View 2 revisions

Fixed in upcoming E-ACSL 0.5.

+Notes

-Issue History
Date Modified Username Field Change
2014-07-16 16:58 arvidj New Issue
2014-07-16 16:58 arvidj Status new => assigned
2014-07-16 16:58 arvidj Assigned To => signoles
2014-07-16 18:05 signoles Relationship added related to 0001636
2014-07-16 18:06 signoles Status assigned => confirmed
2014-07-16 18:08 arvidj File Added: bug-1837-literal-strings.gen.c.out
2014-07-16 18:08 arvidj File Added: bug-1837-literal-strings.c
2014-07-17 00:21 yakobowski File Deleted: bug-1837-literal-strings.gen.c.out
2015-06-04 18:00 signoles Note Added: 0005931
2015-06-04 18:00 signoles Status confirmed => resolved
2015-06-04 18:00 signoles Fixed in Version => Frama-C Sodium
2015-06-04 18:00 signoles Resolution open => fixed
2015-06-04 18:01 signoles Note Edited: 0005931 View Revisions
2015-06-08 14:22 signoles Status resolved => closed
+Issue History