0001636: E-ACSL: executes "__store_block()" but never "__delete_block()"!

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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

Platform

OS Version

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

related to	0001817	closed	kvorobyov	Literal strings in global arrays with compound initializers are not correctly initialized
related to	0001837	closed	signoles	Literal strings can be added multiple times in memory

Notes
(0004477) 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...

(0004478) 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.

(0005930) signoles (manager) 2015-06-04 18:00 edited on: 2015-06-04 18:01	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