From ce82e6dbdd1274e7610850c7190eb317243f291d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Sun, 1 Oct 2017 01:18:07 +0200
Subject: [PATCH] [Eva] (traces) rename API
---
src/plugins/value/domains/traces/traces_domain.ml | 2 +-
src/plugins/value/domains/traces/traces_domain.mli | 2 +-
src/plugins/value/register.ml | 10 +++++-----
3 files changed, 7 insertions(+), 7 deletions(-)
diff --git a/src/plugins/value/domains/traces/traces_domain.ml b/src/plugins/value/domains/traces/traces_domain.ml
index 4fc0009eba4..494dfa232bb 100644
--- a/src/plugins/value/domains/traces/traces_domain.ml
+++ b/src/plugins/value/domains/traces/traces_domain.ml
@@ -712,7 +712,7 @@ let project_of_cfg vreturn s =
-let print_last_traces () =
+let finish_computation () =
let return_stmt = Kernel_function.find_return (fst (Globals.entry_point ())) in
let return_exp = match return_stmt.Cil_types.skind with
| Cil_types.Return (oexp,_) -> oexp
diff --git a/src/plugins/value/domains/traces/traces_domain.mli b/src/plugins/value/domains/traces/traces_domain.mli
index ef1a267c67b..46dbf691414 100644
--- a/src/plugins/value/domains/traces/traces_domain.mli
+++ b/src/plugins/value/domains/traces/traces_domain.mli
@@ -55,4 +55,4 @@ module D: Abstract_domain.Internal
and type location = Precise_locs.precise_location
and type state = state
-val print_last_traces: unit -> unit
+val finish_computation: unit -> unit
diff --git a/src/plugins/value/register.ml b/src/plugins/value/register.ml
index f6db93a3ebd..540ebda3434 100644
--- a/src/plugins/value/register.ml
+++ b/src/plugins/value/register.ml
@@ -36,11 +36,11 @@ let () = Value_parameters.ForceValues.set_output_dependencies [Db.Value.self]
let main () =
(* Value computations *)
- if Value_parameters.ForceValues.get () then !Db.Value.compute ();
- if Db.Value.is_computed () then Red_statuses.report ();
- if Value_parameters.TracesDomain.get () then begin
- Traces_domain.print_last_traces ()
- end
+ if Value_parameters.ForceValues.get () then begin
+ !Db.Value.compute ();
+ Traces_domain.finish_computation ()
+ end;
+ if Db.Value.is_computed () then Red_statuses.report ()
let () = Db.Main.extend main
--
GitLab