From 9fb45638d91ad2d7d1c8fae47d892ff723c98ac6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 9 Apr 2019 11:01:16 +0200
Subject: [PATCH] [Eva] Embeds split_return in partition as a new partitioning
action.
Moves function split_by_evaluation from evaluation to partition.
Moves function split_final_state from transfer_stmt to partition.
New partitioning action Restrict, that restricts the rationing according to the
evaluation of an expression into some expected values.
---
src/plugins/value/engine/evaluation.ml | 39 ------
src/plugins/value/engine/evaluation.mli | 15 ---
src/plugins/value/engine/partition.ml | 127 ++++++++++++++----
src/plugins/value/engine/partition.mli | 2 +-
.../value/engine/trace_partitioning.ml | 41 +++---
src/plugins/value/engine/transfer_stmt.ml | 27 ----
src/plugins/value/engine/transfer_stmt.mli | 3 -
tests/value/oracle/split_return.0.res.oracle | 2 +-
tests/value/oracle/split_return.1.res.oracle | 2 +-
tests/value/oracle/split_return.3.res.oracle | 28 ++--
tests/value/oracle/split_return.4.res.oracle | 50 +++----
11 files changed, 164 insertions(+), 172 deletions(-)
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index bf0c38fa2cc..cc4018b105a 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -208,9 +208,6 @@ module type S = sig
?valuation:Valuation.t -> state -> exp -> bool -> Valuation.t evaluated
val assume:
?valuation:Valuation.t -> state -> exp -> value -> Valuation.t or_bottom
- val split_by_evaluation:
- exp -> Integer.t list -> state list ->
- (Integer.t * state list * bool) list * state list
val eval_function_exp:
exp -> ?args:exp list -> state -> (Kernel_function.t * Valuation.t) list evaluated
val interpret_truth:
@@ -1587,42 +1584,6 @@ module Make
Bottom.bot_of_list list, alarms
end
| _ -> assert false
-
- let split_by_evaluation = match Value.get Main_values.cvalue_key with
- | None -> fun _ _ states -> [], states
- | Some get -> fun expr expected_values states ->
- let typ = Cil.typeOf expr in
- let eval acc state =
- match fst (evaluate state expr) with
- | `Bottom -> (state, `Bottom, false) :: acc
- | `Value (_cache, value) ->
- let zero_or_one = Cvalue.V.cardinal_zero_or_one (get value) in
- (state, `Value value, zero_or_one) :: acc
- in
- let eval_states = List.fold_left eval [] states in
- let match_expected_value expected_value states =
- let process_one_state (eq, mess, neq) (s, v, zero_or_one as current) =
- if Bottom.is_included Value.is_included expected_value v then
- (* The integer on which we split is part of the result *)
- if zero_or_one then
- (s :: eq, mess, neq) (* Clean split *)
- else
- (eq, true, current :: neq) (* v is not exact: mess, i.e. no split *)
- else
- (eq, mess, current :: neq) (* Integer not in the result at all *)
- in
- List.fold_left process_one_state ([], false, []) states
- in
- let process_one_value (acc, states) i =
- let value = `Value (Value.reduce (Value.inject_int typ i)) in
- let eq, mess, neq = match_expected_value value states in
- (i, eq, mess) :: acc, neq
- in
- let matched, tail =
- List.fold_left process_one_value ([], eval_states) expected_values
- in
- matched, List.map (fun (s, _, _) -> s) tail
-
end
diff --git a/src/plugins/value/engine/evaluation.mli b/src/plugins/value/engine/evaluation.mli
index 9f263d86b36..ad8886669f2 100644
--- a/src/plugins/value/engine/evaluation.mli
+++ b/src/plugins/value/engine/evaluation.mli
@@ -94,21 +94,6 @@ module type S = sig
?valuation:Valuation.t ->
state -> exp -> value -> Valuation.t or_bottom
- (* Sorts a list of states by the evaluation of an expression, according to
- a list of expected integer values.
- [split_by_evaluation expr expected_values states] returns two list
- (matched, tail) such as:
- - for each element (i, states, mess) of the first list [matched],
- i was in the list of integer [expected_values], [states] is the list of
- input states where [expr] evaluates to exactly [i], and [mess] is true
- if there was some other input state on which [expr] evaluates to a value
- including [i] (but not equal to [i]).
- - tail are the states on which [expr] does not evaluate to none of the
- [expected_values]. *)
- val split_by_evaluation:
- exp -> Integer.t list -> state list ->
- (Integer.t * state list * bool) list * state list
-
val eval_function_exp:
exp -> ?args:exp list -> state ->
(Kernel_function.t * Valuation.t) list evaluated
diff --git a/src/plugins/value/engine/partition.ml b/src/plugins/value/engine/partition.ml
index ad833cba6dd..8b7c530a1aa 100644
--- a/src/plugins/value/engine/partition.ml
+++ b/src/plugins/value/engine/partition.ml
@@ -158,6 +158,7 @@ type action =
| Incr_loop
| Branch of branch * int
| Ration of rationing
+ | Restrict of Cil_types.exp * Integer.t list
| Split of Cil_types.exp * split_kind * int
| Merge of Cil_types.exp * split_kind
| Update_dynamic_splits
@@ -297,7 +298,6 @@ struct
to increase this limit."
monitor.split_limit pp_count
-
let eval_exp_to_int state exp =
let _valuation, ival = evaluate_exp_to_ival state exp in
try
@@ -308,8 +308,105 @@ struct
| Failure _ ->
fail ~exp "this partitioning parameter is too big"
+ (* Sorts a list of states by the evaluation of an expression, according to
+ a list of expected integer values.
+ [split_by_evaluation expr expected_values states] returns two list
+ (matched, tail) such as:
+ - for each element (i, states, mess) of the first list [matched],
+ i was in the list of integer [expected_values], [states] is the list of
+ input states where [expr] evaluates to exactly [i], and [mess] is true
+ if there was some other input state on which [expr] evaluates to a value
+ including [i] (but not equal to [i]).
+ - tail are the states on which [expr] does not evaluate to none of the
+ [expected_values]. *)
+ let split_by_evaluation = match Abstract.Val.get Main_values.cvalue_key with
+ | None -> fun _ _ states -> [], states
+ | Some get -> fun expr expected_values states ->
+ let typ = Cil.typeOf expr in
+ let eval acc state =
+ match fst (Abstract.Eval.evaluate state expr) with
+ | `Bottom -> (state, `Bottom, false) :: acc
+ | `Value (_cache, value) ->
+ let zero_or_one = Cvalue.V.cardinal_zero_or_one (get value) in
+ (state, `Value value, zero_or_one) :: acc
+ in
+ let eval_states = List.fold_left eval [] states in
+ let match_expected_value expected_value states =
+ let process_one_state (eq, mess, neq) (s, v, zero_or_one as current) =
+ if Bottom.is_included Abstract.Val.is_included expected_value v then
+ (* The integer on which we split is part of the result *)
+ if zero_or_one then
+ (s :: eq, mess, neq) (* Clean split *)
+ else
+ (eq, true, current :: neq) (* v is not exact: mess, i.e. no split *)
+ else
+ (eq, mess, current :: neq) (* Integer not in the result at all *)
+ in
+ List.fold_left process_one_state ([], false, []) states
+ in
+ let process_one_value (acc, states) i =
+ let value = `Value Abstract.Val.(reduce (inject_int typ i)) in
+ let eq, mess, neq = match_expected_value value states in
+ (i, eq, mess) :: acc, neq
+ in
+ let matched, tail =
+ List.fold_left process_one_value ([], eval_states) expected_values
+ in
+ matched, List.map (fun (s, _, _) -> s) tail
+
+ let smash_states = function
+ | [] -> []
+ | v1 :: l -> [ List.fold_left Abstract.Dom.join v1 l ]
+
+ (* In the list of [states], join states in which [expr] evaluates to the
+ same exact value in [expected_values] or to any other value. *)
+ let merge_by_value expr expected_values states =
+ let states =
+ if Cil.isIntegralOrPointerType (Cil.typeOf expr)
+ then
+ let matched, tail =
+ split_by_evaluation expr expected_values states
+ in
+ let process (i, states, mess) =
+ if mess then
+ Value_parameters.result ~once:true ~current:true
+ "cannot properly split on \\result == %a"
+ Abstract_interp.Int.pretty i;
+ states
+ in
+ tail :: List.map process matched
+ else [states]
+ in
+ List.flatten (List.map smash_states states)
+
(* --- Applying partitioning actions onto flows --------------------------- *)
+ (* Applies the transfer function [f] to the states whose partitioning keys
+ only differ by the ration stamp. [f] may smash those states, thus
+ restricting the rationing without affecting the other partitioning. *)
+ let restrict_rationing (f : state list -> state list) (p : t) : t =
+ (* Group the states in buckets, where each bucket is a list of states
+ with the same key except for the ration stamp *)
+ let fill_buckets buckets (k,x) =
+ (* Ignore the ration stamp *)
+ let k = { k with ration_stamp = None } in
+ (* Find the bucket *)
+ let contents =
+ try KMap.find k buckets
+ with Not_found -> []
+ in
+ (* Add the state to the bucket *)
+ KMap.add k (x :: contents) buckets
+ in
+ let buckets = List.fold_left fill_buckets KMap.empty p in
+ (* Apply the transfer function to each bucket *)
+ let result = KMap.map f buckets in
+ (* Rebuild the flow *)
+ let add_bucket k bucket acc =
+ List.map (fun x -> k,x) bucket @ acc
+ in
+ KMap.fold add_bucket result []
+
let split_state ~monitor (kind : split_kind) (exp : Cil_types.exp)
(key : key) (state : state) : (key * state) list =
try
@@ -358,9 +455,12 @@ struct
| Update_dynamic_splits ->
update_dynamic_splits p
+ | Restrict (expr, expected_values) ->
+ restrict_rationing (merge_by_value expr expected_values) p
+
| action -> (* Simple map transfer functions *)
let transfer = match action with
- | Split _ | Update_dynamic_splits ->
+ | Restrict _ | Split _ | Update_dynamic_splits ->
assert false (* Handled above *)
| Enter_loop limit_kind -> fun k x ->
@@ -446,29 +546,6 @@ struct
in
List.fold_left transfer [] p
- let legacy_transfer_states (f : state list -> state list) (p : t) : t =
- (* Group the states in buckets, where each bucket is a list of states
- with the same key except for the ration stamp *)
- let fill_buckets buckets (k,x) =
- (* Ignore the ration stamp *)
- let k = { k with ration_stamp = None } in
- (* Find the bucket *)
- let contents =
- try KMap.find k buckets
- with Not_found -> []
- in
- (* Add the state to the bucket *)
- KMap.add k (x :: contents) buckets
- in
- let buckets = List.fold_left fill_buckets KMap.empty p in
- (* Apply the transfer function to each bucket *)
- let result = KMap.map f buckets in
- (* Rebuild the flow *)
- let add_bucket k bucket acc =
- List.map (fun x -> k,x) bucket @ acc
- in
- KMap.fold add_bucket result []
-
let iter (f : state -> unit) (p : t) : unit =
List.iter (fun (_k,x) -> f x) p
end
diff --git a/src/plugins/value/engine/partition.mli b/src/plugins/value/engine/partition.mli
index 10155a3d869..ed7a1211289 100644
--- a/src/plugins/value/engine/partition.mli
+++ b/src/plugins/value/engine/partition.mli
@@ -102,6 +102,7 @@ type action =
| Incr_loop
| Branch of branch * int (* branch taken, max branches in history *)
| Ration of rationing
+ | Restrict of Cil_types.exp * Integer.t list
| Split of Cil_types.exp * split_kind * int
| Merge of Cil_types.exp * split_kind
| Update_dynamic_splits
@@ -130,7 +131,6 @@ sig
val transfer_keys : t -> action -> t
val transfer_states : (state -> state list) -> t -> t
- val legacy_transfer_states : (state list -> state list) -> t -> t
val iter : (state -> unit) -> t -> unit
end
diff --git a/src/plugins/value/engine/trace_partitioning.ml b/src/plugins/value/engine/trace_partitioning.ml
index 701487999a2..c4bb0eb2bb2 100644
--- a/src/plugins/value/engine/trace_partitioning.ml
+++ b/src/plugins/value/engine/trace_partitioning.ml
@@ -151,38 +151,37 @@ struct
(* Partition transfer functions *)
- let loop_transfer p action =
+ let transfer_action p action =
p.flow_states <- Flow.transfer_keys p.flow_states action
let enter_loop (p : flow) (i : loop) : unit =
- loop_transfer p (Enter_loop (unroll i))
+ transfer_action p (Enter_loop (unroll i))
let leave_loop (p : flow) (_i : loop) : unit =
- loop_transfer p Leave_loop
+ transfer_action p Leave_loop
let next_loop_iteration (p : flow) (_i : loop) : unit =
- loop_transfer p Incr_loop
+ transfer_action p Incr_loop
+
+ let empty_rationing = new_rationing ~limit:0 ~merge:false
let split_return (flow : flow) (return_exp : exp option) : unit =
- (** Join every state in the list *)
- let transfer_split states =
+ let strategy = Split_return.kf_strategy kf in
+ if strategy <> Split_strategy.FullSplit
+ then
+ let smash () =
+ transfer_action flow (Ration empty_rationing);
+ let p = Flow.to_partition flow.flow_states in
+ flow.flow_states <- Flow.of_partition p
+ in
match Split_return.kf_strategy kf with
+ (* SplitAuto already transformed into SplitEqList. *)
+ | Split_strategy.FullSplit | Split_strategy.SplitAuto -> assert false
+ | Split_strategy.NoSplit -> smash ()
| Split_strategy.SplitEqList i ->
- begin match return_exp with
- | Some return_exp ->
- let states = Transfer.split_final_states kf return_exp i states in
- List.flatten (List.map smash_states states)
- | None ->
- smash_states states
- end
- | Split_strategy.NoSplit -> smash_states states
- | Split_strategy.FullSplit -> states
- (* Last case not possible : already transformed into SplitEqList *)
- | Split_strategy.SplitAuto -> assert false
- in
- flow.flow_states <-
- Flow.legacy_transfer_states transfer_split flow.flow_states
-
+ match return_exp with
+ | None -> smash ()
+ | Some return_exp -> transfer_action flow (Restrict (return_exp, i))
(* Reset state (for hierchical convergence) *)
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index c81a78f0133..e7be6f8f582 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -33,8 +33,6 @@ module type S = sig
val call:
stmt -> lval option -> exp -> exp list -> state ->
state list or_bottom * Value_types.cacheable
- val split_final_states:
- kernel_function -> exp -> Integer.t list -> state list -> state list list
val check_unspecified_sequence:
stmt ->
state -> (stmt * lval list * lval list * lval list * stmt ref list) list ->
@@ -764,31 +762,6 @@ module Make (Abstract: Abstractions.Eva) = struct
in
eval, !cacheable
-
- (* ------------------------------------------------------------------------ *)
- (* Function Return *)
- (* ------------------------------------------------------------------------ *)
-
- let split_final_states kf return_expr expected_values states =
- let varinfo = match return_expr.enode with
- | Lval (Var varinfo, NoOffset) -> varinfo
- | _ -> assert false (* Cil invariant *)
- in
- if Cil.isIntegralOrPointerType varinfo.vtype
- then
- let matched, tail =
- Eval.split_by_evaluation return_expr expected_values states
- in
- let process (i, states, mess) =
- if mess then
- Value_parameters.result ~once:true ~current:true
- "%a: cannot properly split on \\result == %a"
- Kernel_function.pretty kf Abstract_interp.Int.pretty i;
- states
- in
- tail :: List.map process matched
- else [states]
-
(* ------------------------------------------------------------------------ *)
(* Unspecified Sequence *)
(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/value/engine/transfer_stmt.mli b/src/plugins/value/engine/transfer_stmt.mli
index a2e64699a2e..567674a5f34 100644
--- a/src/plugins/value/engine/transfer_stmt.mli
+++ b/src/plugins/value/engine/transfer_stmt.mli
@@ -39,9 +39,6 @@ module type S = sig
stmt -> lval option -> exp -> exp list -> state ->
state list or_bottom * Value_types.cacheable
- val split_final_states:
- kernel_function -> exp -> Integer.t list -> state list -> state list list
-
val check_unspecified_sequence:
Cil_types.stmt ->
state ->
diff --git a/tests/value/oracle/split_return.0.res.oracle b/tests/value/oracle/split_return.0.res.oracle
index 342033647fd..073552cab4f 100644
--- a/tests/value/oracle/split_return.0.res.oracle
+++ b/tests/value/oracle/split_return.0.res.oracle
@@ -43,7 +43,7 @@
Called from tests/value/split_return.i:206.
[eva] computing for function f3 <- main3 <- main.
Called from tests/value/split_return.i:73.
-[eva] tests/value/split_return.i:69: f3: cannot properly split on \result == -2
+[eva] tests/value/split_return.i:69: cannot properly split on \result == -2
[eva] Recording results for f3
[eva] Done for function f3
[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2; 7}, {0; 5}
diff --git a/tests/value/oracle/split_return.1.res.oracle b/tests/value/oracle/split_return.1.res.oracle
index ff8657d99c4..27d86c75523 100644
--- a/tests/value/oracle/split_return.1.res.oracle
+++ b/tests/value/oracle/split_return.1.res.oracle
@@ -83,7 +83,7 @@
Called from tests/value/split_return.i:135.
[eva:alarm] tests/value/split_return.i:130: Warning:
assertion got status unknown.
-[eva] tests/value/split_return.i:131: f6: cannot properly split on \result == 0
+[eva] tests/value/split_return.i:131: cannot properly split on \result == 0
[eva] Recording results for f6
[eva] Done for function f6
[eva] Recording results for main6
diff --git a/tests/value/oracle/split_return.3.res.oracle b/tests/value/oracle/split_return.3.res.oracle
index bfdd36469af..1ad5a6b9498 100644
--- a/tests/value/oracle/split_return.3.res.oracle
+++ b/tests/value/oracle/split_return.3.res.oracle
@@ -26,12 +26,12 @@
Called from tests/value/split_return.i:48.
[eva] Recording results for f2
[eva] Done for function f2
-[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {7}, {5}
-[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {5}, {5}
[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {0}, {0}
+[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {5}, {5}
+[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {7}, {5}
[eva] tests/value/split_return.i:51: assertion got status valid.
-[eva] tests/value/split_return.i:53: Frama_C_show_each_f2_2: {7}, {5}
[eva] tests/value/split_return.i:53: Frama_C_show_each_f2_2: {5}, {5}
+[eva] tests/value/split_return.i:53: Frama_C_show_each_f2_2: {7}, {5}
[eva] tests/value/split_return.i:54: assertion got status valid.
[eva] Recording results for main2
[eva] Done for function main2
@@ -41,8 +41,8 @@
Called from tests/value/split_return.i:73.
[eva] Recording results for f3
[eva] Done for function f3
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
[eva] tests/value/split_return.i:76: assertion got status valid.
[eva] tests/value/split_return.i:78: assertion got status valid.
[eva] Recording results for main3
@@ -53,8 +53,8 @@
Called from tests/value/split_return.i:73.
[eva] Recording results for f3
[eva] Done for function f3
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main4 <- main.
@@ -63,8 +63,8 @@
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] tests/value/split_return.i:97: assertion got status valid.
[eva] tests/value/split_return.i:99: assertion got status valid.
[eva] Recording results for main4
@@ -75,8 +75,8 @@
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
@@ -85,8 +85,8 @@
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
@@ -95,8 +95,8 @@
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main5 <- main.
@@ -105,8 +105,8 @@
Called from tests/value/split_return.i:117.
[eva] Recording results for f5
[eva] Done for function f5
-[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {-2}, {0}
[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {7}, {5}
+[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {-2}, {0}
[eva] tests/value/split_return.i:120: assertion got status valid.
[eva] tests/value/split_return.i:122: assertion got status valid.
[eva] Recording results for main5
@@ -155,8 +155,8 @@
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
@@ -165,8 +165,8 @@
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
@@ -175,8 +175,8 @@
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
@@ -185,8 +185,8 @@
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main9 <- main.
diff --git a/tests/value/oracle/split_return.4.res.oracle b/tests/value/oracle/split_return.4.res.oracle
index 060b00fe35e..46c3281323e 100644
--- a/tests/value/oracle/split_return.4.res.oracle
+++ b/tests/value/oracle/split_return.4.res.oracle
@@ -29,12 +29,12 @@
Called from tests/value/split_return.i:48.
[eva] Recording results for f2
[eva] Done for function f2
-[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {7}, {5}
-[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {5}, {5}
[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {0}, {0}
+[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {5}, {5}
+[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {7}, {5}
[eva] tests/value/split_return.i:51: assertion got status valid.
-[eva] tests/value/split_return.i:53: Frama_C_show_each_f2_2: {7}, {5}
[eva] tests/value/split_return.i:53: Frama_C_show_each_f2_2: {5}, {5}
+[eva] tests/value/split_return.i:53: Frama_C_show_each_f2_2: {7}, {5}
[eva] tests/value/split_return.i:54: assertion got status valid.
[eva] Recording results for main2
[eva] Done for function main2
@@ -44,8 +44,8 @@
Called from tests/value/split_return.i:73.
[eva] Recording results for f3
[eva] Done for function f3
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
[eva] tests/value/split_return.i:76: assertion got status valid.
[eva] tests/value/split_return.i:78: assertion got status valid.
[eva] Recording results for main3
@@ -56,8 +56,8 @@
Called from tests/value/split_return.i:73.
[eva] Recording results for f3
[eva] Done for function f3
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main4 <- main.
@@ -66,8 +66,8 @@
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] tests/value/split_return.i:97: assertion got status valid.
[eva] tests/value/split_return.i:99: assertion got status valid.
[eva] Recording results for main4
@@ -78,8 +78,8 @@
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
@@ -88,8 +88,8 @@
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
@@ -98,8 +98,8 @@
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main5 <- main.
@@ -108,8 +108,8 @@
Called from tests/value/split_return.i:117.
[eva] Recording results for f5
[eva] Done for function f5
-[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {-2}, {0}
[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {7}, {5}
+[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {-2}, {0}
[eva] tests/value/split_return.i:120: assertion got status valid.
[eva] tests/value/split_return.i:122: assertion got status valid.
[eva] Recording results for main5
@@ -158,8 +158,8 @@
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
@@ -168,8 +168,8 @@
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
@@ -178,8 +178,8 @@
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
@@ -188,8 +188,8 @@
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main9 <- main.
@@ -483,8 +483,8 @@
Called from tests/value/split_return.i:73.
[eva] Recording results for f3
[eva] Done for function f3
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main3 <- main.
@@ -493,8 +493,8 @@
Called from tests/value/split_return.i:73.
[eva] Recording results for f3
[eva] Done for function f3
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main4 <- main.
@@ -503,8 +503,8 @@
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
@@ -513,8 +513,8 @@
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
@@ -523,8 +523,8 @@
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
@@ -533,8 +533,8 @@
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main5 <- main.
@@ -543,8 +543,8 @@
Called from tests/value/split_return.i:117.
[eva] Recording results for f5
[eva] Done for function f5
-[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {-2}, {0}
[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {7}, {5}
+[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {-2}, {0}
[eva] Recording results for main5
[eva] Done for function main5
[eva] computing for function main6 <- main.
@@ -589,8 +589,8 @@
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
@@ -599,8 +599,8 @@
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
@@ -609,8 +609,8 @@
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
@@ -619,8 +619,8 @@
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main9 <- main.
--
GitLab