From aa6498ca54432f2032d0341812dd83e8ff938606 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 3 Oct 2017 23:37:59 +0200
Subject: [PATCH] [Eva] fixes widening mode
---
.../value/domains/traces/traces_domain.ml | 229 +++++++++++-------
tests/value/traces/oracle/test1.res.oracle | 225 ++++++++---------
tests/value/traces/oracle/test2.res.oracle | 137 +++++------
tests/value/traces/oracle/test3.res.oracle | 12 +-
tests/value/traces/oracle/test4.res.oracle | 106 +++-----
tests/value/traces/test1.c | 6 +-
6 files changed, 360 insertions(+), 355 deletions(-)
diff --git a/src/plugins/value/domains/traces/traces_domain.ml b/src/plugins/value/domains/traces/traces_domain.ml
index 2b894d1d42c..08d003bee74 100644
--- a/src/plugins/value/domains/traces/traces_domain.ml
+++ b/src/plugins/value/domains/traces/traces_domain.ml
@@ -23,6 +23,8 @@
module Frama_c_File = File
open Cil_datatype
+let loop_mode_at_enter_loop = false
+
[@@@ warning "-40-42"]
module Node : sig
@@ -144,7 +146,7 @@ module Edge = struct
(Pretty_utils.pp_list ~sep:",@ " Exp.pretty) exp1
Node.pretty n
| Msg(n,s) -> Format.fprintf fmt "@[%s -> %a@]" s Node.pretty n
- | Loop(n,_,s,g) -> Format.fprintf fmt "@[<hv 2>@[Loop(%a)@] %a @[-> %a@]"
+ | Loop(n,_,s,g) -> Format.fprintf fmt "@[<hv 2>@[Loop(%a)@] %a @[-> %a@]@]"
Node.pretty s
(GraphShape.pretty (Pretty_utils.pp_list pretty)) g Node.pretty n
@@ -197,6 +199,7 @@ module Graph =
type loops =
| Base of Node.t * Graph.t (* current last *)
| OpenLoop of Cil_types.stmt * Node.t (* start node *) * Graph.t (* last iteration *) * Node.t (** current *) * Graph.t * loops
+ | UnrollLoop of Cil_types.stmt * loops
type state = { start : Node.t; current : loops;
call_declared_function: bool;
@@ -233,8 +236,25 @@ module Traces = struct
let c = Graph.compare g1 g2 in
if c <> 0 then c else
compare_loops l1 l2
+ | UnrollLoop(stmt1,l1), UnrollLoop(stmt2,l2) ->
+ let c = Stmt.compare stmt1 stmt2 in
+ if c <> 0 then c else
+ compare_loops l1 l2
| Base _, _ -> -1
| _, Base _ -> 1
+ | OpenLoop _, _ -> -1
+ | _, OpenLoop _ -> 1
+
+ let rec pretty_loops fmt = function
+ | Base (c,g) ->
+ Format.fprintf fmt "@[<hv>%a @[at %a@]@]"
+ Graph.pretty g Node.pretty c
+ | OpenLoop(_,s,_,c,g,l) ->
+ Format.fprintf fmt "@[<hv>@[start %a@]@ %a @[at %a@]@]@ %a"
+ Node.pretty s Graph.pretty g Node.pretty c pretty_loops l
+ | UnrollLoop(_,l) ->
+ Format.fprintf fmt "@[<hv>@[unroll@]@ %a"
+ pretty_loops l
(* Frama-C "datatype" for type [inout] *)
include Datatype.Make_with_collections(struct
@@ -265,14 +285,6 @@ module Traces = struct
let equal = Datatype.from_compare
- let rec pretty_loops fmt = function
- | Base (c,g) ->
- Format.fprintf fmt "@[<hv>%a @[at %a@]@]"
- Graph.pretty g Node.pretty c
- | OpenLoop(_,s,_,c,g,l) ->
- Format.fprintf fmt "@[<hv>@[start %a@]@ %a @[at %a@]@]@ %a"
- Node.pretty s Graph.pretty g Node.pretty c pretty_loops l
-
let pretty fmt m =
if m == top then Format.fprintf fmt "TOP"
else
@@ -287,6 +299,9 @@ module Traces = struct
| OpenLoop(stmt,s,last,c,g,l) ->
Hashtbl.seeded_hash 2
(Stmt.hash stmt, Node.hash s, Graph.hash last, Node.hash c, Graph.hash g, hash_loops l)
+ | UnrollLoop(stmt,l) ->
+ Hashtbl.seeded_hash 2
+ (Stmt.hash stmt, hash_loops l)
let hash m =
Hashtbl.seeded_hash (Node.hash m.start) (hash_loops m.current)
@@ -328,28 +343,39 @@ module Traces = struct
| Loop(n,_,_,_) -> n
let move_to c g state =
- let current = match state.current with
+ let rec aux = function
| Base (_,_) -> Base (c,g)
| OpenLoop(stmt,s,last,_,_,l) ->
- OpenLoop(stmt,s,last,c,g,l) in
+ OpenLoop(stmt,s,last,c,g,l)
+ | UnrollLoop(stmt,l) ->
+ UnrollLoop(stmt,aux l)
+ in
+ let current = aux state.current in
{state with current}
let replace_to c state =
- let current = match state.current with
+ let rec aux = function
| Base (_,g) -> Base (c,g)
| OpenLoop(stmt,s,last,_,g,l) ->
- OpenLoop(stmt,s,last,c,g,l) in
+ OpenLoop(stmt,s,last,c,g,l)
+ | UnrollLoop(stmt,l) -> UnrollLoop(stmt,aux l) in
+ let current = aux state.current in
{state with current}
let get_current state =
- match state.current with
+ let rec aux = function
| Base (c,g) -> (c,g)
| OpenLoop(_,_,_,c,g,_) -> (c,g)
+ | UnrollLoop(_,l) ->
+ aux l in
+ aux state.current
let get_last state =
- match state.current with
+ let rec aux = function
| Base (_,_) -> None
| OpenLoop(_,_,last,_,_,_) -> Some last
+ | UnrollLoop(_,l) -> aux l in
+ aux state.current
let find_succs current g =
match Graph.find current g with
@@ -370,43 +396,43 @@ module Traces = struct
else if c.call_declared_function then c (** forget intermediary state *)
else
let (current,graph) = get_current c in
+ let same edge' =
+ match edge, edge' with
+ | Assign (_,loc1,typ1,exp1), Assign (_,loc2,typ2,exp2) ->
+ let c = Lval.compare loc1 loc2 in
+ if c <> 0 then false else
+ let c = Typ.compare typ1 typ2 in
+ if c <> 0 then false else
+ Exp.compare exp1 exp2 = 0
+ | Assume(_,e1,b1), Assume(_,e2,b2) ->
+ let c = Exp.compare e1 e2 in
+ if c <> 0 then false else
+ Pervasives.compare b1 b2 = 0
+ | EnterScope(_,vs1),EnterScope(_,vs2) ->
+ let c = Extlib.list_compare Varinfo.compare vs1 vs2 in
+ c = 0
+ | LeaveScope(_,vs1), LeaveScope(_,vs2) ->
+ let c = Extlib.list_compare Varinfo.compare vs1 vs2 in
+ c = 0
+ | CallDeclared(_,kf1,exp1,lval1), CallDeclared(_,kf2,exp2,lval2) ->
+ let c = Kernel_function.compare kf1 kf2 in
+ if c <> 0 then false else
+ let c = Extlib.list_compare Exp.compare exp1 exp2 in
+ if c <> 0 then false else
+ let c = Extlib.opt_compare Lval.compare lval1 lval2 in
+ c = 0
+ | Msg(_,s1), Msg(_,s2) ->
+ let c = String.compare s1 s2 in
+ c = 0
+ | Loop(_,stmt1,s1,g1), Loop(_,stmt2,s2,g2) ->
+ Stmt.equal stmt1 stmt2 &&
+ Node.equal s1 s2 && GraphShape.equal g1 g2
+ | _ -> false
+ in
let reusable = match get_last c with
| None -> None
| Some last ->
let succs = find_succs current last in
- let same edge' =
- match edge, edge' with
- | Assign (_,loc1,typ1,exp1), Assign (_,loc2,typ2,exp2) ->
- let c = Lval.compare loc1 loc2 in
- if c <> 0 then false else
- let c = Typ.compare typ1 typ2 in
- if c <> 0 then false else
- Exp.compare exp1 exp2 = 0
- | Assume(_,e1,b1), Assume(_,e2,b2) ->
- let c = Exp.compare e1 e2 in
- if c <> 0 then false else
- Pervasives.compare b1 b2 = 0
- | EnterScope(_,vs1),EnterScope(_,vs2) ->
- let c = Extlib.list_compare Varinfo.compare vs1 vs2 in
- c = 0
- | LeaveScope(_,vs1), LeaveScope(_,vs2) ->
- let c = Extlib.list_compare Varinfo.compare vs1 vs2 in
- c = 0
- | CallDeclared(_,kf1,exp1,lval1), CallDeclared(_,kf2,exp2,lval2) ->
- let c = Kernel_function.compare kf1 kf2 in
- if c <> 0 then false else
- let c = Extlib.list_compare Exp.compare exp1 exp2 in
- if c <> 0 then false else
- let c = Extlib.opt_compare Lval.compare lval1 lval2 in
- c = 0
- | Msg(_,s1), Msg(_,s2) ->
- let c = String.compare s1 s2 in
- c = 0
- | Loop(_,stmt1,s1,g1), Loop(_,stmt2,s2,g2) ->
- Stmt.equal stmt1 stmt2 &&
- Node.equal s1 s2 && GraphShape.equal g1 g2
- | _ -> false
- in
List.find_opt same succs
in
match reusable with
@@ -492,12 +518,13 @@ module Traces = struct
let rec is_included_loops l1 l2 =
match l1, l2 with
- | Base _, OpenLoop _ | OpenLoop _, Base _ ->
+ | Base _, (OpenLoop _ | UnrollLoop _) | (OpenLoop _ | UnrollLoop _), Base _ ->
(* not in the same number of loops *)
false
| Base (c1,_), Base (c2,g2) ->
epsilon_path c1 c2 g2
- | OpenLoop(stmt1,_,_,_,_,_), OpenLoop(stmt2,_,_,_,_,_) when not (Stmt.equal stmt1 stmt2) ->
+ | (OpenLoop(stmt1,_,_,_,_,_) | UnrollLoop(stmt1,_)),
+ (OpenLoop(stmt2,_,_,_,_,_) | UnrollLoop(stmt2,_)) when not (Stmt.equal stmt1 stmt2) ->
(* not same loop *)
false
| OpenLoop(_,s1,_,_,_,_), OpenLoop(_,s2,_,_,_,_) when not (Node.equal s1 s2) ->
@@ -509,6 +536,12 @@ module Traces = struct
is_included_graph last1 last2 &&
is_included_graph g1 g2' &&
epsilon_path c1 c2 g2'
+ | UnrollLoop(_,l1), UnrollLoop(_,l2) ->
+ is_included_loops l1 l2
+ | OpenLoop(_,_,_,_,_,_), UnrollLoop(_,_) ->
+ false
+ | UnrollLoop(_,l1), OpenLoop(_,_,_,_,_,l2) ->
+ is_included_loops l1 l2
let is_included c1 c2 =
(* start is the same *)
@@ -535,14 +568,15 @@ module Traces = struct
let rec join_loops l1 l2 =
match l1, l2 with
- | Base _, OpenLoop _ | OpenLoop _, Base _ ->
+ | Base _, (OpenLoop _ | UnrollLoop _) | (OpenLoop _ | UnrollLoop _), Base _ ->
(* not in the same number of loops *)
`Top
| Base (c1,g1), Base (c2,g2) ->
let g = join_graph g1 g2 in
let (n,g) = join_path g c1 c2 in
`Value( Base (n, g))
- | OpenLoop(stmt1,_,_,_,_,_), OpenLoop(stmt2,_,_,_,_,_) when not (Stmt.equal stmt1 stmt2) ->
+ | (OpenLoop(stmt1,_,_,_,_,_) | UnrollLoop(stmt1,_)),
+ (OpenLoop(stmt2,_,_,_,_,_) | UnrollLoop(stmt2,_)) when not (Stmt.equal stmt1 stmt2) ->
(* not same loop *)
`Top
| OpenLoop(stmt1,s1,last1,c1,g1,l1), OpenLoop(_,s2,_,_,_,l2) when not (Node.equal s1 s2) ->
@@ -560,6 +594,17 @@ module Traces = struct
let (n,g) = join_path g c1 c2 in
`Value(OpenLoop(stmt,s,last,n,g,l))
end
+ | UnrollLoop(stmt,l1), UnrollLoop(_,l2) ->
+ begin match join_loops l1 l2 with
+ | `Top -> `Top
+ | `Value l -> `Value (UnrollLoop(stmt,l))
+ end
+ | (OpenLoop(stmt,s,last,c,g,l1), UnrollLoop(_,l2))
+ | (UnrollLoop(_,l2), OpenLoop(stmt,s,last,c,g,l1)) ->
+ begin match join_loops l1 l2 with
+ | `Top -> `Top
+ | `Value l -> `Value (OpenLoop(stmt,s,last,c,g,l))
+ end
let join c1 c2 =
if c1.call_declared_function || c2.call_declared_function
@@ -579,15 +624,33 @@ module Traces = struct
globals = c1.globals; main_formals = c1.main_formals;
}
- let widen _ _ c1 c2 =
- if c1.call_declared_function || c2.call_declared_function
- then assert false (* should not appended, since nothing append during a call to a not defined function *);
- match view c1, view c2 with
- | `Top, _ -> c1
- | _, `Top -> c2
- | `Other c1, `Other c2 ->
- if not_same_origin c1 c2 then assert false
- else c2
+ let add_loop stmt state =
+ let (n,g) = get_current state in
+ let succs = find_succs n g in
+ let same_loop = function
+ | Loop(_,stmt',s,last) when Stmt.equal stmt' stmt ->
+ 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)
+ | exception Not_found -> Node.next (), Graph.empty in
+ let current = OpenLoop(stmt,s,last,s,Graph.empty,state.current) in
+ { state with current }
+
+ let widen _ stmt' _ c2 =
+ if loop_mode_at_enter_loop
+ then c2
+ else begin
+ match c2.current with
+ | Base _ -> assert false (** must be in a loop *)
+ | OpenLoop(stmt,_,_,_,_,_) ->
+ assert (Stmt.equal stmt' stmt);
+ c2
+ | UnrollLoop(stmt,l) ->
+ assert (Stmt.equal stmt' stmt);
+ add_loop stmt' {c2 with current = l}
+ end
+
let narrow _c1 c2 = `Value c2
end
@@ -721,22 +784,14 @@ module Internal = struct
let enter_loop stmt state =
let state = Traces.add_edge state (Msg(Node.dumb,"enter_loop")) in
- let (n,g) = Traces.get_current state in
- let succs = Traces.find_succs n g in
- let same_loop = function
- | Loop(_,stmt',s,last) when Stmt.equal stmt' stmt ->
- 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)
- | exception Not_found -> Node.next (), Graph.empty in
- let current = OpenLoop(stmt,s,last,s,Graph.empty,state.current) in
- { state with current }
+ let state = if loop_mode_at_enter_loop then Traces.add_loop stmt state else
+ { state with current = UnrollLoop(stmt,state.current) } in
+ state
let incr_loop_counter _ state =
- Format.printf "@[<hv>@[incr_loop_counter:@] %a@]@." Traces.pretty state;
match state.current with
- | Base _ -> assert false (* absurd: we are in at least a loop *)
+ | Base _ -> assert false
+ | UnrollLoop(_,_) -> state
| OpenLoop(stmt,s,last,_,g,l) ->
let last = Traces.join_graph last g in
let current = OpenLoop(stmt,s,last,s,Graph.empty,l) in
@@ -745,14 +800,17 @@ module Internal = struct
state
let leave_loop stmt' state =
- match state.current with
- | Base _ -> assert false (* absurd: we are in at least a loop *)
- | OpenLoop(stmt,s,last,old_current_node,g,current) ->
- assert (Stmt.equal stmt stmt');
- let state = { state with current } in
- let state = Traces.add_edge state (Loop(Node.dumb,stmt,s,Graph.shape last)) in
- let state = Traces.copy_edges s old_current_node g state in
- Traces.add_edge state (Msg(Node.dumb,"leave_loop"))
+ match state.current with
+ | Base _ -> assert false (* absurd: we are in at least a loop *)
+ | UnrollLoop(_,l) -> { state with current = l }
+ | OpenLoop(stmt,s,last,old_current_node,g,current) ->
+ assert (Stmt.equal stmt stmt');
+ let state = { state with current } in
+ let state = if Graph.is_empty last then state
+ else Traces.add_edge state (Loop(Node.dumb,stmt,s,Graph.shape last)) in
+ let state = Traces.copy_edges s old_current_node g state in
+ Traces.add_edge state (Msg(Node.dumb,"leave_loop"))
+
let enter_scope _kf vars state = Traces.add_edge state (EnterScope(Node.dumb,vars))
let leave_scope _kf vars state = Traces.add_edge state (LeaveScope(Node.dumb,vars))
@@ -1004,7 +1062,12 @@ 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;
- Bottom.iter (project_of_cfg return_exp) 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 -> project_of_cfg return_exp state
(*
diff --git a/tests/value/traces/oracle/test1.res.oracle b/tests/value/traces/oracle/test1.res.oracle
index 25e610561c2..fa6b3715603 100644
--- a/tests/value/traces/oracle/test1.res.oracle
+++ b/tests/value/traces/oracle/test1.res.oracle
@@ -3,172 +3,147 @@
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
- Frama_C_entropy_source ∈ [--..--]
+ entropy_source ∈ [--..--]
g ∈ {42}
-[value] computing for function Frama_C_interval <- main.
- Called from tests/value/traces/test1.c:10.
-[value] using specification for function Frama_C_interval
-share/libc/__fc_builtin.h:52:[value] function Frama_C_interval: precondition got status valid.
-[value] Done for function Frama_C_interval
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
- Frama_C_entropy_source ∈ [--..--]
g ∈ {5; 45}
- c ∈ {0; 1}
tmp ∈ {5; 45}
[value:d-traces] Trace domains:
- start: 0; globals = g, Frama_C_entropy_source; main_formals = c
- {[ 0 -> ([ initialize variable: Frama_C_entropy_source -> 1 ])
+ start: 0; globals = g, entropy_source; main_formals = c;
+ {[ 0 -> ([ initialize variable: entropy_source -> 1 ])
1 -> ([ initialize variable using type Library_Global
-Frama_C_entropy_source -> 2 ])
+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 -> ([ EnterScope: \result<Frama_C_interval> -> 7 ])
- 7 -> ([ CallDeclared: \result<Frama_C_interval> =
- Frama_C_interval(0, 1) -> 8 ])
- 8 -> ([ Assign: c = \result<Frama_C_interval> -> 9 ])
- 9 -> ([ LeaveScope: \result<Frama_C_interval> -> 10 ])
- 10 -> ([ Assign: tmp = 0 -> 11 ])
- 11 -> ([ Assume: c false -> 12; Assume: c true -> 13 ])
- 12 -> ([ Assign: tmp = 2 -> 16 ])
- 13 -> ([ Assign: tmp = g -> 15 ])
- 15 -> ([ EnterScope: i -> 21 ])
- 16 -> ([ EnterScope: i -> 18 ])
- 18 -> ([ initialize variable: i -> 19 ])
- 19 -> ([ Assign: i = 0 -> 20 ])
- 20 -> ([ enter_loop -> 26 ])
- 21 -> ([ initialize variable: i -> 22 ])
- 22 -> ([ Assign: i = 0 -> 23 ])
- 23 -> ([ enter_loop -> 25 ])
- 25 -> ([ Assume: i < 3 true -> 28 ])
- 26 -> ([ Assume: i < 3 true -> 29 ])
- 28 -> ([ Assign: tmp = tmp + 1 -> 31 ])
- 29 -> ([ Assign: tmp = tmp + 1 -> 30 ])
- 30 -> ([ Assign: i = i + 1 -> 32 ])
- 31 -> ([ Assign: i = i + 1 -> 33 ])
- 32 -> ([ incr_loop_counter -> 36 ])
- 33 -> ([ incr_loop_counter -> 35 ])
- 35 -> ([ Assume: i < 3 true -> 39 ])
- 36 -> ([ Assume: i < 3 true -> 40 ])
- 39 -> ([ Assign: tmp = tmp + 1 -> 42 ])
- 40 -> ([ Assign: tmp = tmp + 1 -> 41 ])
- 41 -> ([ Assign: i = i + 1 -> 44 ])
- 42 -> ([ Assign: i = i + 1 -> 43 ])
- 43 -> ([ incr_loop_counter -> 48 ])
- 44 -> ([ incr_loop_counter -> 47 ])
- 47 -> ([ Assume: i < 3 true -> 51 ])
- 48 -> ([ Assume: i < 3 true -> 52 ])
- 51 -> ([ Assign: tmp = tmp + 1 -> 54 ])
- 52 -> ([ Assign: tmp = tmp + 1 -> 53 ])
- 53 -> ([ Assign: i = i + 1 -> 56 ])
- 54 -> ([ Assign: i = i + 1 -> 55 ])
- 55 -> ([ incr_loop_counter -> 60 ])
- 56 -> ([ incr_loop_counter -> 59 ])
- 59 -> ([ Assume: i < 3 false -> 63 ])
- 60 -> ([ Assume: i < 3 false -> 64 ])
- 63 -> ([ leave_loop -> 66 ])
- 64 -> ([ leave_loop -> 65 ])
- 65 -> ([ LeaveScope: i -> 68 ])
- 66 -> ([ LeaveScope: i -> 67 ])
- 67 -> ([ Assign: g = tmp -> 70 ])
- 68 -> ([ Assign: g = tmp -> 69 ])
- 69 -> ([ join -> 107 ])
- 70 -> ([ join -> 107 ]) ]}
- current: 107]
-[kernel] warning: no input file.
+ 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
[from] Computing for function main
-[from] Computing for function Frama_C_interval <-main
-[from] Done for function Frama_C_interval
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
-[from] Function Frama_C_interval:
- Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
- \result FROM Frama_C_entropy_source; min; max
[from] Function main:
- Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
- g FROM Frama_C_entropy_source; g
- \result FROM Frama_C_entropy_source; g
+ g FROM g; c
+ \result FROM g; c
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
- Frama_C_entropy_source; g; c; tmp; i
+ g; tmp; i
[inout] Inputs for function main:
- Frama_C_entropy_source; g
+ g
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
- Frama_C_entropy_source ∈ [--..--]
-[value] using specification for function Frama_C_interval
-share/libc/__fc_builtin.h:52:[value] warning: function Frama_C_interval: precondition got status unknown.
+ entropy_source ∈ [--..--]
+ g ∈ {42}
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
- Frama_C_entropy_source ∈ [--..--]
g ∈ {5; 45}
- c ∈ [--..--]
- __retres ∈ {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 */
-#include "__fc_builtin.h"
-int g;
+extern int volatile entropy_source;
+/*@ requires min ≤ max;
+ ensures \old(min) ≤ \result ≤ \old(max);
+ assigns \result, entropy_source;
+ assigns \result \from min, max, entropy_source;
+ assigns entropy_source \from entropy_source;
+ */
+extern int interval(int min, int max);
+
+int g = 42;
int main(int c)
{
- int __retres;
+ int __traces_domain_return;
g = 42;
{
int tmp;
- {
- int \result<Frama_C_interval>;
- \result<Frama_C_interval> = Frama_C_interval(0,1);
- c = \result<Frama_C_interval>;
- tmp = 0;
- if (c) {
- tmp = g;
- {
- i = 0;
- /*@ assert i < 3; */ ;
- tmp ++;
- i ++;
- /*@ assert i < 3; */ ;
- tmp ++;
- i ++;
- /*@ assert i < 3; */ ;
- tmp ++;
- i ++;
- /*@ assert ¬(i < 3); */ ;
- g = tmp;
- __retres = tmp;
- goto return_label;
- }
+ tmp = 0;
+ if (c) {
+ tmp = g;
+ {
+ int i;
+ i = 0;
+ /*@ assert i < 3; */
+ tmp ++;
+ i ++;
+ /*@ assert i < 3; */
+ tmp ++;
+ i ++;
+ /*@ assert i < 3; */
+ tmp ++;
+ i ++;
+ /*@ assert ¬(i < 3); */
+ g = tmp;
+ __traces_domain_return = tmp;
}
- else {
- tmp = 2;
- {
- i = 0;
- /*@ assert i < 3; */ ;
- tmp ++;
- i ++;
- /*@ assert i < 3; */ ;
- tmp ++;
- i ++;
- /*@ assert i < 3; */ ;
- tmp ++;
- i ++;
- /*@ assert ¬(i < 3); */ ;
- g = tmp;
- __retres = tmp;
- goto return_label;
- }
+ }
+ else {
+ tmp = 2;
+ {
+ int i;
+ i = 0;
+ /*@ assert i < 3; */
+ tmp ++;
+ i ++;
+ /*@ assert i < 3; */
+ tmp ++;
+ i ++;
+ /*@ assert i < 3; */
+ tmp ++;
+ i ++;
+ /*@ assert ¬(i < 3); */
+ g = tmp;
+ __traces_domain_return = tmp;
}
- return_label: return __retres;
}
}
+ return __traces_domain_return;
}
diff --git a/tests/value/traces/oracle/test2.res.oracle b/tests/value/traces/oracle/test2.res.oracle
index 9a1328ea5a2..4b76a11dc24 100644
--- a/tests/value/traces/oracle/test2.res.oracle
+++ b/tests/value/traces/oracle/test2.res.oracle
@@ -20,7 +20,7 @@
[value:final-states] Values at end of function main:
tmp ∈ {4; 5}
[value:d-traces] Trace domains:
- start: 0; globals = ; main_formals = c
+ start: 0; globals = ; main_formals = c;
{[ 0 -> ([ initialize variable using type Main_Formal
c -> 1 ])
1 -> ([ EnterScope: tmp -> 2 ])
@@ -29,7 +29,7 @@ c -> 1 ])
4 -> ([ Assign: tmp = 2 -> 8 ])
5 -> ([ Assign: tmp = 1 -> 7 ])
7 -> ([ start_call: loop (true) -> 9 ])
- 8 -> ([ start_call: loop (true) -> 55 ])
+ 8 -> ([ start_call: loop (true) -> 50 ])
9 -> ([ EnterScope: j -> 10 ])
10 -> ([ Assign: j = tmp -> 11 ])
11 -> ([ EnterScope: i -> 12 ])
@@ -39,55 +39,45 @@ c -> 1 ])
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 -> 124 ])
- 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 -> 124 ]) ]}
- current: 124]
-[kernel] warning: no input file.
+ 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
[from] Computing for function loop
[from] Done for function loop
[from] Computing for function main
@@ -115,11 +105,14 @@ c -> 1 ])
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
- __retres ∈ {4; 5}
+ __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)
{
- int __retres;
+ int __traces_domain_return;
{
int tmp;
tmp = 0;
@@ -129,23 +122,23 @@ int main(int c)
int j;
j = tmp;
{
+ int i;
i = 0;
- /*@ assert i < 3; */ ;
+ /*@ assert i < 3; */
j ++;
i ++;
- /*@ assert i < 3; */ ;
+ /*@ assert i < 3; */
j ++;
i ++;
- /*@ assert i < 3; */ ;
+ /*@ assert i < 3; */
j ++;
i ++;
- /*@ assert ¬(i < 3); */ ;
+ /*@ assert ¬(i < 3); */
{
- int \result<loop>;
- \result<loop> = j;
- tmp = \result<loop>;
- __retres = tmp;
- goto return_label;
+ int _result_loop_;
+ _result_loop_ = j;
+ tmp = _result_loop_;
+ __traces_domain_return = tmp;
}
}
}
@@ -156,29 +149,29 @@ int main(int c)
int j;
j = tmp;
{
+ int i;
i = 0;
- /*@ assert i < 3; */ ;
+ /*@ assert i < 3; */
j ++;
i ++;
- /*@ assert i < 3; */ ;
+ /*@ assert i < 3; */
j ++;
i ++;
- /*@ assert i < 3; */ ;
+ /*@ assert i < 3; */
j ++;
i ++;
- /*@ assert ¬(i < 3); */ ;
+ /*@ assert ¬(i < 3); */
{
- int \result<loop>;
- \result<loop> = j;
- tmp = \result<loop>;
- __retres = tmp;
- goto return_label;
+ int _result_loop_;
+ _result_loop_ = j;
+ tmp = _result_loop_;
+ __traces_domain_return = tmp;
}
}
}
}
- return_label: return __retres;
}
+ return __traces_domain_return;
}
diff --git a/tests/value/traces/oracle/test3.res.oracle b/tests/value/traces/oracle/test3.res.oracle
index b43e758a986..0815593eb4d 100644
--- a/tests/value/traces/oracle/test3.res.oracle
+++ b/tests/value/traces/oracle/test3.res.oracle
@@ -12,7 +12,7 @@
tmp ∈ {4}
__retres ∈ {5}
[value:d-traces] Trace domains:
- start: 0; globals = g; main_formals = c
+ start: 0; globals = g; main_formals = c;
{[ 0 -> ([ initialize variable: g -> 1 ])
1 -> ([ initialize variable using type Main_Formal
c -> 2 ])
@@ -22,9 +22,7 @@ c -> 2 ])
5 -> ([ Assign: tmp = 4 -> 6 ])
6 -> ([ Assume: tmp true -> 7 ])
7 -> ([ Assign: g = tmp -> 8 ])
- 8 -> ([ Assign: __retres = g + 1 -> 9 ]) ]}
- current: 9]
-[kernel] warning: no input file.
+ 8 -> ([ Assign: __retres = g + 1 -> 9 ]) ]} at 9
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
@@ -41,8 +39,12 @@ c -> 2 ])
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
-
+ g ∈ {0}
[value] done for function main
[value] ====== VALUES COMPUTED ======
[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
diff --git a/tests/value/traces/oracle/test4.res.oracle b/tests/value/traces/oracle/test4.res.oracle
index 162134d3c3a..7cb901ea75e 100644
--- a/tests/value/traces/oracle/test4.res.oracle
+++ b/tests/value/traces/oracle/test4.res.oracle
@@ -4,48 +4,6 @@
[value] Initial state computed
[value:initial-state] Values of globals at initialization
-incr_loop_counter: start: 0; globals = ; main_formals = c;
- start 9
- {[ 9 -> ([ Assume: i < 3 true -> 10 ])
- 10 -> ([ Assign: tmp = tmp + 1 -> 11 ])
- 11 -> ([ Assign: i = i + 1 -> 12 ]) ]} at 12
- {[ 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 ]) ]} at 8
-incr_loop_counter: start: 0; globals = ; main_formals = c;
- start 9
- {[ 9 -> ([ Assume: i < 3 true -> 10 ])
- 10 -> ([ Assign: tmp = tmp + 1 -> 11 ])
- 11 -> ([ Assign: i = i + 1 -> 12 ]) ]} at 12
- {[ 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 ]) ]} at 8
-incr_loop_counter: start: 0; globals = ; main_formals = c;
- start 9
- {[ 9 -> ([ Assume: i < 3 true -> 10 ])
- 10 -> ([ Assign: tmp = tmp + 1 -> 11 ])
- 11 -> ([ Assign: i = i + 1 -> 12 ]) ]} at 12
- {[ 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 ]) ]} at 8
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
@@ -62,11 +20,17 @@ c -> 1 ])
5 -> ([ initialize variable: i -> 6 ])
6 -> ([ Assign: i = 0 -> 7 ])
7 -> ([ enter_loop -> 8 ])
- 8 -> ([ Loop(9) {[ 9 -> Assume: i < 3 true -> 10
- 10 -> Assign: tmp = tmp + 1 -> 11
- 11 -> Assign: i = i + 1 -> 12 ]} -> 14 ])
- 14 -> ([ Assume: i < 3 false -> 15 ]) 15 -> ([ leave_loop -> 16 ])
- 16 -> ([ LeaveScope: i -> 17 ]) ]} at 17
+ 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
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
@@ -83,27 +47,37 @@ c -> 1 ])
[value] Initial state computed
[value:initial-state] Values of globals at initialization
-tests/value/traces/test4.i:7:[value] entering loop for the first time
-:0:[value] warning: signed overflow. assert tmp + 1 ≤ 2147483647;
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
- __traces_domain_return ∈ [0..2147483647]
+ __traces_domain_return ∈ {3}
[value:d-traces] Trace domains:
TOP
-:0:[kernel] failure: [AST Integrity Check] AST of Eva.Traces_domain
- variable __traces_domain_return(26) is not declared
-[kernel] Current source was: tests/value/traces/test4.i:5
- The full backtrace is:
- Raised at file "src/libraries/project/project.ml", line 402, characters 50-57
- Called from file "src/kernel_internals/runtime/boot.ml", line 51, characters 6-53
- Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 799, characters 8-101
- Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 808, characters 22-39
- Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
-
- Frama-C aborted: internal error.
- Please report as 'crash' at http://bts.frama-c.com/.
- Your Frama-C version is Phosphorus-20170501+dev.
- Note that a version and a backtrace alone often do not contain enough
- information to understand the bug. Guidelines for reporting bugs are at:
- http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
+[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/test1.c b/tests/value/traces/test1.c
index 04a0639deb3..8b3966a6150 100644
--- a/tests/value/traces/test1.c
+++ b/tests/value/traces/test1.c
@@ -18,12 +18,10 @@ int main(int c){
/* c = interval(0,1); */
int tmp;
tmp = 0;
- /* if (c) tmp = g; */
- /* else */ tmp = 2;
+ if (c) tmp = g;
+ else tmp = 2;
for(int i = 0; i < 3; i++){
tmp ++;
- if (tmp > 43) break;
- if (c == 4) return 2;
}
g = tmp;
return tmp;
--
GitLab