From 7689f12aaa3698d77e838cbf1f6e6575f1a53256 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 9 Oct 2017 16:17:47 +0200
Subject: [PATCH] [Eva] Traces domain: improves dot output, fixes oracles
---
src/libraries/utils/hptmap.ml | 15 +-
src/libraries/utils/hptmap_sig.mli | 3 +
.../value/domains/traces/traces_domain.ml | 127 ++--
src/plugins/value/value_parameters.ml | 18 +
src/plugins/value/value_parameters.mli | 2 +
tests/value/traces/oracle/test1.res.oracle | 95 ++-
tests/value/traces/oracle/test2.res.oracle | 117 ++--
tests/value/traces/oracle/test3.res.oracle | 43 +-
tests/value/traces/oracle/test4.res.oracle | 304 ++++++++--
tests/value/traces/oracle/test5.err.oracle | 0
tests/value/traces/oracle/test5.res.oracle | 556 ++++++++++++++++++
tests/value/traces/test1.c | 2 +-
tests/value/traces/test2.i | 2 +-
tests/value/traces/test3.i | 2 +-
tests/value/traces/test4.i | 3 +-
tests/value/traces/test5.i | 25 +
16 files changed, 1081 insertions(+), 233 deletions(-)
create mode 100644 tests/value/traces/oracle/test5.err.oracle
create mode 100644 tests/value/traces/oracle/test5.res.oracle
create mode 100644 tests/value/traces/test5.i
diff --git a/src/libraries/utils/hptmap.ml b/src/libraries/utils/hptmap.ml
index a52b9aa8db4..d05e75ceb1e 100644
--- a/src/libraries/utils/hptmap.ml
+++ b/src/libraries/utils/hptmap.ml
@@ -856,11 +856,6 @@ struct
else if tree1' == Empty then tree0'
else wrap_Branch p m tree0' tree1'
- (* The comment below is outdated: [map] and [endo_map] do not have the
- same signature for [f] *)
- (** [endo_map] is similar to [map], but attempts to physically share its
- result with its input. This saves memory when [f] is the identity
- function. *)
let rec endo_map f tree =
match tree with
| Empty ->
@@ -885,6 +880,16 @@ struct
| Branch (p, m, t1, t2, _) ->
wrap_Branch p m (from_shape f t1) (from_shape f t2)
+ let rec from_shape_id = function
+ | Empty -> Empty
+ | Leaf (key, value, _) -> wrap_Leaf key value
+ | Branch (p, m, t1, t2, _) as t ->
+ let t1' = from_shape_id t1 in
+ let t2' = from_shape_id t2 in
+ if (t1' == t1) && (t2' == t2)
+ then t
+ else wrap_Branch p m t1' t2'
+
module Cacheable = struct
type t = hptmap
diff --git a/src/libraries/utils/hptmap_sig.mli b/src/libraries/utils/hptmap_sig.mli
index c6ae85bcf1e..a22d6fa4b3f 100644
--- a/src/libraries/utils/hptmap_sig.mli
+++ b/src/libraries/utils/hptmap_sig.mli
@@ -317,6 +317,9 @@ module type S = sig
More efficient than just performing successive {!add} the elements
of the other map *)
+ val from_shape_id: v shape -> t
+ (** Same as [from_shape (fun _ v -> v)]. *)
+
val shape: t -> v shape
(** Export the map as a value suitable for functions {!inter_with_shape}
and {!from_shape} *)
diff --git a/src/plugins/value/domains/traces/traces_domain.ml b/src/plugins/value/domains/traces/traces_domain.ml
index 170b2d90411..f466c5f9c22 100644
--- a/src/plugins/value/domains/traces/traces_domain.ml
+++ b/src/plugins/value/domains/traces/traces_domain.ml
@@ -58,25 +58,37 @@ type edge =
(* Frama-C "datatype" for type [inout] *)
module Edge = struct
- let rec pretty fmt = function
- | Assign(n,loc,_typ,exp) -> Format.fprintf fmt "@[Assign:@ %a = %a -> %a@]"
- Lval.pretty loc ExpStructEq.pretty exp Node.pretty n
- | Assume(n,e,b) -> Format.fprintf fmt "@[Assume:@ %a %b -> %a@]" ExpStructEq.pretty e b Node.pretty n
- | EnterScope(n,vs) -> Format.fprintf fmt "@[EnterScope:@ %a -> %a@]"
- (Pretty_utils.pp_list ~sep:"@ " Varinfo.pretty) vs Node.pretty n
- | LeaveScope(n,vs) -> Format.fprintf fmt "@[LeaveScope:@ %a -> %a@]"
- (Pretty_utils.pp_list ~sep:"@ " Varinfo.pretty) vs Node.pretty n
- | CallDeclared(n,kf1,exp1,lval1) ->
- Format.fprintf fmt "@[CallDeclared:@ %a%s(%a) -> %a@]"
+ let succ = function
+ | Assign (n,_,_,_)
+ | Assume (n,_,_)
+ | EnterScope (n,_)
+ | LeaveScope (n,_)
+ | CallDeclared (n,_,_,_)
+ | Msg (n,_)
+ | Loop(n,_,_,_) -> n
+
+
+ let rec pretty_edge fmt = function
+ | Assign(_,loc,_typ,exp) -> Format.fprintf fmt "Assign:@ %a = %a"
+ Lval.pretty loc ExpStructEq.pretty exp
+ | Assume(_,e,b) -> Format.fprintf fmt "Assume:@ %a %b" ExpStructEq.pretty e b
+ | EnterScope(_,vs) -> Format.fprintf fmt "EnterScope:@ %a"
+ (Pretty_utils.pp_list ~sep:"@ " Varinfo.pretty) vs
+ | LeaveScope(_,vs) -> Format.fprintf fmt "LeaveScope:@ %a"
+ (Pretty_utils.pp_list ~sep:"@ " Varinfo.pretty) vs
+ | CallDeclared(_,kf1,exp1,lval1) ->
+ Format.fprintf fmt "CallDeclared:@ %a%s(%a)"
(Pretty_utils.pp_opt ~pre:"" ~suf:" =@ " Lval.pretty) lval1
(Kernel_function.get_name kf1)
(Pretty_utils.pp_list ~sep:",@ " ExpStructEq.pretty) exp1
- Node.pretty n
- | Msg(n,s) -> Format.fprintf fmt "@[%s -> %a@]" s Node.pretty n
- | Loop(n,stmt,s,g) -> Format.fprintf fmt "@[<hv 2>@[Loop(%a) %a@] %a @[-> %a@]@]"
+
+ | Msg(_,s) -> Format.fprintf fmt "%s" s
+ | Loop(_,stmt,s,g) -> Format.fprintf fmt "@[Loop(%a) %a@] %a"
Stmt.pretty_sid stmt
Node.pretty s
- (GraphShape.pretty pretty_list) g Node.pretty n
+ (GraphShape.pretty pretty_list) g
+ and pretty fmt e =
+ Format.fprintf fmt "@[<hv 2>%a @[-> %a@]@]" pretty_edge e Node.pretty (succ e)
and pretty_list fmt l = Pretty_utils.pp_list ~sep:";@ " pretty fmt l
include Datatype.Make_with_collections(struct
@@ -366,15 +378,6 @@ module Traces = struct
~decide_right:Absorbing
g1 g2
- let get_node = function
- | Assign (n,_,_,_)
- | Assume (n,_,_)
- | EnterScope (n,_)
- | LeaveScope (n,_)
- | CallDeclared (n,_,_,_)
- | Msg (n,_)
- | Loop(n,_,_,_) -> n
-
let move_to c g state =
let rec aux = function
| Base (_,_) -> Base (c,g)
@@ -460,6 +463,8 @@ module Traces = struct
all_edges_ever_created := new_;
m
+ let get_node = Edge.succ
+
let add_edge_aux c edge =
let (current,graph) = get_current c in
let reusable =
@@ -692,7 +697,7 @@ module Traces = struct
Some (s,last)
| _ -> None in
let s,last = match Extlib.find_opt same_loop succs with
- | (s,last) -> s,(Graph.from_shape (fun _ v -> v) last)
+ | (s,last) -> s,(Graph.from_shape_id last)
| exception Not_found ->
Stmt.Hashtbl.memo state.all_loop_start stmt (fun _ -> Node.next (),Graph.empty)
in
@@ -799,12 +804,15 @@ module GraphDot = OCamlGraph.Graphviz.Dot(struct
type t =
| Usual of Node.t * Edge.t * Node.t list
| Head of Node.t * Node.t list * Node.t * Node.t list
+ | Back of Node.t * Node.t list * Node.t
let src = function
| Usual (src,_,loops) -> {node=src;loops}
| Head (src,loops,_,_) -> {node=src;loops}
+ | Back (_,loops,src) -> {node=src;loops}
let dst = function
| Usual (_,edge,loops) -> {node=Traces.get_node edge;loops}
| Head (_,_,s,loops) -> {node=s;loops}
+ | Back (dst,loops,_) -> {node=dst;loops}
end
open V
open E
@@ -824,12 +832,15 @@ module GraphDot = OCamlGraph.Graphviz.Dot(struct
| Loop(_,_,s,g) ->
let l' = (k::l) in
f (Head(k,l,s,l'));
- iter_vertex l' g
+ iter_vertex (Some s) l' g
| _ -> ()
- and iter_vertex l g =
- GraphShape.iter (fun k e -> List.iter (iter_edge k l) e) g
+ and iter_vertex back l g =
+ GraphShape.iter (fun k e ->
+ match e, back with
+ | [], Some back -> f (Back(back,l,k))
+ | e, _ -> List.iter (iter_edge k l) e) g
in
- iter_vertex [] (Graph.shape g)
+ iter_vertex None [] (Graph.shape g)
let graph_attributes _ = []
let default_vertex_attributes :
@@ -855,10 +866,35 @@ module GraphDot = OCamlGraph.Graphviz.Dot(struct
let edge_attributes : E.t -> OCamlGraph.Graphviz.DotAttributes.edge list =
function
| Usual(_,Loop _,_) -> [`Label (Format.asprintf "leave_loop")]
- | Usual(_,e,_) -> [`Label (Format.asprintf "%a" Edge.pretty e)]
+ | Usual(_,e,_) -> [`Label (Format.asprintf "@[<h>%a@]" Edge.pretty_edge e)]
| Head _ -> []
+ | Back(_,_,_) -> [`Constraint false]
end)
+(** adds n -> [] for leaves *)
+let rec complete_graph (graph:Graph.t) =
+ Graph.fold (fun k l graph ->
+ let graph, l =
+ Extlib.fold_map (fun graph e ->
+ let m = Graph.singleton (Traces.get_node e) [] in
+ let e = match e with
+ | Assign (_,_,_,_)
+ | Assume (_,_,_)
+ | EnterScope (_,_)
+ | LeaveScope (_,_)
+ | CallDeclared (_,_,_,_)
+ | Msg (_,_) -> e
+ | Loop (n,stmt,s,g) ->
+ let g = Graph.shape (complete_graph (Graph.from_shape_id g)) in
+ Loop(n,stmt,s,g)
+ in
+ Traces.join_graph graph m, e)
+ graph l
+ in
+ Traces.join_graph graph (Graph.singleton k l)
+ ) graph Graph.empty
+
+
let key = Structure.Key_Domain.create_key "traces domain"
module Internal = struct
@@ -1272,6 +1308,15 @@ let project_of_cfg vreturn s =
(* Format.printf "@[<2>@[file3:@] %a@]@." Printer.pp_file file; *)
(* ) () *)
+
+let output_dot filename state =
+ let out = open_out filename in
+ Value_parameters.feedback ~dkey:Internal.log_category "@[Output dot produced to %s.@]" filename;
+ (** *)
+ 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
@@ -1281,18 +1326,18 @@ let finish_computation () =
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;
- 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 false then begin
- let out = open_out "traces_domain.dot" in
- GraphDot.output_graph out (snd (Traces.get_current state));
- close_out out;
- end;
- project_of_cfg return_exp 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
(*
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 9efa279d727..6e4f5af72b2 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -339,6 +339,24 @@ module TracesStorage =
end)
let () = add_precision_dep TracesStorage.parameter
+let () = Parameter_customize.set_group domains
+module TracesDot = Empty_string
+ (struct
+ let option_name = "-eva-traces-dot"
+ let help = "Output to the given filename the Cfg in dot format."
+ let arg_name = "FILENAME"
+ end)
+
+
+let () = Parameter_customize.set_group domains
+module TracesProject = Bool
+ (struct
+ let option_name = "-eva-traces-project"
+ let help = "Try to convert the Cfg into a program in a new project."
+ let default = false
+ end)
+let () = add_precision_dep TracesProject.parameter
+
(* -------------------------------------------------------------------------- *)
(* --- Performance options --- *)
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 1015dc5e091..5aa46bb0a03 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -58,6 +58,8 @@ module GaugesStorage: Parameter_sig.Bool
module ApronStorage: Parameter_sig.Bool
module BitwiseOffsmStorage: Parameter_sig.Bool
module TracesStorage: Parameter_sig.Bool
+module TracesDot: Parameter_sig.String
+module TracesProject: Parameter_sig.Bool
module AutomaticContextMaxDepth: Parameter_sig.Int
diff --git a/tests/value/traces/oracle/test1.res.oracle b/tests/value/traces/oracle/test1.res.oracle
index fa6b3715603..fb550f92c6d 100644
--- a/tests/value/traces/oracle/test1.res.oracle
+++ b/tests/value/traces/oracle/test1.res.oracle
@@ -13,52 +13,52 @@
tmp ∈ {5; 45}
[value:d-traces] Trace domains:
start: 0; globals = g, entropy_source; main_formals = c;
- {[ 0 -> ([ initialize variable: entropy_source -> 1 ])
- 1 -> ([ initialize variable using type Library_Global
-entropy_source -> 2 ])
- 2 -> ([ initialize variable: g -> 3 ])
- 3 -> ([ Assign: g = 42 -> 4 ])
- 4 -> ([ initialize variable using type Main_Formal
-c -> 5 ])
- 5 -> ([ EnterScope: tmp -> 6 ])
- 6 -> ([ Assign: tmp = 0 -> 7 ])
- 7 -> ([ Assume: c false -> 8; Assume: c true -> 9 ])
- 8 -> ([ Assign: tmp = 2 -> 12 ])
- 9 -> ([ Assign: tmp = g -> 11 ])
- 11 -> ([ EnterScope: i -> 17 ])
- 12 -> ([ EnterScope: i -> 14 ])
- 14 -> ([ initialize variable: i -> 15 ])
- 15 -> ([ Assign: i = 0 -> 16 ])
- 16 -> ([ enter_loop -> 22 ])
- 17 -> ([ initialize variable: i -> 18 ])
- 18 -> ([ Assign: i = 0 -> 19 ])
- 19 -> ([ enter_loop -> 21 ])
- 21 -> ([ Assume: i < 3 true -> 24 ])
- 22 -> ([ Assume: i < 3 true -> 25 ])
- 24 -> ([ Assign: tmp = tmp + 1 -> 27 ])
- 25 -> ([ Assign: tmp = tmp + 1 -> 26 ])
- 26 -> ([ Assign: i = i + 1 -> 28 ])
- 27 -> ([ Assign: i = i + 1 -> 29 ])
- 28 -> ([ Assume: i < 3 true -> 34 ])
- 29 -> ([ Assume: i < 3 true -> 33 ])
- 33 -> ([ Assign: tmp = tmp + 1 -> 36 ])
- 34 -> ([ Assign: tmp = tmp + 1 -> 35 ])
- 35 -> ([ Assign: i = i + 1 -> 38 ])
- 36 -> ([ Assign: i = i + 1 -> 37 ])
- 37 -> ([ Assume: i < 3 true -> 44 ])
- 38 -> ([ Assume: i < 3 true -> 43 ])
- 43 -> ([ Assign: tmp = tmp + 1 -> 46 ])
- 44 -> ([ Assign: tmp = tmp + 1 -> 45 ])
- 45 -> ([ Assign: i = i + 1 -> 48 ])
- 46 -> ([ Assign: i = i + 1 -> 47 ])
- 47 -> ([ Assume: i < 3 false -> 54 ])
- 48 -> ([ Assume: i < 3 false -> 53 ])
- 53 -> ([ LeaveScope: i -> 55 ])
- 54 -> ([ LeaveScope: i -> 56 ])
- 55 -> ([ Assign: g = tmp -> 58 ])
- 56 -> ([ Assign: g = tmp -> 57 ])
- 57 -> ([ join -> 95 ])
- 58 -> ([ join -> 95 ]) ]} at 95
+ {[ 0 -> initialize variable: entropy_source -> 1
+ 1 -> initialize variable using type Library_Global
+entropy_source -> 2
+ 2 -> initialize variable: g -> 3
+ 3 -> Assign: g = 42 -> 4
+ 4 -> initialize variable using type Main_Formal
+c -> 5
+ 5 -> EnterScope: tmp -> 6
+ 6 -> Assign: tmp = 0 -> 7
+ 7 -> Assume: c false -> 8; Assume: c true -> 9
+ 8 -> Assign: tmp = 2 -> 12
+ 9 -> Assign: tmp = g -> 11
+ 11 -> EnterScope: i -> 17
+ 12 -> EnterScope: i -> 14
+ 14 -> initialize variable: i -> 15
+ 15 -> Assign: i = 0 -> 16
+ 16 -> enter_loop -> 22
+ 17 -> initialize variable: i -> 18
+ 18 -> Assign: i = 0 -> 19
+ 19 -> enter_loop -> 21
+ 21 -> Assume: i < 3 true -> 24
+ 22 -> Assume: i < 3 true -> 25
+ 24 -> Assign: tmp = tmp + 1 -> 27
+ 25 -> Assign: tmp = tmp + 1 -> 26
+ 26 -> Assign: i = i + 1 -> 28
+ 27 -> Assign: i = i + 1 -> 29
+ 28 -> Assume: i < 3 true -> 34
+ 29 -> Assume: i < 3 true -> 33
+ 33 -> Assign: tmp = tmp + 1 -> 36
+ 34 -> Assign: tmp = tmp + 1 -> 35
+ 35 -> Assign: i = i + 1 -> 38
+ 36 -> Assign: i = i + 1 -> 37
+ 37 -> Assume: i < 3 true -> 44
+ 38 -> Assume: i < 3 true -> 43
+ 43 -> Assign: tmp = tmp + 1 -> 46
+ 44 -> Assign: tmp = tmp + 1 -> 45
+ 45 -> Assign: i = i + 1 -> 48
+ 46 -> Assign: i = i + 1 -> 47
+ 47 -> Assume: i < 3 false -> 54
+ 48 -> Assume: i < 3 false -> 53
+ 53 -> LeaveScope: i -> 55
+ 54 -> LeaveScope: i -> 56
+ 55 -> Assign: g = tmp -> 58
+ 56 -> Assign: g = tmp -> 57
+ 57 -> join -> 59
+ 58 -> join -> 59 ]} at 59
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
@@ -82,9 +82,6 @@ c -> 5 ])
[value:final-states] Values at end of function main:
g ∈ {5; 45}
__traces_domain_return ∈ {5; 45}
-[value:d-traces] Trace domains:
- TOP
-[value] failure: The trace is TOP can't generate code
/* Generated by Frama-C */
extern int volatile entropy_source;
diff --git a/tests/value/traces/oracle/test2.res.oracle b/tests/value/traces/oracle/test2.res.oracle
index 4b76a11dc24..b855d5a7819 100644
--- a/tests/value/traces/oracle/test2.res.oracle
+++ b/tests/value/traces/oracle/test2.res.oracle
@@ -21,63 +21,63 @@
tmp ∈ {4; 5}
[value:d-traces] Trace domains:
start: 0; globals = ; main_formals = c;
- {[ 0 -> ([ initialize variable using type Main_Formal
-c -> 1 ])
- 1 -> ([ EnterScope: tmp -> 2 ])
- 2 -> ([ Assign: tmp = 0 -> 3 ])
- 3 -> ([ Assume: c false -> 4; Assume: c true -> 5 ])
- 4 -> ([ Assign: tmp = 2 -> 8 ])
- 5 -> ([ Assign: tmp = 1 -> 7 ])
- 7 -> ([ start_call: loop (true) -> 9 ])
- 8 -> ([ start_call: loop (true) -> 50 ])
- 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 -> ([ Assume: i < 3 true -> 20 ])
- 20 -> ([ Assign: j = j + 1 -> 21 ])
- 21 -> ([ Assign: i = i + 1 -> 22 ])
- 22 -> ([ Assume: i < 3 true -> 25 ])
- 25 -> ([ Assign: j = j + 1 -> 26 ])
- 26 -> ([ Assign: i = i + 1 -> 27 ])
- 27 -> ([ Assume: i < 3 false -> 30 ])
- 30 -> ([ LeaveScope: i -> 31 ])
- 31 -> ([ EnterScope: \result<loop> -> 32 ])
- 32 -> ([ Assign: \result<loop> = j -> 33 ])
- 33 -> ([ LeaveScope: j -> 46 ])
- 46 -> ([ finalize_call: loop -> 47 ])
- 47 -> ([ Assign: tmp = \result<loop> -> 48 ])
- 48 -> ([ LeaveScope: \result<loop> -> 49 ])
- 49 -> ([ join -> 113 ])
- 50 -> ([ EnterScope: j -> 51 ])
- 51 -> ([ Assign: j = tmp -> 52 ])
- 52 -> ([ EnterScope: i -> 54 ])
- 54 -> ([ initialize variable: i -> 55 ])
- 55 -> ([ Assign: i = 0 -> 56 ])
- 56 -> ([ enter_loop -> 57 ])
- 57 -> ([ Assume: i < 3 true -> 58 ])
- 58 -> ([ Assign: j = j + 1 -> 59 ])
- 59 -> ([ Assign: i = i + 1 -> 60 ])
- 60 -> ([ Assume: i < 3 true -> 62 ])
- 62 -> ([ Assign: j = j + 1 -> 63 ])
- 63 -> ([ Assign: i = i + 1 -> 64 ])
- 64 -> ([ Assume: i < 3 true -> 67 ])
- 67 -> ([ Assign: j = j + 1 -> 68 ])
- 68 -> ([ Assign: i = i + 1 -> 69 ])
- 69 -> ([ Assume: i < 3 false -> 72 ])
- 72 -> ([ LeaveScope: i -> 73 ])
- 73 -> ([ EnterScope: \result<loop> -> 74 ])
- 74 -> ([ Assign: \result<loop> = j -> 75 ])
- 75 -> ([ LeaveScope: j -> 105 ])
- 105 -> ([ finalize_call: loop -> 106 ])
- 106 -> ([ Assign: tmp = \result<loop> -> 107 ])
- 107 -> ([ LeaveScope: \result<loop> -> 108 ])
- 108 -> ([ join -> 113 ]) ]} at 113
+ {[ 0 -> initialize variable using type Main_Formal
+c -> 1
+ 1 -> EnterScope: tmp -> 2
+ 2 -> Assign: tmp = 0 -> 3
+ 3 -> Assume: c false -> 4; Assume: c true -> 5
+ 4 -> Assign: tmp = 2 -> 8
+ 5 -> Assign: tmp = 1 -> 7
+ 7 -> start_call: loop (true) -> 9
+ 8 -> start_call: loop (true) -> 45
+ 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 -> Assume: i < 3 true -> 20
+ 20 -> Assign: j = j + 1 -> 21
+ 21 -> Assign: i = i + 1 -> 22
+ 22 -> Assume: i < 3 true -> 25
+ 25 -> Assign: j = j + 1 -> 26
+ 26 -> Assign: i = i + 1 -> 27
+ 27 -> Assume: i < 3 false -> 30
+ 30 -> LeaveScope: i -> 31
+ 31 -> EnterScope: \result<loop> -> 32
+ 32 -> Assign: \result<loop> = j -> 33
+ 33 -> LeaveScope: j -> 41
+ 41 -> finalize_call: loop -> 42
+ 42 -> Assign: tmp = \result<loop> -> 43
+ 43 -> LeaveScope: \result<loop> -> 44
+ 44 -> join -> 90
+ 45 -> EnterScope: j -> 46
+ 46 -> Assign: j = tmp -> 47
+ 47 -> EnterScope: i -> 49
+ 49 -> initialize variable: i -> 50
+ 50 -> Assign: i = 0 -> 51
+ 51 -> enter_loop -> 52
+ 52 -> Assume: i < 3 true -> 53
+ 53 -> Assign: j = j + 1 -> 54
+ 54 -> Assign: i = i + 1 -> 55
+ 55 -> Assume: i < 3 true -> 57
+ 57 -> Assign: j = j + 1 -> 58
+ 58 -> Assign: i = i + 1 -> 59
+ 59 -> Assume: i < 3 true -> 62
+ 62 -> Assign: j = j + 1 -> 63
+ 63 -> Assign: i = i + 1 -> 64
+ 64 -> Assume: i < 3 false -> 67
+ 67 -> LeaveScope: i -> 68
+ 68 -> EnterScope: \result<loop> -> 69
+ 69 -> Assign: \result<loop> = j -> 70
+ 70 -> LeaveScope: j -> 86
+ 86 -> finalize_call: loop -> 87
+ 87 -> Assign: tmp = \result<loop> -> 88
+ 88 -> LeaveScope: \result<loop> -> 89
+ 89 -> join -> 90 ]} at 90
[from] Computing for function loop
[from] Done for function loop
[from] Computing for function main
@@ -106,9 +106,6 @@ c -> 1 ])
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
__traces_domain_return ∈ {4; 5}
-[value:d-traces] Trace domains:
- TOP
-[value] failure: The trace is TOP can't generate code
/* Generated by Frama-C */
int main(int c)
{
diff --git a/tests/value/traces/oracle/test3.res.oracle b/tests/value/traces/oracle/test3.res.oracle
index 0815593eb4d..a5b57bde5ac 100644
--- a/tests/value/traces/oracle/test3.res.oracle
+++ b/tests/value/traces/oracle/test3.res.oracle
@@ -13,16 +13,16 @@
__retres ∈ {5}
[value:d-traces] Trace domains:
start: 0; globals = g; main_formals = c;
- {[ 0 -> ([ initialize variable: g -> 1 ])
- 1 -> ([ initialize variable using type Main_Formal
-c -> 2 ])
- 2 -> ([ EnterScope: __retres -> 3 ])
- 3 -> ([ EnterScope: tmp -> 4 ])
- 4 -> ([ initialize variable: tmp -> 5 ])
- 5 -> ([ Assign: tmp = 4 -> 6 ])
- 6 -> ([ Assume: tmp true -> 7 ])
- 7 -> ([ Assign: g = tmp -> 8 ])
- 8 -> ([ Assign: __retres = g + 1 -> 9 ]) ]} at 9
+ {[ 0 -> initialize variable: g -> 1
+ 1 -> initialize variable using type Main_Formal
+c -> 2
+ 2 -> EnterScope: __retres -> 3
+ 3 -> EnterScope: tmp -> 4
+ 4 -> initialize variable: tmp -> 5
+ 5 -> Assign: tmp = 4 -> 6
+ 6 -> Assume: tmp true -> 7
+ 7 -> Assign: g = tmp -> 8
+ 8 -> Assign: __retres = g + 1 -> 9 ]} at 9
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
@@ -45,6 +45,23 @@ c -> 2 ])
[value:final-states] Values at end of function main:
g ∈ {4}
__traces_domain_return ∈ {5}
-[value:d-traces] Trace domains:
- TOP
-[value] failure: The trace is TOP can't generate code
+/* Generated by Frama-C */
+int g;
+int main(int c)
+{
+ int __traces_domain_return;
+ {
+ int __retres;
+ {
+ int tmp;
+ tmp = 4;
+ /*@ assert tmp ≢ 0; */
+ g = tmp;
+ __retres = g + 1;
+ __traces_domain_return = __retres;
+ }
+ }
+ return __traces_domain_return;
+}
+
+
diff --git a/tests/value/traces/oracle/test4.res.oracle b/tests/value/traces/oracle/test4.res.oracle
index 7cb901ea75e..f8b7c0adf4e 100644
--- a/tests/value/traces/oracle/test4.res.oracle
+++ b/tests/value/traces/oracle/test4.res.oracle
@@ -4,33 +4,256 @@
[value] Initial state computed
[value:initial-state] Values of globals at initialization
+tests/value/traces/test4.i:9:[value] entering loop for the first time
+tests/value/traces/test4.i:11:[value] warning: signed overflow. assert tmp + 1 ≤ 2147483647;
+tests/value/traces/test4.i:14:[value] warning: signed overflow. assert tmp + 1 ≤ 2147483647;
+tests/value/traces/test4.i:17:[value] warning: signed overflow. assert tmp + 1 ≤ 2147483647;
+tests/value/traces/test4.i:20:[value] warning: signed overflow. assert tmp + 1 ≤ 2147483647;
+tests/value/traces/test4.i:23:[value] warning: signed overflow. assert tmp + 1 ≤ 2147483647;
+tests/value/traces/test4.i:25:[value] warning: signed overflow. assert tmp + 1 ≤ 2147483647;
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
- tmp ∈ {3}
+ tmp ∈ [46..2147483647]
[value:d-traces] Trace domains:
start: 0; globals = ; main_formals = c;
- {[ 0 -> ([ initialize variable using type Main_Formal
-c -> 1 ])
- 1 -> ([ EnterScope: tmp -> 2 ])
- 2 -> ([ initialize variable: tmp -> 3 ])
- 3 -> ([ Assign: tmp = 0 -> 4 ])
- 4 -> ([ EnterScope: i -> 5 ])
- 5 -> ([ initialize variable: i -> 6 ])
- 6 -> ([ Assign: i = 0 -> 7 ])
- 7 -> ([ enter_loop -> 8 ])
- 8 -> ([ Assume: i < 3 true -> 9 ])
- 9 -> ([ Assign: tmp = tmp + 1 -> 10 ])
- 10 -> ([ Assign: i = i + 1 -> 11 ])
- 11 -> ([ Assume: i < 3 true -> 13 ])
- 13 -> ([ Assign: tmp = tmp + 1 -> 14 ])
- 14 -> ([ Assign: i = i + 1 -> 15 ])
- 15 -> ([ Assume: i < 3 true -> 18 ])
- 18 -> ([ Assign: tmp = tmp + 1 -> 19 ])
- 19 -> ([ Assign: i = i + 1 -> 20 ])
- 20 -> ([ Assume: i < 3 false -> 23 ])
- 23 -> ([ LeaveScope: i -> 24 ]) ]} at 24
+ {[ 0 -> initialize variable using type Main_Formal
+c -> 1
+ 1 -> EnterScope: tmp -> 2
+ 2 -> initialize variable: tmp -> 3
+ 3 -> Assign: tmp = 0 -> 4
+ 4 -> EnterScope: i -> 5
+ 5 -> initialize variable: i -> 6
+ 6 -> Assign: i = 0 -> 7
+ 7 -> enter_loop -> 8
+ 8 -> Assume: i < 100 true -> 9
+ 9 -> Assume: i % 2 false -> 10
+ 10 -> Assume: i % 3 false -> 11
+ 11 -> Assume: i % 5 false -> 12
+ 12 -> Assume: i % 7 false -> 13
+ 13 -> Assume: i % 11 false -> 14
+ 14 -> Assign: tmp = tmp + 1 -> 15
+ 15 -> Assign: i = i + 1 -> 16
+ 16 -> Assume: i < 100 true -> 18
+ 18 -> Assume: i % 2 true -> 19
+ 19 -> Assign: tmp = tmp + 1 -> 20
+ 20 -> Assume: i % 3 true -> 21
+ 21 -> Assign: tmp = tmp + 1 -> 22
+ 22 -> Assume: i % 5 true -> 23
+ 23 -> Assign: tmp = tmp + 1 -> 24
+ 24 -> Assume: i % 7 true -> 25
+ 25 -> Assign: tmp = tmp + 1 -> 26
+ 26 -> Assume: i % 11 true -> 27
+ 27 -> Assign: tmp = tmp + 1 -> 28
+ 28 -> Assign: tmp = tmp + 1 -> 29
+ 29 -> Assign: i = i + 1 -> 30
+ 30 -> Assume: i < 100 true -> 33
+ 33 -> Assume: i % 2 false -> 34
+ 34 -> Assume: i % 3 true -> 35
+ 35 -> Assign: tmp = tmp + 1 -> 36
+ 36 -> Assume: i % 5 true -> 38
+ 38 -> Assign: tmp = tmp + 1 -> 39
+ 39 -> Assume: i % 7 true -> 41
+ 41 -> Assign: tmp = tmp + 1 -> 42
+ 42 -> Assume: i % 11 true -> 44
+ 44 -> Assign: tmp = tmp + 1 -> 45
+ 45 -> Assign: tmp = tmp + 1 -> 47
+ 47 -> Assign: i = i + 1 -> 48
+ 48 -> Assume: i < 100 true -> 51
+ 51 -> Assume: i % 2 true -> 52
+ 52 -> Assign: tmp = tmp + 1 -> 53
+ 53 -> Assume: i % 3 false -> 55
+ 55 -> Assume: i % 5 true -> 56
+ 56 -> Assign: tmp = tmp + 1 -> 57
+ 57 -> Assume: i % 7 true -> 59
+ 59 -> Assign: tmp = tmp + 1 -> 60
+ 60 -> Assume: i % 11 true -> 62
+ 62 -> Assign: tmp = tmp + 1 -> 63
+ 63 -> Assign: tmp = tmp + 1 -> 65
+ 65 -> Assign: i = i + 1 -> 66
+ 66 -> Assume: i < 100 true -> 69
+ 69 -> Assume: i % 2 false -> 70
+ 70 -> Assume: i % 3 true -> 71
+ 71 -> Assign: tmp = tmp + 1 -> 72
+ 72 -> Assume: i % 5 true -> 74
+ 74 -> Assign: tmp = tmp + 1 -> 75
+ 75 -> Assume: i % 7 true -> 77
+ 77 -> Assign: tmp = tmp + 1 -> 78
+ 78 -> Assume: i % 11 true -> 80
+ 80 -> Assign: tmp = tmp + 1 -> 81
+ 81 -> Assign: tmp = tmp + 1 -> 83
+ 83 -> Assign: i = i + 1 -> 84
+ 84 -> Assume: i < 100 true -> 87
+ 87 -> Assume: i % 2 true -> 88
+ 88 -> Assign: tmp = tmp + 1 -> 89
+ 89 -> Assume: i % 3 true -> 91
+ 91 -> Assign: tmp = tmp + 1 -> 92
+ 92 -> Assume: i % 5 false -> 94
+ 94 -> Assume: i % 7 true -> 95
+ 95 -> Assign: tmp = tmp + 1 -> 96
+ 96 -> Assume: i % 11 true -> 98
+ 98 -> Assign: tmp = tmp + 1 -> 99
+ 99 -> Assign: tmp = tmp + 1 -> 101
+ 101 -> Assign: i = i + 1 -> 102
+ 102 -> Assume: i < 100 true -> 105
+ 105 -> Assume: i % 2 false -> 106
+ 106 -> Assume: i % 3 false -> 107
+ 107 -> Assume: i % 5 true -> 108
+ 108 -> Assign: tmp = tmp + 1 -> 109
+ 109 -> Assume: i % 7 true -> 111
+ 111 -> Assign: tmp = tmp + 1 -> 112
+ 112 -> Assume: i % 11 true -> 114
+ 114 -> Assign: tmp = tmp + 1 -> 115
+ 115 -> Assign: tmp = tmp + 1 -> 117
+ 117 -> Assign: i = i + 1 -> 118
+ 118 -> Assume: i < 100 true -> 121
+ 121 -> Assume: i % 2 true -> 122
+ 122 -> Assign: tmp = tmp + 1 -> 123
+ 123 -> Assume: i % 3 true -> 125
+ 125 -> Assign: tmp = tmp + 1 -> 126
+ 126 -> Assume: i % 5 true -> 128
+ 128 -> Assign: tmp = tmp + 1 -> 129
+ 129 -> Assume: i % 7 false -> 131
+ 131 -> Assume: i % 11 true -> 132
+ 132 -> Assign: tmp = tmp + 1 -> 133
+ 133 -> Assign: tmp = tmp + 1 -> 135
+ 135 -> Assign: i = i + 1 -> 136
+ 136 -> Assume: i < 100 true -> 139
+ 139 -> Assume: i % 2 false -> 140
+ 140 -> Assume: i % 3 true -> 141
+ 141 -> Assign: tmp = tmp + 1 -> 142
+ 142 -> Assume: i % 5 true -> 144
+ 144 -> Assign: tmp = tmp + 1 -> 145
+ 145 -> Assume: i % 7 true -> 147
+ 147 -> Assign: tmp = tmp + 1 -> 148
+ 148 -> Assume: i % 11 true -> 150
+ 150 -> Assign: tmp = tmp + 1 -> 151
+ 151 -> Assign: tmp = tmp + 1 -> 153
+ 153 -> Assign: i = i + 1 -> 154
+ 154 -> Assume: i < 100 true -> 157
+ 157 -> Assume: i % 2 true -> 158
+ 158 -> Assign: tmp = tmp + 1 -> 159
+ 159 -> Assume: i % 3 false -> 161
+ 161 -> Assume: i % 5 true -> 162
+ 162 -> Assign: tmp = tmp + 1 -> 163
+ 163 -> Assume: i % 7 true -> 165
+ 165 -> Assign: tmp = tmp + 1 -> 166
+ 166 -> Assume: i % 11 true -> 168
+ 168 -> Assign: tmp = tmp + 1 -> 169
+ 169 -> Assign: tmp = tmp + 1 -> 171
+ 171 -> Assign: i = i + 1 -> 172
+ 172 -> Assume: i < 100 true -> 175; join -> 190
+ 175 -> Assume: i % 2 false -> 176; join -> 193
+ 176 -> Assume: i % 3 true -> 177; join -> 199
+ 177 -> Assign: tmp = tmp + 1 -> 178
+ 178 -> Assume: i % 5 false -> 180; join -> 203
+ 180 -> Assume: i % 7 true -> 181; join -> 209
+ 181 -> Assign: tmp = tmp + 1 -> 182
+ 182 -> Assume: i % 11 true -> 184; join -> 213
+ 184 -> Assign: tmp = tmp + 1 -> 185
+ 185 -> Assign: tmp = tmp + 1 -> 187; join -> 219
+ 187 -> Assign: i = i + 1 -> 188; join -> 221
+ 188 -> join -> 190
+ 190 -> Assume: i < 100 true -> 192; join -> 224
+ 192 -> join -> 193
+ 193 -> Assume: i % 2 false -> 194; Assume: i % 2 true -> 195; join -> 227
+ 194 -> join -> 198
+ 195 -> Assign: tmp = tmp + 1 -> 196
+ 196 -> join -> 198
+ 198 -> join -> 199
+ 199 -> Assume: i % 3 true -> 200; join -> 233
+ 200 -> Assign: tmp = tmp + 1 -> 201
+ 201 -> join -> 203
+ 203 -> Assume: i % 5 false -> 204; Assume: i % 5 true -> 205; join -> 239
+ 204 -> join -> 208
+ 205 -> Assign: tmp = tmp + 1 -> 206
+ 206 -> join -> 208
+ 208 -> join -> 209
+ 209 -> Assume: i % 7 true -> 210; join -> 245
+ 210 -> Assign: tmp = tmp + 1 -> 211
+ 211 -> join -> 213
+ 213 -> Assume: i % 11 false -> 214; Assume: i % 11 true -> 215;
+ join -> 249
+ 214 -> join -> 218
+ 215 -> Assign: tmp = tmp + 1 -> 216; join -> 252
+ 216 -> join -> 218
+ 218 -> join -> 219
+ 219 -> Assign: tmp = tmp + 1 -> 220; join -> 256
+ 220 -> join -> 221
+ 221 -> Assign: i = i + 1 -> 222; join -> 258
+ 222 -> join -> 224
+ 224 -> Assume: i < 100 true -> 226; join -> 261
+ 226 -> join -> 227
+ 227 -> Assume: i % 2 false -> 228; Assume: i % 2 true -> 229; join -> 265
+ 228 -> join -> 232
+ 229 -> Assign: tmp = tmp + 1 -> 230
+ 230 -> join -> 232
+ 232 -> join -> 233
+ 233 -> Assume: i % 3 false -> 234; Assume: i % 3 true -> 235; join -> 271
+ 234 -> join -> 238
+ 235 -> Assign: tmp = tmp + 1 -> 236
+ 236 -> join -> 238
+ 238 -> join -> 239
+ 239 -> Assume: i % 5 false -> 240; Assume: i % 5 true -> 241; join -> 277
+ 240 -> join -> 244
+ 241 -> Assign: tmp = tmp + 1 -> 242
+ 242 -> join -> 244
+ 244 -> join -> 245
+ 245 -> Assume: i % 7 true -> 246; join -> 283
+ 246 -> Assign: tmp = tmp + 1 -> 247; join -> 286
+ 247 -> join -> 249
+ 249 -> Assume: i % 11 false -> 250; Assume: i % 11 true -> 251;
+ join -> 290
+ 250 -> join -> 255
+ 251 -> join -> 252
+ 252 -> Assign: tmp = tmp + 1 -> 253; join -> 293
+ 253 -> join -> 255
+ 255 -> join -> 256
+ 256 -> Assign: tmp = tmp + 1 -> 257; join -> 297
+ 257 -> join -> 258
+ 258 -> Assign: i = i + 1 -> 259; join -> 299
+ 259 -> join -> 261
+ 261 -> join -> 265
+ 265 -> join -> 271
+ 271 -> join -> 277
+ 277 -> join -> 283
+ 283 -> join -> 286
+ 286 -> join -> 290
+ 290 -> join -> 293
+ 293 -> join -> 297
+ 297 -> join -> 299
+ 299 -> Loop(4) 262 {[ 262 -> Assume: i < 100 true -> 264
+ 264 -> Assume: i % 2 false -> 266;
+ Assume: i % 2 true -> 267
+ 266 -> join -> 270
+ 267 -> Assign: tmp = tmp + 1 -> 268
+ 268 -> join -> 270
+ 270 -> Assume: i % 3 false -> 272;
+ Assume: i % 3 true -> 273
+ 272 -> join -> 276
+ 273 -> Assign: tmp = tmp + 1 -> 274
+ 274 -> join -> 276
+ 276 -> Assume: i % 5 false -> 278;
+ Assume: i % 5 true -> 279
+ 278 -> join -> 282
+ 279 -> Assign: tmp = tmp + 1 -> 280
+ 280 -> join -> 282
+ 282 -> Assume: i % 7 false -> 284;
+ Assume: i % 7 true -> 285
+ 284 -> join -> 289
+ 285 -> Assign: tmp = tmp + 1 -> 287
+ 287 -> join -> 289
+ 289 -> Assume: i % 11 false -> 291;
+ Assume: i % 11 true -> 292
+ 291 -> join -> 296
+ 292 -> Assign: tmp = tmp + 1 -> 294
+ 294 -> join -> 296
+ 296 -> Assign: tmp = tmp + 1 -> 298
+ 298 -> Assign: i = i + 1 -> 300 ]} -> 304
+ 304 -> Assume: i < 100 false -> 305
+ 305 -> leave_loop -> 306
+ 306 -> LeaveScope: i -> 312 ]} at 312
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
@@ -42,42 +265,3 @@ c -> 1 ])
tmp; i
[inout] Inputs for function main:
\nothing
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value:initial-state] Values of globals at initialization
-
-[value] done for function main
-[value] ====== VALUES COMPUTED ======
-[value:final-states] Values at end of function main:
- __traces_domain_return ∈ {3}
-[value:d-traces] Trace domains:
- TOP
-[value] failure: The trace is TOP can't generate code
-/* Generated by Frama-C */
-int main(int c)
-{
- int __traces_domain_return;
- {
- int tmp;
- tmp = 0;
- {
- int i;
- i = 0;
- /*@ assert i < 3; */
- tmp ++;
- i ++;
- /*@ assert i < 3; */
- tmp ++;
- i ++;
- /*@ assert i < 3; */
- tmp ++;
- i ++;
- /*@ assert ¬(i < 3); */
- __traces_domain_return = tmp;
- }
- }
- return __traces_domain_return;
-}
-
-
diff --git a/tests/value/traces/oracle/test5.err.oracle b/tests/value/traces/oracle/test5.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/traces/oracle/test5.res.oracle b/tests/value/traces/oracle/test5.res.oracle
new file mode 100644
index 00000000000..9c6a9068b06
--- /dev/null
+++ b/tests/value/traces/oracle/test5.res.oracle
@@ -0,0 +1,556 @@
+[kernel] Parsing tests/value/traces/test5.i (no preprocessing)
+tests/value/traces/test5.i:21:[kernel] warning: Calling undeclared function my_switch. Old style K&R code?
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value:initial-state] Values of globals at initialization
+
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+tests/value/traces/test5.i:21:[kernel] warning: Neither code nor specification for function my_switch, generating default assigns from the prototype
+[value] using specification for function my_switch
+[value] Done for function my_switch
+tests/value/traces/test5.i:21:[value] warning: signed overflow.
+ assert tmp_0 + tmp ≤ 2147483647;
+ (tmp_0 from my_switch(tmp))
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+tests/value/traces/test5.i:21:[value] warning: signed overflow.
+ assert -2147483648 ≤ tmp_0 + tmp;
+ (tmp_0 from my_switch(tmp))
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+tests/value/traces/test5.i:20:[value] entering loop for the first time
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+tests/value/traces/test5.i:19:[value] entering loop for the first time
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+[value] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[value] Done for function my_switch
+[value] Recording results for main
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value:final-states] Values at end of function main:
+ tmp ∈ [--..--]
+[value:d-traces] Trace domains:
+ start: 0; globals = ; main_formals = c;
+ {[ 0 -> initialize variable using type Main_Formal
+c -> 1
+ 1 -> EnterScope: tmp -> 2
+ 2 -> initialize variable: tmp -> 3
+ 3 -> Assign: tmp = 1 -> 4
+ 4 -> EnterScope: i -> 5
+ 5 -> initialize variable: i -> 6
+ 6 -> Assign: i = 0 -> 7
+ 7 -> enter_loop -> 8
+ 8 -> Assume: i < 10 true -> 9
+ 9 -> EnterScope: j -> 10
+ 10 -> initialize variable: j -> 11
+ 11 -> Assign: j = 0 -> 12
+ 12 -> enter_loop -> 13
+ 13 -> Assume: j < 10 true -> 14
+ 14 -> EnterScope: tmp_0 -> 15
+ 15 -> EnterScope: \result<my_switch> -> 16
+ 16 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 17
+ 17 -> Assign: tmp_0 = \result<my_switch> -> 18
+ 18 -> LeaveScope: \result<my_switch> -> 19
+ 19 -> Assign: tmp = tmp_0 + tmp -> 20
+ 20 -> LeaveScope: tmp_0 -> 21
+ 21 -> Assign: j = j + 1 -> 22
+ 22 -> Assume: j < 10 true -> 24
+ 24 -> EnterScope: tmp_0 -> 25
+ 25 -> EnterScope: \result<my_switch> -> 26
+ 26 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 27
+ 27 -> Assign: tmp_0 = \result<my_switch> -> 29
+ 29 -> LeaveScope: \result<my_switch> -> 30
+ 30 -> Assign: tmp = tmp_0 + tmp -> 31
+ 31 -> LeaveScope: tmp_0 -> 33
+ 33 -> Assign: j = j + 1 -> 34
+ 34 -> Assume: j < 10 true -> 37
+ 37 -> EnterScope: tmp_0 -> 38
+ 38 -> EnterScope: \result<my_switch> -> 39
+ 39 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 40
+ 40 -> Assign: tmp_0 = \result<my_switch> -> 42
+ 42 -> LeaveScope: \result<my_switch> -> 43
+ 43 -> Assign: tmp = tmp_0 + tmp -> 44
+ 44 -> LeaveScope: tmp_0 -> 46
+ 46 -> Assign: j = j + 1 -> 47
+ 47 -> Assume: j < 10 true -> 50
+ 50 -> EnterScope: tmp_0 -> 51
+ 51 -> EnterScope: \result<my_switch> -> 52
+ 52 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 53
+ 53 -> Assign: tmp_0 = \result<my_switch> -> 55
+ 55 -> LeaveScope: \result<my_switch> -> 56
+ 56 -> Assign: tmp = tmp_0 + tmp -> 57
+ 57 -> LeaveScope: tmp_0 -> 59
+ 59 -> Assign: j = j + 1 -> 60
+ 60 -> Assume: j < 10 true -> 63
+ 63 -> EnterScope: tmp_0 -> 64
+ 64 -> EnterScope: \result<my_switch> -> 65
+ 65 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 66
+ 66 -> Assign: tmp_0 = \result<my_switch> -> 68
+ 68 -> LeaveScope: \result<my_switch> -> 69
+ 69 -> Assign: tmp = tmp_0 + tmp -> 70
+ 70 -> LeaveScope: tmp_0 -> 72
+ 72 -> Assign: j = j + 1 -> 73
+ 73 -> Assume: j < 10 true -> 76
+ 76 -> EnterScope: tmp_0 -> 77
+ 77 -> EnterScope: \result<my_switch> -> 78
+ 78 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 79
+ 79 -> Assign: tmp_0 = \result<my_switch> -> 81
+ 81 -> LeaveScope: \result<my_switch> -> 82
+ 82 -> Assign: tmp = tmp_0 + tmp -> 83
+ 83 -> LeaveScope: tmp_0 -> 85
+ 85 -> Assign: j = j + 1 -> 86
+ 86 -> Assume: j < 10 true -> 89
+ 89 -> EnterScope: tmp_0 -> 90
+ 90 -> EnterScope: \result<my_switch> -> 91
+ 91 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 92
+ 92 -> Assign: tmp_0 = \result<my_switch> -> 94
+ 94 -> LeaveScope: \result<my_switch> -> 95
+ 95 -> Assign: tmp = tmp_0 + tmp -> 96
+ 96 -> LeaveScope: tmp_0 -> 98
+ 98 -> Assign: j = j + 1 -> 99
+ 99 -> Assume: j < 10 true -> 102
+ 102 -> EnterScope: tmp_0 -> 103
+ 103 -> EnterScope: \result<my_switch> -> 104
+ 104 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 105
+ 105 -> Assign: tmp_0 = \result<my_switch> -> 107
+ 107 -> LeaveScope: \result<my_switch> -> 108
+ 108 -> Assign: tmp = tmp_0 + tmp -> 109
+ 109 -> LeaveScope: tmp_0 -> 111
+ 111 -> Assign: j = j + 1 -> 112
+ 112 -> Assume: j < 10 true -> 115
+ 115 -> EnterScope: tmp_0 -> 116
+ 116 -> EnterScope: \result<my_switch> -> 117
+ 117 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 118
+ 118 -> Assign: tmp_0 = \result<my_switch> -> 120
+ 120 -> LeaveScope: \result<my_switch> -> 121
+ 121 -> Assign: tmp = tmp_0 + tmp -> 122
+ 122 -> LeaveScope: tmp_0 -> 124
+ 124 -> Assign: j = j + 1 -> 125
+ 125 -> Assume: j < 10 true -> 128
+ 128 -> EnterScope: tmp_0 -> 129
+ 129 -> EnterScope: \result<my_switch> -> 130
+ 130 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 131
+ 131 -> Assign: tmp_0 = \result<my_switch> -> 133
+ 133 -> LeaveScope: \result<my_switch> -> 134
+ 134 -> Assign: tmp = tmp_0 + tmp -> 135
+ 135 -> LeaveScope: tmp_0 -> 137
+ 137 -> Assign: j = j + 1 -> 138
+ 138 -> Assume: j < 10 false -> 141; join -> 151
+ 141 -> LeaveScope: j -> 142
+ 142 -> Assign: i = i + 1 -> 143
+ 143 -> Assume: i < 10 true -> 145
+ 145 -> EnterScope: j -> 146
+ 146 -> initialize variable: j -> 147
+ 147 -> Assign: j = 0 -> 148
+ 148 -> enter_loop -> 150
+ 150 -> join -> 151
+ 151 -> Assume: j < 10 false -> 153; Assume: j < 10 true -> 154;
+ join -> 166
+ 153 -> LeaveScope: j -> 213
+ 154 -> EnterScope: tmp_0 -> 155; join -> 170
+ 155 -> EnterScope: \result<my_switch> -> 156; join -> 172
+ 156 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 157
+ 157 -> Assign: tmp_0 = \result<my_switch> -> 159
+ 159 -> LeaveScope: \result<my_switch> -> 160
+ 160 -> Assign: tmp = tmp_0 + tmp -> 161; join -> 178
+ 161 -> LeaveScope: tmp_0 -> 163
+ 163 -> Assign: j = j + 1 -> 164; join -> 182
+ 164 -> join -> 166
+ 166 -> Assume: j < 10 false -> 168; Assume: j < 10 true -> 169;
+ join -> 185
+ 168 -> LeaveScope: j -> 214
+ 169 -> join -> 170
+ 170 -> EnterScope: tmp_0 -> 171; join -> 192
+ 171 -> join -> 172
+ 172 -> EnterScope: \result<my_switch> -> 173; join -> 194
+ 173 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 174
+ 174 -> Assign: tmp_0 = \result<my_switch> -> 176
+ 176 -> LeaveScope: \result<my_switch> -> 177
+ 177 -> join -> 178
+ 178 -> Assign: tmp = tmp_0 + tmp -> 179; join -> 200
+ 179 -> LeaveScope: tmp_0 -> 181
+ 181 -> join -> 182
+ 182 -> Assign: j = j + 1 -> 183; join -> 204
+ 183 -> join -> 185
+ 185 -> Assume: j < 10 false -> 190; join -> 192
+ 190 -> leave_loop -> 191
+ 191 -> LeaveScope: j -> 215
+ 192 -> join -> 194
+ 194 -> join -> 200
+ 200 -> join -> 204
+ 204 -> join -> 256;
+ Loop(16) 186 {[ 186 -> Assume: j < 10 true -> 189
+ 189 -> EnterScope: tmp_0 -> 193
+ 193 -> EnterScope: \result<my_switch> -> 195
+ 195 -> CallDeclared:
+ \result<my_switch> =
+ my_switch(tmp) -> 196
+ 196 -> Assign: tmp_0 = \result<my_switch> -> 198
+ 198 -> LeaveScope: \result<my_switch> -> 199
+ 199 -> Assign: tmp = tmp_0 + tmp -> 201
+ 201 -> LeaveScope: tmp_0 -> 203
+ 203 -> Assign: j = j + 1 -> 205 ]} -> 208
+ 208 -> Assume: j < 10 false -> 209
+ 209 -> leave_loop -> 210
+ 210 -> LeaveScope: j -> 216
+ 213 -> Assign: i = i + 1 -> 217
+ 214 -> Assign: i = i + 1 -> 218
+ 215 -> Assign: i = i + 1 -> 219
+ 216 -> Assign: i = i + 1 -> 220
+ 217 -> Assume: i < 10 true -> 232
+ 218 -> Assume: i < 10 true -> 231
+ 219 -> Assume: i < 10 true -> 230
+ 220 -> Assume: i < 10 true -> 229
+ 229 -> EnterScope: j -> 242
+ 230 -> EnterScope: j -> 239
+ 231 -> EnterScope: j -> 236
+ 232 -> EnterScope: j -> 233
+ 233 -> initialize variable: j -> 234
+ 234 -> Assign: j = 0 -> 235
+ 235 -> enter_loop -> 252
+ 236 -> initialize variable: j -> 237
+ 237 -> Assign: j = 0 -> 238
+ 238 -> enter_loop -> 251
+ 239 -> initialize variable: j -> 240
+ 240 -> Assign: j = 0 -> 241
+ 241 -> enter_loop -> 250
+ 242 -> initialize variable: j -> 243
+ 243 -> Assign: j = 0 -> 244
+ 244 -> enter_loop -> 249
+ 249 -> join -> 253
+ 250 -> join -> 253
+ 251 -> join -> 254
+ 252 -> join -> 255
+ 253 -> join -> 254
+ 254 -> join -> 255
+ 255 -> join -> 256
+ 256 -> join -> 275;
+ Loop(16) 186 {[ 186 -> Assume: j < 10 true -> 189
+ 189 -> EnterScope: tmp_0 -> 193
+ 193 -> EnterScope: \result<my_switch> -> 195
+ 195 -> CallDeclared:
+ \result<my_switch> =
+ my_switch(tmp) -> 196
+ 196 -> Assign: tmp_0 = \result<my_switch> -> 198
+ 198 -> LeaveScope: \result<my_switch> -> 199
+ 199 -> Assign: tmp = tmp_0 + tmp -> 201
+ 201 -> LeaveScope: tmp_0 -> 203
+ 203 -> Assign: j = j + 1 -> 205 ]} -> 258
+ 258 -> Assume: j < 10 false -> 259
+ 259 -> leave_loop -> 260
+ 260 -> LeaveScope: j -> 264
+ 264 -> Assign: i = i + 1 -> 265
+ 265 -> Assume: i < 10 false -> 268; Assume: i < 10 true -> 269
+ 268 -> LeaveScope: i -> 443
+ 269 -> EnterScope: j -> 270
+ 270 -> initialize variable: j -> 271
+ 271 -> Assign: j = 0 -> 272
+ 272 -> enter_loop -> 274
+ 274 -> join -> 275
+ 275 -> join -> 294;
+ Loop(16) 186 {[ 186 -> Assume: j < 10 true -> 189
+ 189 -> EnterScope: tmp_0 -> 193
+ 193 -> EnterScope: \result<my_switch> -> 195
+ 195 -> CallDeclared:
+ \result<my_switch> =
+ my_switch(tmp) -> 196
+ 196 -> Assign: tmp_0 = \result<my_switch> -> 198
+ 198 -> LeaveScope: \result<my_switch> -> 199
+ 199 -> Assign: tmp = tmp_0 + tmp -> 201
+ 201 -> LeaveScope: tmp_0 -> 203
+ 203 -> Assign: j = j + 1 -> 205 ]} -> 277
+ 277 -> Assume: j < 10 false -> 278
+ 278 -> leave_loop -> 279
+ 279 -> LeaveScope: j -> 283
+ 283 -> Assign: i = i + 1 -> 284
+ 284 -> Assume: i < 10 false -> 287; Assume: i < 10 true -> 288
+ 287 -> LeaveScope: i -> 444
+ 288 -> EnterScope: j -> 289
+ 289 -> initialize variable: j -> 290
+ 290 -> Assign: j = 0 -> 291
+ 291 -> enter_loop -> 293
+ 293 -> join -> 294
+ 294 -> join -> 313;
+ Loop(16) 186 {[ 186 -> Assume: j < 10 true -> 189
+ 189 -> EnterScope: tmp_0 -> 193
+ 193 -> EnterScope: \result<my_switch> -> 195
+ 195 -> CallDeclared:
+ \result<my_switch> =
+ my_switch(tmp) -> 196
+ 196 -> Assign: tmp_0 = \result<my_switch> -> 198
+ 198 -> LeaveScope: \result<my_switch> -> 199
+ 199 -> Assign: tmp = tmp_0 + tmp -> 201
+ 201 -> LeaveScope: tmp_0 -> 203
+ 203 -> Assign: j = j + 1 -> 205 ]} -> 296
+ 296 -> Assume: j < 10 false -> 297
+ 297 -> leave_loop -> 298
+ 298 -> LeaveScope: j -> 302
+ 302 -> Assign: i = i + 1 -> 303
+ 303 -> Assume: i < 10 false -> 306; Assume: i < 10 true -> 307
+ 306 -> LeaveScope: i -> 445
+ 307 -> EnterScope: j -> 308
+ 308 -> initialize variable: j -> 309
+ 309 -> Assign: j = 0 -> 310
+ 310 -> enter_loop -> 312
+ 312 -> join -> 313
+ 313 -> join -> 332;
+ Loop(16) 186 {[ 186 -> Assume: j < 10 true -> 189
+ 189 -> EnterScope: tmp_0 -> 193
+ 193 -> EnterScope: \result<my_switch> -> 195
+ 195 -> CallDeclared:
+ \result<my_switch> =
+ my_switch(tmp) -> 196
+ 196 -> Assign: tmp_0 = \result<my_switch> -> 198
+ 198 -> LeaveScope: \result<my_switch> -> 199
+ 199 -> Assign: tmp = tmp_0 + tmp -> 201
+ 201 -> LeaveScope: tmp_0 -> 203
+ 203 -> Assign: j = j + 1 -> 205 ]} -> 315
+ 315 -> Assume: j < 10 false -> 316
+ 316 -> leave_loop -> 317
+ 317 -> LeaveScope: j -> 321
+ 321 -> Assign: i = i + 1 -> 322
+ 322 -> Assume: i < 10 false -> 325; Assume: i < 10 true -> 326
+ 325 -> LeaveScope: i -> 446
+ 326 -> EnterScope: j -> 327
+ 327 -> initialize variable: j -> 328
+ 328 -> Assign: j = 0 -> 329
+ 329 -> enter_loop -> 331
+ 331 -> join -> 332
+ 332 -> join -> 351;
+ Loop(16) 186 {[ 186 -> Assume: j < 10 true -> 189
+ 189 -> EnterScope: tmp_0 -> 193
+ 193 -> EnterScope: \result<my_switch> -> 195
+ 195 -> CallDeclared:
+ \result<my_switch> =
+ my_switch(tmp) -> 196
+ 196 -> Assign: tmp_0 = \result<my_switch> -> 198
+ 198 -> LeaveScope: \result<my_switch> -> 199
+ 199 -> Assign: tmp = tmp_0 + tmp -> 201
+ 201 -> LeaveScope: tmp_0 -> 203
+ 203 -> Assign: j = j + 1 -> 205 ]} -> 334
+ 334 -> Assume: j < 10 false -> 335
+ 335 -> leave_loop -> 336
+ 336 -> LeaveScope: j -> 340
+ 340 -> Assign: i = i + 1 -> 341
+ 341 -> Assume: i < 10 false -> 344; Assume: i < 10 true -> 345;
+ join -> 362
+ 344 -> LeaveScope: i -> 447
+ 345 -> EnterScope: j -> 346; join -> 366
+ 346 -> initialize variable: j -> 347
+ 347 -> Assign: j = 0 -> 348
+ 348 -> enter_loop -> 350
+ 350 -> join -> 351
+ 351 -> join -> 372;
+ Loop(16) 186 {[ 186 -> Assume: j < 10 true -> 189
+ 189 -> EnterScope: tmp_0 -> 193
+ 193 -> EnterScope: \result<my_switch> -> 195
+ 195 -> CallDeclared:
+ \result<my_switch> =
+ my_switch(tmp) -> 196
+ 196 -> Assign: tmp_0 = \result<my_switch> -> 198
+ 198 -> LeaveScope: \result<my_switch> -> 199
+ 199 -> Assign: tmp = tmp_0 + tmp -> 201
+ 201 -> LeaveScope: tmp_0 -> 203
+ 203 -> Assign: j = j + 1 -> 205 ]} -> 353
+ 353 -> Assume: j < 10 false -> 354
+ 354 -> leave_loop -> 355
+ 355 -> LeaveScope: j -> 359; join -> 380
+ 359 -> Assign: i = i + 1 -> 360; join -> 382
+ 360 -> join -> 362
+ 362 -> Assume: i < 10 false -> 364; Assume: i < 10 true -> 365;
+ join -> 385
+ 364 -> LeaveScope: i -> 448
+ 365 -> join -> 366
+ 366 -> EnterScope: j -> 367; join -> 389
+ 367 -> initialize variable: j -> 368
+ 368 -> Assign: j = 0 -> 369
+ 369 -> enter_loop -> 371
+ 371 -> join -> 372
+ 372 -> join -> 395;
+ Loop(16) 186 {[ 186 -> Assume: j < 10 true -> 189
+ 189 -> EnterScope: tmp_0 -> 193
+ 193 -> EnterScope: \result<my_switch> -> 195
+ 195 -> CallDeclared:
+ \result<my_switch> =
+ my_switch(tmp) -> 196
+ 196 -> Assign: tmp_0 = \result<my_switch> -> 198
+ 198 -> LeaveScope: \result<my_switch> -> 199
+ 199 -> Assign: tmp = tmp_0 + tmp -> 201
+ 201 -> LeaveScope: tmp_0 -> 203
+ 203 -> Assign: j = j + 1 -> 205 ]} -> 374
+ 374 -> Assume: j < 10 false -> 375
+ 375 -> leave_loop -> 376
+ 376 -> join -> 380
+ 380 -> LeaveScope: j -> 381; join -> 403
+ 381 -> join -> 382
+ 382 -> Assign: i = i + 1 -> 383; join -> 405
+ 383 -> join -> 385
+ 385 -> Assume: i < 10 false -> 387; Assume: i < 10 true -> 388;
+ join -> 408
+ 387 -> LeaveScope: i -> 449
+ 388 -> join -> 389
+ 389 -> EnterScope: j -> 390; join -> 415
+ 390 -> initialize variable: j -> 391
+ 391 -> Assign: j = 0 -> 392
+ 392 -> enter_loop -> 394
+ 394 -> join -> 395
+ 395 -> join -> 421;
+ Loop(16) 186 {[ 186 -> Assume: j < 10 true -> 189
+ 189 -> EnterScope: tmp_0 -> 193
+ 193 -> EnterScope: \result<my_switch> -> 195
+ 195 -> CallDeclared:
+ \result<my_switch> =
+ my_switch(tmp) -> 196
+ 196 -> Assign: tmp_0 = \result<my_switch> -> 198
+ 198 -> LeaveScope: \result<my_switch> -> 199
+ 199 -> Assign: tmp = tmp_0 + tmp -> 201
+ 201 -> LeaveScope: tmp_0 -> 203
+ 203 -> Assign: j = j + 1 -> 205 ]} -> 397
+ 397 -> Assume: j < 10 false -> 398
+ 398 -> leave_loop -> 399
+ 399 -> join -> 403
+ 403 -> LeaveScope: j -> 404; join -> 429
+ 404 -> join -> 405
+ 405 -> Assign: i = i + 1 -> 406; join -> 431
+ 406 -> join -> 408
+ 408 -> Assume: i < 10 false -> 413; join -> 415
+ 413 -> leave_loop -> 414
+ 414 -> LeaveScope: i -> 450
+ 415 -> join -> 421
+ 421 -> join -> 429
+ 429 -> join -> 431
+ 431 -> Loop(10) 409 {[ 409 -> Assume: i < 10 true -> 412
+ 412 -> EnterScope: j -> 416
+ 416 -> initialize variable: j -> 417
+ 417 -> Assign: j = 0 -> 418
+ 418 -> enter_loop -> 420
+ 420 -> Loop(16) 186 {[ 186 -> Assume:
+ j < 10 true
+ -> 189
+ 189 -> EnterScope:
+ tmp_0 -> 193
+ 193 -> EnterScope:
+ \result<my_switch>
+ -> 195
+ 195 -> CallDeclared:
+ \result<my_switch> =
+ my_switch(
+ tmp) -> 196
+ 196 -> Assign:
+ tmp_0 = \result<my_switch>
+ -> 198
+ 198 -> LeaveScope:
+ \result<my_switch>
+ -> 199
+ 199 -> Assign:
+ tmp = tmp_0 + tmp
+ -> 201
+ 201 -> LeaveScope:
+ tmp_0 -> 203
+ 203 -> Assign:
+ j = j + 1
+ -> 205 ]}
+ -> 423
+ 423 -> Assume: j < 10 false -> 424
+ 424 -> leave_loop -> 425
+ 425 -> LeaveScope: j -> 430
+ 430 -> Assign: i = i + 1 -> 432 ]} -> 435
+ 435 -> Assume: i < 10 false -> 436
+ 436 -> leave_loop -> 437
+ 437 -> LeaveScope: i -> 451
+ 443 -> join -> 459
+ 444 -> join -> 458
+ 445 -> join -> 457
+ 446 -> join -> 456
+ 447 -> join -> 455
+ 448 -> join -> 454
+ 449 -> join -> 453
+ 450 -> join -> 452
+ 451 -> join -> 452
+ 452 -> join -> 453
+ 453 -> join -> 454
+ 454 -> join -> 455
+ 455 -> join -> 456
+ 456 -> join -> 457
+ 457 -> join -> 458
+ 458 -> join -> 459 ]} at 459
+[from] Computing for function main
+[from] Computing for function my_switch <-main
+[from] Done for function my_switch
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function my_switch:
+ \result FROM x_0
+[from] Function main:
+ \result FROM \nothing
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main:
+ tmp; i; j; tmp_0
+[inout] Inputs for function main:
+ \nothing
+[kernel] user error: no known last created project.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/value/traces/test1.c b/tests/value/traces/test1.c
index 8b3966a6150..7fbd4347cc7 100644
--- a/tests/value/traces/test1.c
+++ b/tests/value/traces/test1.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10" +"-then-last -val -print"
+ STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10 -eva-traces-project" +"-then-last -val -print -value-msg-key=-d-traces"
*/
extern volatile int entropy_source;
diff --git a/tests/value/traces/test2.i b/tests/value/traces/test2.i
index 8d34b91c868..6369b92fd4c 100644
--- a/tests/value/traces/test2.i
+++ b/tests/value/traces/test2.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10" +"-then-last -check -print -val"
+ STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10 -eva-traces-project" +"-then-last -val -print -value-msg-key=-d-traces"
*/
diff --git a/tests/value/traces/test3.i b/tests/value/traces/test3.i
index 6eab55ed2c2..6cd21d4315d 100644
--- a/tests/value/traces/test3.i
+++ b/tests/value/traces/test3.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10" +"-then-last -val"
+ STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10 -eva-traces-project" +"-then-last -val -print -value-msg-key=-d-traces"
*/
int g;
diff --git a/tests/value/traces/test4.i b/tests/value/traces/test4.i
index 9a95eac246a..9d4bc60920a 100644
--- a/tests/value/traces/test4.i
+++ b/tests/value/traces/test4.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10" +"-then-last -val -slevel 10 -print -no-eva-traces-domain"
+ STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10"
*/
/* Test of join inside a loop */
@@ -10,7 +10,6 @@ int main(c){
if(i % 2){
tmp ++;
};
- //@ slevel merge;
if(i % 3){
tmp ++;
};
diff --git a/tests/value/traces/test5.i b/tests/value/traces/test5.i
new file mode 100644
index 00000000000..046cafc6515
--- /dev/null
+++ b/tests/value/traces/test5.i
@@ -0,0 +1,25 @@
+/* run.config
+ STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10" +"-then-last -val -slevel 10 -print -no-eva-traces-domain"
+*/
+
+
+/* Check the fix for the creation of expression by dataflows2 for
+ switch (conversion to list of if) */
+
+int myswitch(i){
+ switch(i){
+ case 0: return 0;
+ case 1: return 1;
+ default: return 2;
+ }
+}
+
+int main(c){
+ int tmp = 1;
+ for(int i = 0; i < 10; i++){
+ for(int j = 0; j < 10; j++){
+ tmp = my_switch(tmp) + tmp;
+ }
+ }
+ return tmp;
+}
--
GitLab