| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001636 | Frama-C | Plug-in > E-ACSL | public | 2014-01-30 13:28 | 2015-06-08 14:23 | ||||
| Reporter | ThomasJ | ||||||||
| Assigned To | signoles | ||||||||
| Priority | normal | Severity | major | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Fluorine-20130601 | ||||||||
| Target Version | Frama-C Sodium | Fixed in Version | Frama-C Sodium | ||||||
| Summary | 0001636: E-ACSL: executes "__store_block()" but never "__delete_block()"! | ||||||||
| 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; } | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|||||||||||
|
|||||||||||
 Relationships |
| 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 Last edited: 2015-06-04 18:01 |
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 |