Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002137Frama-CPlug-in > value analysispublic2015-06-26 13:092017-03-31 20:21
Reporterrcl 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Sodium 
Target VersionFrama-C PhosphorusFixed in Version 
Summary0002137: value analysis introduces weird pointer assert with variable length arrays
DescriptionThe 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 ReproduceRun the value analysis plugin on the attached source code form.
TagsNo tags attached.
Attached Filesc file icon ptrcmp.c [^] (384 bytes) 2015-06-26 13:09 [Show Content]
c file icon ptrcmp.2.c [^] (468 bytes) 2015-07-17 09:28 [Show Content]

- Relationships

-  Notes
(0005943)
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
(0005983)
rcl (reporter)
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

(0006191)
yakobowski (manager)
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.

(0006392)
yakobowski (manager)
2017-03-31 20:21

alloca will be properly handled in Phosphorus.

- Issue History
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 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


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker