Option "-lib-entry" results misses possible values of function pointers
ID0002254: This issue was created automatically from Mantis Issue 2254. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002254 | Frama-C | Plug-in > Eva | public | 2016-11-07 | 2017-12-17 |
| Reporter | Jochen | Assigned To | maroneze | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | xubuntu | OS Version | - |
| Product Version | Frama-C Aluminium | Target Version | - | Fixed in Version | - |
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.