diff --git a/src/plugins/value/domains/traces/traces_domain.ml b/src/plugins/value/domains/traces/traces_domain.ml
index 8e8296daf464f235bedf01b2ffb1965bec21049e..334f722ea511cd9b01e696f15bded7767a7a1049 100644
--- a/src/plugins/value/domains/traces/traces_domain.ml
+++ b/src/plugins/value/domains/traces/traces_domain.ml
@@ -330,16 +330,24 @@ module Internal = struct
`Value(Traces.add_edge state (Assume(0,e,pos)))
let start_call _stmt call _valuation state =
- let msg =
- Format.asprintf "start_call: %a" (Pretty_utils.pp_list ~sep:",@ "
- (fun fmt v -> Cil_datatype.Varinfo.pretty fmt v.Eval.formal))
- call.Eval.arguments in
+ let msg = Format.asprintf "start_call: %s" (Kernel_function.get_name call.Eval.kf) in
let state = Traces.add_edge state (Msg(0,msg)) in
+ let formals = List.map (fun arg -> arg.Eval.formal) call.Eval.arguments in
+ let state = Traces.add_edge state (EnterScope(0,formals)) in
+ let state = List.fold_left (fun state arg ->
+ Traces.add_edge state (Assign(0,
+ Cil.var arg.Eval.formal,
+ arg.Eval.formal.Cil_types.vtype,
+ arg.Eval.concrete))) state call.Eval.arguments in
`Value state
let finalize_call _stmt call ~pre:_ ~post =
- `Value (Traces.add_edge post (Msg(0,Format.asprintf "finalize_call: %a"
- (Pretty_utils.pp_opt Cil_datatype.Varinfo.pretty) call.Eval.return)))
+ let state = post in
+ let msg = Format.asprintf "finalize_call: %s" (Kernel_function.get_name call.Eval.kf) in
+ let state = Traces.add_edge state (Msg(0,msg)) in
+ (* let formals = List.map (fun arg -> arg.Eval.formal) call.Eval.arguments in *)
+ (* let state = Traces.add_edge state (LeaveScope(0,formals)) in *)
+ `Value state
let update _valuation state = `Value state
diff --git a/tests/value/traces/oracle/test2.res.oracle b/tests/value/traces/oracle/test2.res.oracle
index 52bb89001275159df17551cb2a5ce176e55eae48..7a40e8f876e0eace697193ed9a22f9c27088b015 100644
--- a/tests/value/traces/oracle/test2.res.oracle
+++ b/tests/value/traces/oracle/test2.res.oracle
@@ -24,61 +24,65 @@ tests/value/traces/test2.i:20:[value] Frama_C_dump_each:
3 -> ([ Assume: c false -> 4; Assume: c true -> 5 ])
4 -> ([ Assign: tmp = 2 -> 8 ])
5 -> ([ Assign: tmp = 1 -> 7 ])
- 7 -> ([ start_call: j -> 9 ])
- 8 -> ([ start_call: j -> 53 ])
- 9 -> ([ EnterScope: i -> 10 ])
- 10 -> ([ initialize variable: i -> 11 ])
- 11 -> ([ Assign: i = 0 -> 12 ])
- 12 -> ([ enter_loop -> 13 ])
- 13 -> ([ Assume: i < 3 true -> 14 ])
- 14 -> ([ Assign: j = j + 1 -> 15 ])
- 15 -> ([ Assign: i = i + 1 -> 16 ])
- 16 -> ([ incr_loop_counter -> 17 ])
- 17 -> ([ Assume: i < 3 true -> 19 ])
- 19 -> ([ Assign: j = j + 1 -> 20 ])
- 20 -> ([ Assign: i = i + 1 -> 21 ])
- 21 -> ([ incr_loop_counter -> 23 ])
- 23 -> ([ Assume: i < 3 true -> 25 ])
- 25 -> ([ Assign: j = j + 1 -> 26 ])
- 26 -> ([ Assign: i = i + 1 -> 27 ])
- 27 -> ([ incr_loop_counter -> 29 ])
- 29 -> ([ Assume: i < 3 false -> 31 ])
- 31 -> ([ leave_loop -> 32 ])
- 32 -> ([ LeaveScope: i -> 33 ])
- 33 -> ([ EnterScope: \result<loop> -> 34 ])
- 34 -> ([ Assign: \result<loop> = j -> 35 ])
- 35 -> ([ LeaveScope: j -> 49 ])
- 49 -> ([ finalize_call: \result<loop> -> 50 ])
- 50 -> ([ Assign: tmp = \result<loop> -> 51 ])
- 51 -> ([ LeaveScope: \result<loop> -> 52 ])
- 52 -> ([ join -> 116 ])
- 53 -> ([ EnterScope: i -> 55 ])
- 55 -> ([ initialize variable: i -> 56 ])
- 56 -> ([ Assign: i = 0 -> 57 ])
- 57 -> ([ enter_loop -> 58 ])
- 58 -> ([ Assume: i < 3 true -> 59 ])
- 59 -> ([ Assign: j = j + 1 -> 60 ])
- 60 -> ([ Assign: i = i + 1 -> 61 ])
- 61 -> ([ incr_loop_counter -> 62 ])
- 62 -> ([ Assume: i < 3 true -> 64 ])
- 64 -> ([ Assign: j = j + 1 -> 65 ])
- 65 -> ([ Assign: i = i + 1 -> 66 ])
- 66 -> ([ incr_loop_counter -> 68 ])
- 68 -> ([ Assume: i < 3 true -> 70 ])
- 70 -> ([ Assign: j = j + 1 -> 71 ])
- 71 -> ([ Assign: i = i + 1 -> 72 ])
- 72 -> ([ incr_loop_counter -> 74 ])
- 74 -> ([ Assume: i < 3 false -> 76 ])
- 76 -> ([ leave_loop -> 77 ])
- 77 -> ([ LeaveScope: i -> 78 ])
- 78 -> ([ EnterScope: \result<loop> -> 79 ])
- 79 -> ([ Assign: \result<loop> = j -> 80 ])
- 80 -> ([ LeaveScope: j -> 112 ])
- 112 -> ([ finalize_call: \result<loop> -> 113 ])
- 113 -> ([ Assign: tmp = \result<loop> -> 114 ])
- 114 -> ([ LeaveScope: \result<loop> -> 115 ])
- 115 -> ([ join -> 116 ]) ]}
- current: 116]
+ 7 -> ([ start_call: loop -> 9 ])
+ 8 -> ([ start_call: loop -> 55 ])
+ 9 -> ([ EnterScope: j -> 10 ])
+ 10 -> ([ Assign: j = tmp -> 11 ])
+ 11 -> ([ EnterScope: i -> 12 ])
+ 12 -> ([ initialize variable: i -> 13 ])
+ 13 -> ([ Assign: i = 0 -> 14 ])
+ 14 -> ([ enter_loop -> 15 ])
+ 15 -> ([ Assume: i < 3 true -> 16 ])
+ 16 -> ([ Assign: j = j + 1 -> 17 ])
+ 17 -> ([ Assign: i = i + 1 -> 18 ])
+ 18 -> ([ incr_loop_counter -> 19 ])
+ 19 -> ([ Assume: i < 3 true -> 21 ])
+ 21 -> ([ Assign: j = j + 1 -> 22 ])
+ 22 -> ([ Assign: i = i + 1 -> 23 ])
+ 23 -> ([ incr_loop_counter -> 25 ])
+ 25 -> ([ Assume: i < 3 true -> 27 ])
+ 27 -> ([ Assign: j = j + 1 -> 28 ])
+ 28 -> ([ Assign: i = i + 1 -> 29 ])
+ 29 -> ([ incr_loop_counter -> 31 ])
+ 31 -> ([ Assume: i < 3 false -> 33 ])
+ 33 -> ([ leave_loop -> 34 ])
+ 34 -> ([ LeaveScope: i -> 35 ])
+ 35 -> ([ EnterScope: \result<loop> -> 36 ])
+ 36 -> ([ Assign: \result<loop> = j -> 37 ])
+ 37 -> ([ LeaveScope: j -> 51 ])
+ 51 -> ([ finalize_call: loop -> 52 ])
+ 52 -> ([ Assign: tmp = \result<loop> -> 53 ])
+ 53 -> ([ LeaveScope: \result<loop> -> 54 ])
+ 54 -> ([ join -> 120 ])
+ 55 -> ([ EnterScope: j -> 56 ])
+ 56 -> ([ Assign: j = tmp -> 57 ])
+ 57 -> ([ EnterScope: i -> 59 ])
+ 59 -> ([ initialize variable: i -> 60 ])
+ 60 -> ([ Assign: i = 0 -> 61 ])
+ 61 -> ([ enter_loop -> 62 ])
+ 62 -> ([ Assume: i < 3 true -> 63 ])
+ 63 -> ([ Assign: j = j + 1 -> 64 ])
+ 64 -> ([ Assign: i = i + 1 -> 65 ])
+ 65 -> ([ incr_loop_counter -> 66 ])
+ 66 -> ([ Assume: i < 3 true -> 68 ])
+ 68 -> ([ Assign: j = j + 1 -> 69 ])
+ 69 -> ([ Assign: i = i + 1 -> 70 ])
+ 70 -> ([ incr_loop_counter -> 72 ])
+ 72 -> ([ Assume: i < 3 true -> 74 ])
+ 74 -> ([ Assign: j = j + 1 -> 75 ])
+ 75 -> ([ Assign: i = i + 1 -> 76 ])
+ 76 -> ([ incr_loop_counter -> 78 ])
+ 78 -> ([ Assume: i < 3 false -> 80 ])
+ 80 -> ([ leave_loop -> 81 ])
+ 81 -> ([ LeaveScope: i -> 82 ])
+ 82 -> ([ EnterScope: \result<loop> -> 83 ])
+ 83 -> ([ Assign: \result<loop> = j -> 84 ])
+ 84 -> ([ LeaveScope: j -> 116 ])
+ 116 -> ([ finalize_call: loop -> 117 ])
+ 117 -> ([ Assign: tmp = \result<loop> -> 118 ])
+ 118 -> ([ LeaveScope: \result<loop> -> 119 ])
+ 119 -> ([ join -> 120 ]) ]}
+ current: 120]
==END OF DUMP==
[value] Recording results for main
[value] done for function main