[Eva] New file engine/function_calls to decide how to analyze a function.
Function [define_analysis_target] decides whether a builtin, the specification or the definition is used for the analysis of a given C function, according to Eva parameters. This function is then used in compute_functions.ml. [define_analysis_target] also decides whether the resulting states of an analysis should be saved, according to [-eva-results] parameters. Finally, [define_analysis_target] registers analyzed function calls in tables, with the caller/callsite and the defined analysis status.
Showing
- Makefile 2 additions, 1 deletionMakefile
- src/plugins/value/engine/compute_functions.ml 143 additions, 138 deletionssrc/plugins/value/engine/compute_functions.ml
- src/plugins/value/engine/function_calls.ml 128 additions, 0 deletionssrc/plugins/value/engine/function_calls.ml
- src/plugins/value/engine/function_calls.mli 37 additions, 0 deletionssrc/plugins/value/engine/function_calls.mli
- tests/value/oracle/recursion.0.res.oracle 7 additions, 0 deletionstests/value/oracle/recursion.0.res.oracle
Loading
Please register or sign in to comment