2020-12-05 00:43 CET

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

-Notes

~0004477

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...

~0004478

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.

~0005930

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