diff --git a/src/plugins/value/domains/traces/traces_domain.ml b/src/plugins/value/domains/traces/traces_domain.ml
index c5e1f29a9c3969c37a7e4cb3d94d9c5d2135525d..dde1607f54371381e3966af014a4e08109a7dbd5 100644
--- a/src/plugins/value/domains/traces/traces_domain.ml
+++ b/src/plugins/value/domains/traces/traces_domain.ml
@@ -1087,8 +1087,6 @@ module Internal = struct
end
-module D = Domain_builder.Complete (Internal)
-
let dummy_loc = Location.unknown
let subst_in_full var_mapping =
@@ -1327,28 +1325,31 @@ let output_dot filename state =
GraphDot.output_graph out (complete_graph (snd (Traces.get_current state)));
close_out out
-
-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
- | _ -> assert false in
- let state = D.Store.get_stmt_state ~after:true return_stmt in
- let header fmt = Format.fprintf fmt "Trace domains:" in
- let body = Bottom.pretty Traces.pretty in
- Value_parameters.printf ~dkey:Internal.log_category ~header " @[%a@]" body state;
- if Value_parameters.TracesProject.get () ||
- not (Value_parameters.TracesDot.is_default ()) then
- match state with
- | `Bottom ->
- Value_parameters.failure "The trace is Bottom can't generate code"
- | `Value state when state ==Traces.top ->
- Value_parameters.failure "The trace is TOP can't generate code"
- | `Value state ->
- if not (Value_parameters.TracesDot.is_default ())
- then output_dot (Value_parameters.TracesDot.get ()) state;
- if Value_parameters.TracesProject.get ()
- then project_of_cfg return_exp state
+module D = struct
+ include Internal
+ module Store = Domain_store.Make(Internal)
+
+ let post_analysis state =
+ 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
+ | _ -> assert false in
+ let header fmt = Format.fprintf fmt "Trace domains:" in
+ let body = Bottom.pretty Traces.pretty in
+ Value_parameters.printf ~dkey:Internal.log_category ~header " @[%a@]" body state;
+ if Value_parameters.TracesProject.get () ||
+ not (Value_parameters.TracesDot.is_default ()) then
+ match state with
+ | `Bottom ->
+ Value_parameters.failure "The trace is Bottom can't generate code"
+ | `Value state when state ==Traces.top ->
+ Value_parameters.failure "The trace is TOP can't generate code"
+ | `Value state ->
+ if not (Value_parameters.TracesDot.is_default ())
+ then output_dot (Value_parameters.TracesDot.get ()) state;
+ if Value_parameters.TracesProject.get ()
+ then project_of_cfg return_exp state
+end
(*
diff --git a/src/plugins/value/domains/traces/traces_domain.mli b/src/plugins/value/domains/traces/traces_domain.mli
index 02d986afe83d6ad5d65ee168b54e578cff20cfca..7a3ee6fce2c11ce77d23ebb8ded732154b1aa4d6 100644
--- a/src/plugins/value/domains/traces/traces_domain.mli
+++ b/src/plugins/value/domains/traces/traces_domain.mli
@@ -60,5 +60,3 @@ module D: Abstract_domain.Internal
with type value = Cvalue.V.t
and type location = Precise_locs.precise_location
and type state = state
-
-val finish_computation: unit -> unit
diff --git a/src/plugins/value/register.ml b/src/plugins/value/register.ml
index b4ccc156516e3e0cfb9053233f72e2db1c9be09f..b7198f212195417767e50c26497c272c0026b8c5 100644
--- a/src/plugins/value/register.ml
+++ b/src/plugins/value/register.ml
@@ -36,11 +36,7 @@ let () = Value_parameters.ForceValues.set_output_dependencies [Db.Value.self]
let main () =
(* Value computations *)
- if Value_parameters.ForceValues.get () then begin
- !Db.Value.compute ();
- if Value_parameters.TracesDomain.get () then
- Traces_domain.finish_computation ()
- end;
+ if Value_parameters.ForceValues.get () then !Db.Value.compute ();
if Db.Value.is_computed () then Red_statuses.report ()
let () = Db.Main.extend main
diff --git a/tests/value/traces/oracle/test1.err.oracle b/tests/value/traces/oracle/test1.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/tests/value/traces/oracle/test1.res.oracle b/tests/value/traces/oracle/test1.res.oracle
index 011f6645879b2f33794ba38f1a6e4aff01c49281..4f8d20b4edd5ef89a733ef48ea8940de161b45be 100644
--- a/tests/value/traces/oracle/test1.res.oracle
+++ b/tests/value/traces/oracle/test1.res.oracle
@@ -60,7 +60,9 @@ c -> 5
42 -> Assign: g = tmp -> 45
43 -> Assign: g = tmp -> 44
44 -> join -> 46
- 45 -> join -> 46 ]} at 46
+ 45 -> join -> 46
+ 46 -> EnterScope: \result<main> -> 47
+ 47 -> Assign: \result<main> = tmp -> 48 ]} at 48
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
@@ -119,7 +121,11 @@ int main(int c)
i ++;
/*@ assert ¬(i < 3); */
g = tmp;
- __traces_domain_return = tmp;
+ {
+ int _result_main_;
+ _result_main_ = tmp;
+ __traces_domain_return = tmp;
+ }
}
}
else {
@@ -138,7 +144,11 @@ int main(int c)
i ++;
/*@ assert ¬(i < 3); */
g = tmp;
- __traces_domain_return = tmp;
+ {
+ int _result_main_;
+ _result_main_ = tmp;
+ __traces_domain_return = tmp;
+ }
}
}
}
diff --git a/tests/value/traces/oracle/test2.err.oracle b/tests/value/traces/oracle/test2.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/tests/value/traces/oracle/test2.res.oracle b/tests/value/traces/oracle/test2.res.oracle
index 963ee92ec44b1f6a9de50e1a4d8d4929ce75452e..f86140502f69964568d9a673a99ab4b1f1d76402 100644
--- a/tests/value/traces/oracle/test2.res.oracle
+++ b/tests/value/traces/oracle/test2.res.oracle
@@ -79,7 +79,9 @@ c -> 1
75 -> finalize_call: loop -> 76
76 -> Assign: tmp = \result<loop> -> 77
77 -> LeaveScope: \result<loop> -> 78
- 78 -> join -> 79 ]} at 79
+ 78 -> join -> 79
+ 79 -> EnterScope: \result<main> -> 80
+ 80 -> Assign: \result<main> = tmp -> 81 ]} at 81
[from] Computing for function loop
[from] Done for function loop
[from] Computing for function main
@@ -137,7 +139,11 @@ int main(int c)
int _result_loop_;
_result_loop_ = j;
tmp = _result_loop_;
- __traces_domain_return = tmp;
+ {
+ int _result_main_;
+ _result_main_ = tmp;
+ __traces_domain_return = tmp;
+ }
}
}
}
@@ -164,7 +170,11 @@ int main(int c)
int _result_loop_;
_result_loop_ = j;
tmp = _result_loop_;
- __traces_domain_return = tmp;
+ {
+ int _result_main_;
+ _result_main_ = tmp;
+ __traces_domain_return = tmp;
+ }
}
}
}
diff --git a/tests/value/traces/oracle/test3.err.oracle b/tests/value/traces/oracle/test3.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/tests/value/traces/oracle/test3.res.oracle b/tests/value/traces/oracle/test3.res.oracle
index f773988a12d52fc2da93b1de8d6c5128169f9529..d99315838e92aad39c6e71fdddf12bbbf71b6085 100644
--- a/tests/value/traces/oracle/test3.res.oracle
+++ b/tests/value/traces/oracle/test3.res.oracle
@@ -22,7 +22,9 @@ c -> 2
5 -> Assign: tmp = 4 -> 6
6 -> Assume: tmp true -> 7
7 -> Assign: g = tmp -> 8
- 8 -> Assign: __retres = g + 1 -> 9 ]} at 9
+ 8 -> Assign: __retres = g + 1 -> 9
+ 9 -> EnterScope: \result<main> -> 10
+ 10 -> Assign: \result<main> = __retres -> 11 ]} at 11
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
@@ -58,7 +60,11 @@ int main(int c)
/*@ assert tmp ≢ 0; */
g = tmp;
__retres = g + 1;
- __traces_domain_return = __retres;
+ {
+ int _result_main_;
+ _result_main_ = __retres;
+ __traces_domain_return = __retres;
+ }
}
}
return __traces_domain_return;
diff --git a/tests/value/traces/oracle/test4.err.oracle b/tests/value/traces/oracle/test4.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/tests/value/traces/oracle/test4.res.oracle b/tests/value/traces/oracle/test4.res.oracle
index 58d76d1237695a1dc97a49ef367b042c67f254ce..62f44d1b1031d4d20500bb91b2d631300bead971 100644
--- a/tests/value/traces/oracle/test4.res.oracle
+++ b/tests/value/traces/oracle/test4.res.oracle
@@ -260,7 +260,9 @@ c -> 1
228 -> Assume: i < 100 false -> 229
229 -> leave_loop -> 230
230 -> LeaveScope: i -> 231
- 231 -> LeaveScope: i -> 232 ]} at 232
+ 231 -> LeaveScope: i -> 232
+ 232 -> EnterScope: \result<main> -> 233
+ 233 -> Assign: \result<main> = tmp -> 234 ]} at 234
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
diff --git a/tests/value/traces/oracle/test5.err.oracle b/tests/value/traces/oracle/test5.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/tests/value/traces/oracle/test5.res.oracle b/tests/value/traces/oracle/test5.res.oracle
index 44b41790709aaacdddb7a1205dace5c258bcf91a..3e62ee426800f13b6834b0e94ff0c75ae1b13e18 100644
--- a/tests/value/traces/oracle/test5.res.oracle
+++ b/tests/value/traces/oracle/test5.res.oracle
@@ -563,7 +563,9 @@ c -> 1
368 -> join -> 369
369 -> join -> 370
370 -> join -> 371
- 371 -> join -> 372 ]} at 372
+ 371 -> join -> 372
+ 372 -> EnterScope: \result<main> -> 373
+ 373 -> Assign: \result<main> = tmp -> 374 ]} at 374
[from] Computing for function main
[from] Computing for function my_switch <-main
[from] Done for function my_switch