|View Issue Details|
|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|
|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|
\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.|
- 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
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
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.
|alloca will be properly handled in Phosphorus.|
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.
|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|