2021-03-05 02:15 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001636Frama-CPlug-in > E-ACSLpublic2015-06-08 14:23
Assigned Tosignoles 
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

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 



signoles (manager)

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)

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)

Last edited: 2015-06-04 18:01

View 2 revisions

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
+Issue History