ID0001636: **This issue was created automatically from Mantis Issue 1636. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0001636 | Frama-C | Plug-in > E-ACSL | public | 2014-01-30 | 2015-06-08 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | ThomasJ | **Assigned To** | signoles | **Resolution** | fixed | | **Priority** | normal | **Severity** | major | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | Frama-C Sodium | **Fixed in Version** | Frama-C Sodium | ### Description : 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 ### Steps To Reproduce : E-ACSL translation of: int main(void) { int x = 0; /*@ assert x == 0; */ while(1) { printf("###"); } return 0; }