Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002254Frama-CPlug-in > Evapublic2016-11-07 15:332017-12-17 21:26
ReporterJochen 
Assigned Tomaroneze 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSxubuntuOS Version
Product VersionFrama-C Aluminium 
Target VersionFixed in Version 
Summary0002254: Option "-lib-entry" results misses possible values of function pointers
Description(I posed this question also on frama-c-discuss on 3 Nov 2016, 16:20, and received a reply from David Mentré on 5 Nov 2016, 15:52. The advice to use an invariant and increase the slevel originates from Julien Signoles.)

Running "frama-c -val -main foo -lib-entry -slevel 10 fctptr.c" on the attached program results in an output of:
  a ∈ [--..--]
  fct ∈ {0}
While option "-lib-entry" behaves on the int variable "a" as described in the value analysis manual (sect.5.2.3, p.58), it seems to have no effect on the function pointer variable "fct". Moreover, the latter is analyzed to contain a null pointer, while it actually never does, due to its initialization at the declaration. Instead, since "fct" is declared "static", I'd expect the analysis to report:
  a ∈ [--..--]
  fct ∈ {{ &f1, &f2 }}

When "-lib-entry" is omitted, Frama-C's analysis coincides with mine:
  a ∈ {1}
  fct ∈ {{ &f1 }}

Both with and without option "-lib-entry", Frama-C's results don't change when the invariant is removed. To sum up, it seems that the use of option "-lib-entry" inhibits information from call analysis, but also from explicit invariants.
TagsNo tags attached.
Attached Filesc file icon fctptr.c [^] (384 bytes) 2016-11-07 15:33 [Show Content]

- Relationships

-  Notes
(0006490)
yakobowski (manager)
2017-12-17 21:26

Apologies, I somehow missed this issue. (As well as the discussion.)

The -lib-entry option suffers from some limitations. In particular, global invariants, or the preconditions of main, are not used to build the initial state. But the behavior you observe is too surprising. We should probably emit a warning when we limit a function pointer to NULL.

Even better, we should generate as initial value for a function pointer of type T the set of all known functions with a type compatible with T, plus NULL. This would increase range of programs that can be soundly analyzed with -lib-entry.

- Issue History
Date Modified Username Field Change
2016-11-07 15:33 Jochen New Issue
2016-11-07 15:33 Jochen Status new => assigned
2016-11-07 15:33 Jochen Assigned To => yakobowski
2016-11-07 15:33 Jochen File Added: fctptr.c
2017-12-17 21:26 yakobowski Note Added: 0006490
2017-12-17 21:26 yakobowski Assigned To yakobowski => maroneze
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker