View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001907 | Frama-C | Plug-in > Eva | public | 2014-08-08 14:17 | 2015-03-17 22:18 | ||||
Reporter | Anne | ||||||||
Assigned To | yakobowski | ||||||||
Priority | normal | Severity | minor | Reproducibility | have not tried | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | |||||||||
Target Version | Fixed in Version | Frama-C Sodium | |||||||
Summary | 0001907: Value abort because of Zero-sized location | ||||||||
Description | Value usually support structure types holding an array field with an undefined size, but in the attached case, it aborts with: user error: Zero-sized location S_buf[0].chunk (type 'int []'). Probably empty struct. Aborting * Notice that the size of `buf` is defined since it is only a pointer. * If `buf` is defined instead of just declared `extern`, the problem disappear. | ||||||||
Steps To Reproduce | $ frama-c -val struct.c | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
yakobowski (manager) 2014-08-08 14:25 |
Thank. I was probably a bit over-zealous in fixing 1874, and will look into this. No guarantee, as this is a flexible member array, that are more or less unsupported by Value at the moment. |
Anne (reporter) 2014-08-08 14:32 |
I have many of those in the application I am analyzing, and it is usually working pretty well... except this external variable problem. |
yakobowski (manager) 2014-08-08 14:35 |
Because this is one is external, it is treated as if -lib-entry was enabled. In this mode, we fail when trying to feel the unknown size array. |
yakobowski (manager) 2014-08-10 21:27 |
Fix committed to master branch. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2014-08-08 14:17 | Anne | New Issue | |
2014-08-08 14:17 | Anne | Status | new => assigned |
2014-08-08 14:17 | Anne | Assigned To | => yakobowski |
2014-08-08 14:17 | Anne | File Added: struct.c | |
2014-08-08 14:25 | yakobowski | Note Added: 0005401 | |
2014-08-08 14:32 | Anne | Note Added: 0005402 | |
2014-08-08 14:35 | yakobowski | Note Added: 0005403 | |
2014-08-10 21:27 | yakobowski | Source_changeset_attached | => framac master c8dfa50c |
2014-08-10 21:27 | yakobowski | Note Added: 0005405 | |
2014-08-10 21:27 | yakobowski | Status | assigned => resolved |
2014-08-10 21:27 | yakobowski | Resolution | open => fixed |
2015-01-28 18:08 | Lau | Tag Attached: struct | |
2015-01-28 18:08 | Lau | Tag Detached: struct | |
2015-03-17 22:17 | signoles | Fixed in Version | => Frama-C Sodium |
2015-03-17 22:18 | signoles | Status | resolved => closed |
2018-01-12 14:26 | signoles | Category | Plug-in > value analysis => Plug-in > Eva |