0001817: Literal strings in global arrays with compound initializers are not correctly initialized

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001817

Frama-C

Plug-in > E-ACSL

public

2014-06-25 09:49

2017-01-18 15:09

Reporter

arvidj

Assigned To

kvorobyov

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Product Version

Frama-C GIT, precise the release id

Target Version

Fixed in Version

Frama-C 14-Silicon

Summary

0001817: Literal strings in global arrays with compound initializers are not correctly initialized

Description

Frama-C GIT Commit: b71d80efb3808c286f1a2f17dbf54bc3909824d0

The generated function for initializing global variables "__e_acsl_memory_init" does not handle arrays containing literal strings with compound intializers.

Example:

char *A[2] = {"foo", "bar"};
int main(void) {
    /*@ assert \valid(A[0]) ; */
    /*@ assert \valid(A[1]) ; */
}

Generated __e_acsl_memory_init:
  void __e_acsl_memory_init(void)
  {
    char *__e_acsl_literal_string;
    __store_block((void *)(A),sizeof(char *[2]));
    __e_acsl_literal_string = "bar";
    __store_block((void *)__e_acsl_literal_string,sizeof("bar"));
    __full_init((void *)__e_acsl_literal_string,sizeof("bar"));
    __literal_string((void *)__e_acsl_literal_string);
    A = (char *)__e_acsl_literal_string;
    return;
  }

The last assignment is incorrect.

Tags

No tags attached.

Attached Files

usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i (351,415 bytes) 2015-11-16 19:17

Relationships

related to

0001636

closed

signoles

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

Relationships

Notes
~0006101 George Karpenkov (reporter) 2015-11-16 19:20	(sorry for uploading a file, I did not realize I can't remove them in Mantis). The issue seems to be more general, and not restricted to arrays. Struct initializers are affected in the same way. See the initial file and the pre-processed version: http://metaworld.me/issues/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i http://metaworld.me/issues/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i.frama.c

~0006103 signoles (manager) 2015-11-17 08:27	Thanks George. You're right. We are investigating it. Your example should help us to debug.

~0006114 George Karpenkov (reporter) 2015-12-08 13:02	Hi, is there any timeline on how long do normally bugs stay in the tracker? I was trying to work with a large-ish dataset, and unfortunately my files are processed in such a way that I'm hitting this bug on almost every single instance.

~0006115 signoles (manager) 2015-12-08 13:18	There is no (public) timeline (except for users with an official support contract). We do our best according to our (limited) manpower, our own priorities and how important/difficult to fix the opened task is. Some issues are unfortunately opened for years, while some others are fixed in a few hours (and available within the next public release which occurs once or twice per year). About this particular bug: I'm happy to say that a fix is about to be merged in our development version and will be part of the next public release (should be in January).

~0006116 signoles (manager) 2015-12-08 13:22	Anyway it is always good to know what issues are critical for any user: it helps us to fix priorities, but we cannot provide any guarantee that we are able to fix each of them quickly.

~0006345 signoles (manager) 2017-01-18 15:09	Fixed in E-ACSL 0.8 compatible with Frama-C Silicon.

Notes

Date Modified	Username	Field	Change
Issue History
2014-06-25 09:49	arvidj	New Issue
2014-06-25 09:49	arvidj	Status	new => assigned
2014-06-25 09:49	arvidj	Assigned To	=> signoles
2014-06-26 15:12	signoles	Status	assigned => confirmed
2014-07-16 18:05	signoles	Relationship added	related to 0001636
2015-10-29 11:30	signoles	Assigned To	signoles => kvorobyov
2015-10-29 11:30	signoles	Status	confirmed => assigned
2015-11-16 19:17	George Karpenkov	File Added: usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i
2015-11-16 19:20	George Karpenkov	Note Added: 0006101
2015-11-17 08:27	signoles	Note Added: 0006103
2015-12-08 13:02	George Karpenkov	Note Added: 0006114
2015-12-08 13:03	signoles	Note View State: 0006114: private
2015-12-08 13:03	signoles	Note View State: 0006114: public
2015-12-08 13:18	signoles	Note Added: 0006115
2015-12-08 13:22	signoles	Note Added: 0006116
2015-12-14 21:49	signoles	Status	assigned => resolved
2015-12-14 21:49	signoles	Resolution	open => fixed
2017-01-18 15:09	signoles	Fixed in Version	=> Frama-C 14-Silicon
2017-01-18 15:09	signoles	Note Added: 0006345
2017-01-18 15:09	signoles	Status	resolved => closed

Issue History