diff --git a/src/plugins/value/domains/traces/traces_domain.ml b/src/plugins/value/domains/traces/traces_domain.ml index 4fc0009eba456fb968eb7f2c9428f4b825d66b88..494dfa232bbb2f4a0bd578772b2f198eb7f2a662 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 ef1a267c67ba5a89cab305aaf16454b84676cd2c..46dbf6914143d8ce4a9e635e415625c124c58fb5 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 f6db93a3ebd8ad8ae09db5bc3c2b55cf9193b689..540ebda343404e2712eb3a5b7b9efe3e18b7a3fb 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