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

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001837Frama-CPlug-in > E-ACSLpublic2014-07-16 16:582015-06-08 14:22
Reporterarvidj 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
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 Filesc file icon bug-1837-literal-strings.c [^] (149 bytes) 2014-07-16 18:08 [Show Content]

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

-  Notes
(0005931)
signoles (manager)
2015-06-04 18:00
edited on: 2015-06-04 18:01

 Fixed in upcoming E-ACSL 0.5.

- 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

Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker