Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001817Frama-CPlug-in > E-ACSLpublic2014-06-25 09:492017-01-18 15:09
Reporterarvidj 
Assigned Tokvorobyov 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C 14-Silicon 
Summary0001817: Literal strings in global arrays with compound initializers are not correctly initialized
DescriptionFrama-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.



TagsNo tags attached.
Attached Files? file icon 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 0001636closedsignoles E-ACSL: executes "__store_block()" but never "__delete_block()"! 

-  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.

- Issue History
Date Modified Username Field Change
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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker