Skip to content
Snippets Groups Projects
Commit 921f957e authored by David Bühler's avatar David Bühler
Browse files

[Eva] Moves and renames [no_memoization_enabled] as [partial_results].

From Mark_noresults to Function_calls.
parent e711d912
No related branches found
No related tags found
No related merge requests found
......@@ -1623,7 +1623,7 @@ module Make
Self.abort ~current:true
"Calls through function pointers are not supported without the cvalue \
domain.";
if Mark_noresults.no_memoization_enabled () then
if Function_calls.partial_results () then
Self.abort ~current:true
"Function pointer evaluates to anything. Try deactivating \
option(s) -eva-no-results and -eva-no-results-function."
......
......@@ -26,6 +26,12 @@ open Eval
let save_results f =
Parameters.ResultsAll.get () && not (Parameters.NoResultsFunctions.mem f)
(* Signal that some results are not stored. The gui or some API calls
may fail ungracefully. *)
let partial_results () =
not (Parameters.ResultsAll.get ()) ||
not (Parameters.NoResultsFunctions.is_empty ())
let info name : (module State_builder.Info_with_size) =
(module struct
......
......@@ -25,6 +25,10 @@ open Cil_types
(** True if the results should be saved for the given function. *)
val save_results: fundec -> bool
(** True if some results are not stored due to options -eva-no-results
or -eva-no-results-function. *)
val partial_results: unit -> bool
(** What is used for the analysis of a given function:
- a Cvalue builtin (and other domains use the specification)
- the function specification
......
......@@ -43,7 +43,7 @@ module UsedVarState =
let used_var = UsedVarState.memo
(fun var ->
Mark_noresults.no_memoization_enabled () ||
Function_calls.partial_results () ||
try
let f = fst (Globals.entry_point ()) in
let inputs = !Db.Inputs.get_external f in
......
......@@ -29,13 +29,6 @@ let () = Db.Value.no_results :=
(fun fd -> not (should_memorize_function fd)
|| not (Parameters.Domains.mem "cvalue"))
(* Signal that some results are not stored. The gui, or some calls to
Db.Value, may fail ungracefully *)
let no_memoization_enabled () =
not (Parameters.ResultsAll.get ()) ||
not (Parameters.NoResultsFunctions.is_empty ())
(*
Local Variables:
......
......@@ -22,6 +22,3 @@
(** Are the states of the function analysis saved? *)
val should_memorize_function: Cil_types.fundec -> bool
(** Signal that some analysis results are not stored. *)
val no_memoization_enabled: unit -> bool
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment