Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001636Frama-CPlug-in > E-ACSLpublic2014-01-30 13:282015-06-08 14:23
Assigned Tosignoles 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFrama-C SodiumFixed in VersionFrama-C Sodium 
Summary0001636: E-ACSL: executes "__store_block()" but never "__delete_block()"!
DescriptionE-ACSL translation of a simple printf like: printf("###"); results in the following code: char *__e_acsl_literal_string; __e_acsl_literal_string = "###"; __store_block((void *)__e_acsl_literal_string,sizeof("###")); __full_init((void *)__e_acsl_literal_string); __literal_string((void *)__e_acsl_literal_string); printf(__e_acsl_literal_string); The "__store_block()" function allocates memory, but there is no "__delete_block()" function in order to deallocate the memory! Consider a periodic execution of printf()... On my ARM processor with 1024KByte Flash and 160KByte RAM, this malloc without free will end up in the following error: "assertion "new_leaf != NULL" failed: file "e-acsl/memory_model/e_acsl_bittree.c", line 256, function: __add_element" malloc without free! :O
Steps To ReproduceE-ACSL translation of: int main(void) { int x = 0; /*@ assert x == 0; */ while(1) { printf("###"); } return 0; }
TagsNo tags attached.
Attached Files

- Relationships
related to 0001817closedkvorobyov Literal strings in global arrays with compound initializers are not correctly initialized 
related to 0001837closedsignoles Literal strings can be added multiple times in memory 

-  Notes
signoles (manager)
2014-01-31 16:11

After investigation, there is no simple fix to this bug. Just adding a "delete_block" at the end of the block containing the literal string does solve this issue, but may introduce RTE when verifying properties over strings. Safe solution: - add a pre-analysis to detect literal strings - allocate/initialize the corresponding generated variables at the beginning of the main - use them when the literal strings are used - deallocate them at the end of the main. That requires to fully re-implement the way of handling literal strings in the compilation scheme...
signoles (manager)
2014-01-31 16:13

Additional info: the absence of "delete_block" corresponding to "store_block" only occurs for literal strings. It should not appear for other constructs.
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-01-30 13:28 ThomasJ New Issue
2014-01-30 13:28 ThomasJ Status new => assigned
2014-01-30 13:28 ThomasJ Assigned To => signoles
2014-01-30 17:57 signoles Status assigned => confirmed
2014-01-31 16:11 signoles Note Added: 0004477
2014-01-31 16:13 signoles Note Added: 0004478
2014-07-16 18:05 signoles Relationship added related to 0001817
2014-07-16 18:05 signoles Relationship added related to 0001837
2015-06-04 18:00 signoles Note Added: 0005930
2015-06-04 18:00 signoles Status confirmed => resolved
2015-06-04 18:00 signoles Resolution open => fixed
2015-06-04 18:00 signoles Target Version => Frama-C Sodium
2015-06-04 18:01 signoles Note Edited: 0005930 View Revisions
2015-06-08 14:23 signoles Status resolved => closed
2015-06-08 14:23 signoles Fixed in Version => Frama-C Sodium

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker