Frama-C Bug Tracking System - Frama-C
View Issue Details
0002254Frama-CPlug-in > Evapublic2016-11-07 15:332017-12-17 21:26
Jochen 
maroneze 
normalminoralways
assignedopen 
xubuntu
Frama-C Aluminium 
 
0002254: Option "-lib-entry" results misses possible values of function pointers
(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.
No tags attached.
c fctptr.c (384) 2016-11-07 15:33
https://bts.frama-c.com/file_download.php?file_id=1123&type=bug
Issue History
2016-11-07 15:33JochenNew Issue
2016-11-07 15:33JochenStatusnew => assigned
2016-11-07 15:33JochenAssigned To => yakobowski
2016-11-07 15:33JochenFile Added: fctptr.c
2017-12-17 21:26yakobowskiNote Added: 0006490
2017-12-17 21:26yakobowskiAssigned Toyakobowski => maroneze
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0006490)
yakobowski   
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.