Frama-C Bug Tracking System - Frama-C
View Issue Details
0001817Frama-CPlug-in > E-ACSLpublic2014-06-25 09:492017-01-18 15:09
arvidj 
kvorobyov 
normalminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C 14-Silicon 
0001817: Literal strings in global arrays with compound initializers are not correctly initialized
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.
No tags attached.
related to 0001636closed signoles E-ACSL: executes "__store_block()" but never "__delete_block()"! 
? usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i (351,415) 2015-11-16 19:17
https://bts.frama-c.com/file_download.php?file_id=1072&type=bug
Issue History
2014-06-25 09:49arvidjNew Issue
2014-06-25 09:49arvidjStatusnew => assigned
2014-06-25 09:49arvidjAssigned To => signoles
2014-06-26 15:12signolesStatusassigned => confirmed
2014-07-16 18:05signolesRelationship addedrelated to 0001636
2015-10-29 11:30signolesAssigned Tosignoles => kvorobyov
2015-10-29 11:30signolesStatusconfirmed => assigned
2015-11-16 19:17George KarpenkovFile Added: usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i
2015-11-16 19:20George KarpenkovNote Added: 0006101
2015-11-17 08:27signolesNote Added: 0006103
2015-12-08 13:02George KarpenkovNote Added: 0006114
2015-12-08 13:03signolesNote View State: 0006114: private
2015-12-08 13:03signolesNote View State: 0006114: public
2015-12-08 13:18signolesNote Added: 0006115
2015-12-08 13:22signolesNote Added: 0006116
2015-12-14 21:49signolesStatusassigned => resolved
2015-12-14 21:49signolesResolutionopen => fixed
2017-01-18 15:09signolesFixed in Version => Frama-C 14-Silicon
2017-01-18 15:09signolesNote Added: 0006345
2017-01-18 15:09signolesStatusresolved => closed

Notes
(0006101)
George Karpenkov   
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   
2015-11-17 08:27   
Thanks George. You're right. We are investigating it. Your example should help us to debug.
(0006114)
George Karpenkov   
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   
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   
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   
2017-01-18 15:09   
Fixed in E-ACSL 0.8 compatible with Frama-C Silicon.