| Anonymous | Login | Signup for a new account | 2020-04-06 12:50 CEST |  |
| Main | My View | View Issues | Change Log | Roadmap | Repositories |
| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | 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 | ||||||
| Platform | OS | OS Version | |||||||
| 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 |
||||||
|
||||||
 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 |
|
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 |
|
Issue History |
| Copyright © 2000 - 2020 MantisBT Team |
|