Frama-C Bug Tracking System - Frama-C
View Issue Details
0002137Frama-CPlug-in > Evapublic2015-06-26 13:092017-06-15 15:56
Frama-C Sodium 
Frama-C 15-PhosphorusFrama-C 15-Phosphorus 
0002137: value analysis introduces weird pointer assert with variable length arrays
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.
Run the value analysis plugin on the attached source code form.
No tags attached.
c ptrcmp.c (384) 2015-06-26 13:09
c ptrcmp.2.c (468) 2015-07-17 09:28
Issue History
2015-06-26 13:09rclNew Issue
2015-06-26 13:09rclStatusnew => assigned
2015-06-26 13:09rclAssigned To => yakobowski
2015-06-26 13:09rclFile Added: ptrcmp.c
2015-06-26 20:21jensNote Added: 0005943
2015-07-17 09:27rclNote Added: 0005983
2015-07-17 09:28rclFile Added: ptrcmp.2.c
2015-07-17 09:29rclNote Edited: 0005983View Revisions
2016-05-31 19:20yakobowskiNote Added: 0006191
2016-05-31 19:21yakobowskiNote Edited: 0006191View Revisions
2017-03-06 11:35yakobowskiTarget Version => Frama-C 15-Phosphorus
2017-03-31 20:21yakobowskiNote Added: 0006392
2017-03-31 20:21yakobowskiStatusassigned => resolved
2017-03-31 20:21yakobowskiResolutionopen => fixed
2017-05-31 19:04signolesFixed in Version => Frama-C 15-Phosphorus
2017-05-31 19:05signolesStatusresolved => closed
2017-06-15 15:55maronezeNote Added: 0006414
2017-06-15 15:55maronezeStatusclosed => resolved
2017-06-15 15:56maronezeStatusresolved => closed
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

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
2015-07-17 09:27   
(edited on: 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
2016-05-31 19:20   
(edited on: 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.
2017-03-31 20:21   
alloca will be properly handled in Phosphorus.
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.