View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002137 | Frama-C | Plug-in > Eva | public | 2015-06-26 13:09 | 2017-06-15 15:56 | ||||
Reporter | rcl | ||||||||
Assigned To | yakobowski | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Sodium | ||||||||
Target Version | Frama-C 15-Phosphorus | Fixed in Version | Frama-C 15-Phosphorus | ||||||
Summary | 0002137: value analysis introduces weird pointer assert with variable length arrays | ||||||||
Description | The value analysis plugin generates an assertion of the form /*@ assert Value: ptr_comparison: \pointer_comparable((void *)*(arr+0), (void *)val); */ when arr is a VLA. This assertion looks bogus; it doesn't make any sense and doesn't even type check. | ||||||||
Steps To Reproduce | Run the value analysis plugin on the attached source code form. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
jens (reporter) 2015-06-26 20:21 |
- please add the exact command line with which you called Frama-C - also your file contains an explicit (and probably unnecessary) reference to your local Frama-C installation. - the remarks in your source are in German |
rcl (reporter) 2015-07-17 09:27 Last edited: 2015-07-17 09:29 |
I'm sorry for not answering until now. Attached is an updated version of the source file that addresses your issues. Please invoke Frama-C like this on the source file: frama-c-gui -val ptrcmp.2.c |
yakobowski (manager) 2016-05-31 19:20 Last edited: 2016-05-31 19:21 |
The modelization of alloca is/was broken (or, more to the point non-existent). This will be corrected in Frama-C Silicium. |
yakobowski (manager) 2017-03-31 20:21 |
alloca will be properly handled in Phosphorus. |
maroneze (administrator) 2017-06-15 15:55 |
Just for clarification, here's the current situation: - alloca is not handled in Frama-C 15 Phosphorus; - however, VLAs are, and their usage leads to a syntactic transformation that inserts calls to __fc_vla_alloc/__fc_vla_free. Option -val-builtins-list shows that __fc_vla_alloc is mapped to the builtin Frama_C_vla_alloc_by_stack, and __fc_vla_free is mapped to Frama_C_vla_free. These builtins should ensure correct handling of VLAs. In the example, with Frama-C 15 Phosphorus we have a definitive alarm about accessing the uninitialized array element, but no more \pointer_comparable. So the reported issue has been fixed. Note that, unfortunately, using __fc_vla_alloc leads to a warning about "Neither code nor specification for function __fc_vla_alloc, generating default assigns from the prototype". This should be handled in the next Frama-C release. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2015-06-26 13:09 | rcl | New Issue | |
2015-06-26 13:09 | rcl | Status | new => assigned |
2015-06-26 13:09 | rcl | Assigned To | => yakobowski |
2015-06-26 13:09 | rcl | File Added: ptrcmp.c | |
2015-06-26 20:21 | jens | Note Added: 0005943 | |
2015-07-17 09:27 | rcl | Note Added: 0005983 | |
2015-07-17 09:28 | rcl | File Added: ptrcmp.2.c | |
2015-07-17 09:29 | rcl | Note Edited: 0005983 | View Revisions |
2016-05-31 19:20 | yakobowski | Note Added: 0006191 | |
2016-05-31 19:21 | yakobowski | Note Edited: 0006191 | View Revisions |
2017-03-06 11:35 | yakobowski | Target Version | => Frama-C 15-Phosphorus |
2017-03-31 20:21 | yakobowski | Note Added: 0006392 | |
2017-03-31 20:21 | yakobowski | Status | assigned => resolved |
2017-03-31 20:21 | yakobowski | Resolution | open => fixed |
2017-05-31 19:04 | signoles | Fixed in Version | => Frama-C 15-Phosphorus |
2017-05-31 19:05 | signoles | Status | resolved => closed |
2017-06-15 15:55 | maroneze | Note Added: 0006414 | |
2017-06-15 15:55 | maroneze | Status | closed => resolved |
2017-06-15 15:56 | maroneze | Status | resolved => closed |
2018-01-12 14:26 | signoles | Category | Plug-in > value analysis => Plug-in > Eva |