Skip to content

Recursive calls in value analysis

ID0002185: This issue was created automatically from Mantis Issue 2185. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0002185 Frama-C Plug-in > Eva public 2015-11-03 2015-12-04
Reporter lammyday Assigned To yakobowski Resolution won't fix
Priority normal Severity minor Reproducibility always
Platform - OS Linux OS Version ubuntu 13.04
Product Version - Target Version - Fixed in Version -

Description :

Frama-c pdg could not generate pdg graphs for program containing recursive calls.

Additional Information :

See implicit.c file here: http://git.savannah.gnu.org/cgit/make.git/tree/implicit.c?id=2860d3b247e70a34246936fb085aeec951ea49b1

you can download the full GNU make version repository here:

http://git.savannah.gnu.org/cgit/make.git/commit/?id=2860d3b247e70a34246936fb085aeec951ea49b1

Steps To Reproduce :

Running "frama-c -pdg -dot-pdg graph -pdg-print implicit.i -main pattern_search" for the GNU make version repository 2860d3b2 gives the following errors:

implicit.c:700:[value] warning: recursive call during value analysis (pattern_search <- pattern_search) Use -val-ignore-recursive-calls to ignore (beware this will make the analysis unsound) [kernel] State_builder.aborted because of unimplemented feature. Please send a feature request at http://bts.frama-c.com with: 'recursive calls in value analysis'

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information