Frama-C Bug Tracking System - Frama-C
View Issue Details
0001636Frama-CPlug-in > E-ACSLpublic2014-01-30 13:282015-06-08 14:23
Frama-C Fluorine-20130601 
Frama-C SodiumFrama-C Sodium 
0001636: E-ACSL: executes "__store_block()" but never "__delete_block()"!
E-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
E-ACSL translation of: int main(void) { int x = 0; /*@ assert x == 0; */ while(1) { printf("###"); } return 0; }
No tags attached.
related to 0001817closed kvorobyov Literal strings in global arrays with compound initializers are not correctly initialized 
related to 0001837closed signoles Literal strings can be added multiple times in memory 
Issue History
2014-01-30 13:28ThomasJNew Issue
2014-01-30 13:28ThomasJStatusnew => assigned
2014-01-30 13:28ThomasJAssigned To => signoles
2014-01-30 17:57signolesStatusassigned => confirmed
2014-01-31 16:11signolesNote Added: 0004477
2014-01-31 16:13signolesNote Added: 0004478
2014-07-16 18:05signolesRelationship addedrelated to 0001817
2014-07-16 18:05signolesRelationship addedrelated to 0001837
2015-06-04 18:00signolesNote Added: 0005930
2015-06-04 18:00signolesStatusconfirmed => resolved
2015-06-04 18:00signolesResolutionopen => fixed
2015-06-04 18:00signolesTarget Version => Frama-C Sodium
2015-06-04 18:01signolesNote Edited: 0005930View Revisions
2015-06-08 14:23signolesStatusresolved => closed
2015-06-08 14:23signolesFixed in Version => Frama-C Sodium

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...
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.
2015-06-04 18:00   
(edited on: 2015-06-04 18:01)
Fixed in upcoming E-ACSL 0.5.