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:

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);

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; */
  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 - 2019 MantisBT Team
Powered by Mantis Bugtracker