From b3e8e96ffe82945320eaa1c59ea8620212c068fc Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 17 May 2019 19:25:59 +0200
Subject: [PATCH] [Eva] Allow the partitioning to survive function returns
---
src/plugins/value/engine/compute_functions.ml | 51 +++--
src/plugins/value/engine/iterator.ml | 120 +++++-----
src/plugins/value/engine/iterator.mli | 3 +-
src/plugins/value/engine/mem_exec.ml | 15 +-
src/plugins/value/engine/mem_exec.mli | 4 +-
.../value/engine/transfer_specification.ml | 8 +-
.../value/engine/transfer_specification.mli | 2 +-
src/plugins/value/engine/transfer_stmt.ml | 70 +++---
src/plugins/value/engine/transfer_stmt.mli | 9 +-
src/plugins/value/partitioning/partition.ml | 215 +++++++++++++-----
src/plugins/value/partitioning/partition.mli | 12 +-
.../value/partitioning/trace_partitioning.ml | 9 +-
.../value/partitioning/trace_partitioning.mli | 5 +-
.../oracle/partitioning-annots.2.res.oracle | 3 -
.../partitioning-interproc.0.res.oracle | 13 +-
.../partitioning-interproc.1.res.oracle | 2 +-
tests/value/oracle/split_return.0.res.oracle | 4 +-
tests/value/oracle/split_return.1.res.oracle | 10 +-
tests/value/oracle/split_return.4.res.oracle | 2 +-
tests/value/partitioning-interproc.c | 2 +-
20 files changed, 333 insertions(+), 226 deletions(-)
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index a932d0eebdc..a93a27e8d51 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -164,7 +164,7 @@ module Make (Abstract: Abstractions.Eva) = struct
is the instruction at which the call takes place, and is used to update
the statuses of the preconditions of [kf]. If [show_progress] is true,
the callstack and additional information are printed. *)
- let compute_using_spec_or_body call_kinstr call recursion state =
+ let compute_using_spec_or_body call_kinstr call recursion pkey state =
let kf = call.kf in
Value_results.mark_kf_as_called kf;
let global = match call_kinstr with Kglobal -> true | _ -> false in
@@ -199,7 +199,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let vi = Kernel_function.get_vi kf in
if Cil.is_in_libc vi.vattr then
Library_functions.warn_unsupported_spec vi.vorig_name;
- Spec.compute_using_specification ~warn:true call_kinstr call spec state,
+ Spec.compute_using_specification ~warn:true
+ call_kinstr call spec (pkey,state),
Eval.Cacheable
| `Def _fundec ->
Db.Value.Call_Type_Value_Callbacks.apply (`Def, cvalue_state, call_stack);
@@ -215,9 +216,9 @@ module Make (Abstract: Abstractions.Eva) = struct
module MemExec = Mem_exec.Make (Abstract.Val) (Abstract.Dom)
- let compute_and_cache_call stmt call recursion init_state =
+ let compute_and_cache_call stmt call recursion pkey init_state =
let default () =
- compute_using_spec_or_body (Kstmt stmt) call recursion init_state
+ compute_using_spec_or_body (Kstmt stmt) call recursion pkey init_state
in
if Value_parameters.MemExecAll.get () then
let args =
@@ -274,14 +275,14 @@ module Make (Abstract: Abstractions.Eva) = struct
let rest = List.map (fun (e, assgn) -> e, lift_assigned assgn) call.rest in
{ call with arguments; rest }
- let join_states = function
+ let join_states default_key = function
| [] -> `Bottom
- | [state] -> `Value state
- | s :: l -> `Value (List.fold_left Abstract.Dom.join s l)
+ | (_k,s) :: l ->
+ `Value (default_key, List.fold_left Abstract.Dom.join s (List.map snd l))
- let compute_call_or_builtin stmt call recursion state =
+ let compute_call_or_builtin stmt call recursion pkey state =
match Builtins.find_builtin_override call.kf with
- | None -> compute_and_cache_call stmt call recursion state
+ | None -> compute_and_cache_call stmt call recursion pkey state
| Some (name, builtin, cacheable, spec) ->
Value_results.mark_kf_as_called call.kf;
let kinstr = Kstmt stmt in
@@ -293,11 +294,10 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Do not track garbled mixes created when interpreting the specification,
as the result of the cvalue builtin will overwrite them. *)
Locations.Location_Bytes.do_track_garbled_mix false;
- let states =
- Spec.compute_using_specification ~warn:false kinstr call spec state
- in
+ let states = Spec.compute_using_specification
+ ~warn:false kinstr call spec (pkey,state) in
Locations.Location_Bytes.do_track_garbled_mix true;
- let final_state = states >>- join_states in
+ let final_state = join_states pkey states in
let cvalue_state = Abstract.Dom.get_cvalue_or_top state in
match final_state with
| `Bottom ->
@@ -305,24 +305,32 @@ module Make (Abstract: Abstractions.Eva) = struct
Db.Value.Call_Type_Value_Callbacks.apply (`Spec spec, cvalue_state, cs);
let cacheable = Eval.Cacheable in
Transfer.{states; cacheable; builtin=true}
- | `Value final_state ->
+ | `Value (pkey,final_state) ->
let cvalue_call = get_cvalue_call call in
let post = Abstract.Dom.get_cvalue_or_top final_state in
let cvalue_states =
Builtins.apply_builtin builtin cvalue_call ~pre:cvalue_state ~post
in
let insert cvalue_state =
- Abstract.Dom.set Cvalue_domain.State.key cvalue_state final_state
+ pkey,Abstract.Dom.set Cvalue_domain.State.key cvalue_state final_state
in
- let states = Bottom.bot_of_list (List.map insert cvalue_states) in
+ let states = List.map insert cvalue_states in
Transfer.{states; cacheable; builtin=true}
+ let recombine_keys compute =
+ fun stmt call recursion pkey state ->
+ let result = compute stmt call recursion Partition.Key.zero state in
+ let recombine (pkey',state') =
+ Partition.Key.recombine pkey pkey', state'
+ in
+ Transfer.{ result with states = List.map recombine result.states }
+
let compute_call =
if Abstract.Dom.mem Cvalue_domain.State.key
&& Abstract.Val.mem Main_values.CVal.key
&& Abstract.Loc.mem Main_locations.PLoc.key
- then compute_call_or_builtin
- else compute_and_cache_call
+ then recombine_keys compute_call_or_builtin
+ else recombine_keys compute_and_cache_call
let () = Transfer.compute_call_ref := compute_call
@@ -339,11 +347,12 @@ module Make (Abstract: Abstractions.Eva) = struct
let call =
{ kf; callstack = []; arguments = []; rest = []; return = None; }
in
+ let pkey = Partition.Key.zero in
let final_result =
- compute_using_spec_or_body Kglobal call None init_state
+ compute_using_spec_or_body Kglobal call None pkey init_state
in
- let final_states = final_result.Transfer.states in
- let final_state = PowersetDomain.(final_states >>-: of_list >>- join) in
+ let final_states = List.map snd (final_result.Transfer.states) in
+ let final_state = PowersetDomain.(final_states |> of_list |> join) in
Value_util.pop_call_stack ();
Value_parameters.feedback "done for function %a" Kernel_function.pretty kf;
Abstract.Dom.Store.mark_as_computed ();
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index 933035419a6..dac195362c4 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -95,12 +95,12 @@ module Make_Dataflow
(* --- Abstract values storage --- *)
- module Partition = Trace_partitioning.Make (Abstract) (AnalysisParam)
+ module Partitioning = Trace_partitioning.Make (Abstract) (AnalysisParam)
- type store = Partition.store
- type flow = Partition.flow
- type tank = Partition.tank
- type widening = Partition.widening
+ type store = Partitioning.store
+ type flow = Partitioning.flow
+ type tank = Partitioning.tank
+ type widening = Partitioning.widening
type edge_info = {
mutable fireable : bool (* Does any states survive the transition ? *)
@@ -141,9 +141,9 @@ module Make_Dataflow
| `Value state -> state
let initial_tank =
- Partition.initial_tank (States.to_list initial_states)
+ Partitioning.initial_tank (States.to_list initial_states)
let get_initial_flow () =
- -1 (* Dummy edge id *), Partition.drain initial_tank
+ -1 (* Dummy edge id *), Partitioning.drain initial_tank
let post_conditions = ref false
@@ -180,11 +180,11 @@ module Make_Dataflow
(* Default (Initial) stores on vertex and edges *)
let default_vertex_store (v : vertex) () : store =
- Partition.empty_store ~stmt:v.vertex_start_of
+ Partitioning.empty_store ~stmt:v.vertex_start_of
let default_vertex_widening (v : vertex) () : widening =
- Partition.empty_widening ~stmt:v.vertex_start_of
+ Partitioning.empty_widening ~stmt:v.vertex_start_of
let default_edge_tank () : tank * edge_info =
- Partition.empty_tank (), { fireable = false }
+ Partitioning.empty_tank (), { fireable = false }
(* Get the stores associated to a control point or edge *)
let get_vertex_store (v : vertex) : store =
@@ -217,24 +217,28 @@ module Make_Dataflow
(* --- Transfer functions application --- *)
+ type key = Partition.key
type state = Domain.t
- type transfer_function = state -> state list
+ type transfer_function = (key * state) -> (key * state) list
- let id : transfer_function = fun x -> [x]
+ let id : transfer_function = fun (k,x) -> [(k,x)]
(* Thse lifting function helps to uniformize the transfer functions to a
common signature *)
let lift (f : state -> state) : transfer_function =
- fun x -> [f x]
+ fun (k,x) -> [(k,f x)]
let lift' (f : state -> state or_bottom) : transfer_function =
- fun x -> Bottom.to_list (f x)
+ fun (k,x) -> Bottom.to_list (f x >>-: fun y -> k,y)
+
+ let lift'' (f : state -> state list) : transfer_function =
+ fun (k,x) -> List.map (fun y -> k,y) (f x)
let sequence (f1 : transfer_function) (f2 : transfer_function)
: transfer_function =
- fun x -> List.fold_left (fun acc y -> f2 y @ acc) [] (f1 x)
+ fun (k,x) -> List.fold_left (fun acc (k',y) -> f2 (k',y) @ acc) [] (f1 (k,x))
(* Tries to evaluate \assigns … \from … clauses for assembly code. *)
@@ -269,14 +273,14 @@ module Make_Dataflow
if vars = [] then id else lift (Domain.leave_scope kf vars)
let transfer_call (stmt : stmt) (dest : lval option) (callee : exp)
- (args : exp list) (state : state) : state list =
+ (args : exp list) (key,state : key * state) : (key*state) list =
let result, call_cacheable =
- Transfer.call stmt dest callee args state
+ Transfer.call stmt dest callee args key state
in
if call_cacheable = Eval.NoCacheCallers then
(* Propagate info that the current call cannot be cached either *)
cacheable := Eval.NoCacheCallers;
- Bottom.list_of_bot result
+ result
let transfer_instr (stmt : stmt) (instr : instr) : transfer_function =
match instr with
@@ -289,13 +293,13 @@ module Make_Dataflow
lift' transfer
| Local_init (vi, ConsInit (f, args, k), loc) ->
let kind = Abstract_domain.Local kf in
- let as_func dest callee args _loc state =
+ let as_func dest callee args _loc (key,state) =
(* This variable enters the scope too early, as it should
be introduced after the call to [f] but before the assignment
to [v]. This is currently not possible, at least without
splitting Transfer.call in two. *)
let state = Domain.enter_scope kind [vi] state in
- transfer_call stmt dest callee args state
+ transfer_call stmt dest callee args (key,state)
in
Cil.treat_constructor_as_func as_func vi f args k loc
| Set (dest, exp, _loc) ->
@@ -331,7 +335,7 @@ module Make_Dataflow
(* Assign the return value *)
and assign_retval =
match return_exp with
- | None -> id
+ | None -> fun state -> [state]
| Some return_exp ->
let vi_ret = Option.get (Library_functions.get_retres_vi kf) in
let return_lval = Var vi_ret, NoOffset in
@@ -342,7 +346,7 @@ module Make_Dataflow
let state' = Transfer.assign state kstmt return_lval return_exp in
Bottom.to_list state'
in
- sequence check_postconditions assign_retval
+ sequence (lift'' check_postconditions) (lift'' assign_retval)
let transfer_transition (t : vertex transition) : transfer_function =
match t with
@@ -357,7 +361,8 @@ module Make_Dataflow
| Leave (block) -> transfer_leave block
| Prop _ -> id (* Annotations are interpreted in [transfer_statement]. *)
- let transfer_annotations (stmt : stmt) ~(record : bool) : transfer_function =
+ let transfer_annotations (stmt : stmt) ~(record : bool)
+ : state -> state list =
let annots =
(* We do not interpret annotations that come from statement contracts
and everything previously emitted by Value (currently, alarms) *)
@@ -395,20 +400,20 @@ module Make_Dataflow
(transition : vertex transition) (flow : flow) : flow =
(* Split return *)
let flow = match transition with
- | Return (return_exp, _) -> Partition.split_return flow return_exp
+ | Return (return_exp, _) -> Partitioning.split_return flow return_exp
| _ -> flow
in
(* Loop transitions *)
let the_stmt v = Option.get v.vertex_start_of in
let enter_loop f v =
- let f = Partition.enter_loop f (the_stmt v) in
- Partition.transfer (lift (Domain.enter_loop (the_stmt v))) f
+ let f = Partitioning.enter_loop f (the_stmt v) in
+ Partitioning.transfer (lift (Domain.enter_loop (the_stmt v))) f
and leave_loop f v =
- let f = Partition.leave_loop f (the_stmt v) in
- Partition.transfer (lift (Domain.leave_loop (the_stmt v))) f
+ let f = Partitioning.leave_loop f (the_stmt v) in
+ Partitioning.transfer (lift (Domain.leave_loop (the_stmt v))) f
and incr_loop_counter f v =
- let f = Partition.next_loop_iteration f (the_stmt v) in
- Partition.transfer (lift (Domain.incr_loop_counter (the_stmt v))) f
+ let f = Partitioning.next_loop_iteration f (the_stmt v) in
+ Partitioning.transfer (lift (Domain.incr_loop_counter (the_stmt v))) f
in
let loops_left, loops_entered =
Interpreted_automata.get_wto_index_diff kf v1 v2
@@ -422,14 +427,14 @@ module Make_Dataflow
let process_edge (v1,e,v2 : G.edge) : flow =
let {edge_transition=transition; edge_kinstr=kinstr} = e in
let tank,edge_info = get_edge_data e in
- let flow = Partition.drain tank in
+ let flow = Partitioning.drain tank in
Db.yield ();
check_signals ();
current_ki := kinstr;
Cil.CurrentLoc.set e.edge_loc;
- let flow = Partition.transfer (transfer_transition transition) flow in
+ let flow = Partitioning.transfer (transfer_transition transition) flow in
let flow = process_partitioning_transitions v1 v2 transition flow in
- if not (Partition.is_empty_flow flow) then
+ if not (Partitioning.is_empty_flow flow) then
edge_info.fireable <- true;
flow
@@ -439,7 +444,7 @@ module Make_Dataflow
let call_statement_callbacks (stmt : stmt) (f : flow) : unit =
(* TODO: apply on all domains. *)
- let states = Partition.contents f in
+ let states = Partitioning.contents f in
let cvalue_states = gather_cvalues states in
Db.Value.Compute_Statement_Callbacks.apply
(stmt, Value_util.call_stack (), cvalue_states)
@@ -457,36 +462,37 @@ module Make_Dataflow
(* Get vertex store *)
let store = get_vertex_store v in
(* Join incoming s tates *)
- let flow = Partition.join sources store in
+ let flow = Partitioning.join sources store in
let flow =
match v.vertex_start_of with
| Some stmt ->
(* Callbacks *)
call_statement_callbacks stmt flow;
(* Transfer function associated to the statement *)
- Partition.transfer (transfer_statement stmt) flow
+ Partitioning.transfer (lift'' (transfer_statement stmt)) flow
| _ -> flow
in
(* Widen if necessary *)
let flow =
- if widening && not (Partition.is_empty_flow flow) then begin
- let flow = Partition.widen (get_vertex_widening v) flow in
+ if widening && not (Partitioning.is_empty_flow flow) then begin
+ let flow = Partitioning.widen (get_vertex_widening v) flow in
(* Try to correct over-widenings *)
let correct_over_widening stmt =
(* Do *not* record the status after interpreting the annotation
here. Possible unproven assertions have already been recorded
when the assertion has been interpreted the first time higher
in this function. *)
- Partition.transfer (transfer_annotations stmt ~record:false) flow
+ Partitioning.transfer
+ (lift'' (transfer_annotations stmt ~record:false)) flow
in
Option.fold ~some:correct_over_widening ~none:flow v.vertex_start_of
end else
flow
in
(* Dispatch to successors *)
- List.iter (fun into -> Partition.fill flow ~into) (get_succ_tanks v);
+ List.iter (fun into -> Partitioning.fill flow ~into) (get_succ_tanks v);
(* Return whether the iterator should stop or not *)
- Partition.is_empty_flow flow
+ Partitioning.is_empty_flow flow
let process_vertex ?(widening : bool = false) (v : vertex) : bool =
(* Process predecessors *)
@@ -509,7 +515,7 @@ module Make_Dataflow
(* Try every possible successor *)
let add_if_fireable (_,e,succ as edge) acc =
let f = process_edge edge in
- if Partition.is_empty_flow f
+ if Partitioning.is_empty_flow f
then acc
else (e.edge_key,f,succ) :: acc
in
@@ -525,13 +531,13 @@ module Make_Dataflow
let reset_component (vertex_list : vertex list) : unit =
let reset_edge (_,e,_) =
let t,_ = get_edge_data e in
- Partition.reset_tank t
+ Partitioning.reset_tank t
in
let reset_vertex v =
let s = get_vertex_store v
and w = get_vertex_widening v in
- Partition.reset_store s;
- Partition.reset_widening w;
+ Partitioning.reset_store s;
+ Partitioning.reset_widening w;
List.iter reset_edge (G.succ_e graph v)
in
List.iter reset_vertex vertex_list
@@ -547,7 +553,7 @@ module Make_Dataflow
is especially useful for nested loops. *)
if hierachical_convergence
then reset_component (v :: Wto.flatten w)
- else Partition.reset_widening_counter (get_vertex_widening v);
+ else Partitioning.reset_widening_counter (get_vertex_widening v);
(* Iterate until convergence *)
let iteration_count = ref 0 in
while
@@ -578,7 +584,7 @@ module Make_Dataflow
let mark_degeneration () =
let f stmt (v,_) =
let l = get_succ_tanks v in
- if not (List.for_all Partition.is_empty_tank l) then
+ if not (List.for_all Partitioning.is_empty_tank l) then
Value_util.DegenerationPoints.replace stmt false
in
StmtTable.iter f automaton.stmt_table;
@@ -594,7 +600,7 @@ module Make_Dataflow
ignore (Logic.check_fct_postconditions kf active_behaviors Normal
~pre_state:initial_state ~post_states:States.empty ~result:None)
- let compute () : state list or_bottom =
+ let compute () : (key*state) list =
if interpreter_mode then
simulate automaton.entry_point (get_initial_flow ())
else begin
@@ -603,7 +609,7 @@ module Make_Dataflow
end;
if not !post_conditions then mark_postconds_as_true ();
let final_store = get_vertex_store automaton.return_point in
- Bottom.bot_of_list (Partition.expanded final_store)
+ Partitioning.expanded final_store
(* --- Results conversion --- *)
@@ -664,7 +670,7 @@ module Make_Dataflow
let merged_states = VertexTable.create control_point_count
and get_smashed_store v =
let store = get_vertex_store v in
- Partition.smashed store
+ Partitioning.smashed store
in
fun ~all stmt (v : vertex) ->
if all || is_instr stmt
@@ -685,8 +691,8 @@ module Make_Dataflow
let unmerged_pre_cvalues = lazy
(StmtTable.map (fun _stmt (v,_) ->
let store = get_vertex_store v in
- let states = Partition.expanded store in
- List.map (fun x -> Domain.get_cvalue_or_top x) states)
+ let states = Partitioning.expanded store in
+ List.map (fun (_k,x) -> Domain.get_cvalue_or_top x) states)
automaton.stmt_table)
in
let merged_pre_cvalues = lazy (lift_to_cvalues merged_pre_states)
@@ -772,12 +778,10 @@ module Computer
Kernel_function.pretty kf;
Dataflow.merge_results ();
let f = Kernel_function.get_definition kf in
- (match results with
- | `Value (_::_) when Cil.hasAttribute "noreturn" f.svar.vattr ->
- Value_util.warning_once_current
- "function %a may terminate but has the noreturn attribute"
- Kernel_function.pretty kf;
- | _ -> ());
+ if Cil.hasAttribute "noreturn" f.svar.vattr && results <> [] then
+ Value_util.warning_once_current
+ "function %a may terminate but has the noreturn attribute"
+ Kernel_function.pretty kf;
results, !Dataflow.cacheable
in
let cleanup () =
diff --git a/src/plugins/value/engine/iterator.mli b/src/plugins/value/engine/iterator.mli
index 163796d15e9..b76ecae19a4 100644
--- a/src/plugins/value/engine/iterator.mli
+++ b/src/plugins/value/engine/iterator.mli
@@ -21,7 +21,6 @@
(**************************************************************************)
open Cil_types
-open Eval
(** Mark the analysis as aborted. It will be stopped at the next safe point *)
val signal_abort: unit -> unit
@@ -46,7 +45,7 @@ module Computer
val compute:
kernel_function -> kinstr -> Abstract.Dom.t ->
- Abstract.Dom.t list or_bottom * Eval.cacheable
+ (Partition.key * Abstract.Dom.t) list * Eval.cacheable
end
diff --git a/src/plugins/value/engine/mem_exec.ml b/src/plugins/value/engine/mem_exec.ml
index 7a8e0351821..54c5d3f5e9f 100644
--- a/src/plugins/value/engine/mem_exec.ml
+++ b/src/plugins/value/engine/mem_exec.ml
@@ -53,7 +53,7 @@ module Make
incr counter;
- module CallOutput = Datatype.List (Domain)
+ module CallOutput = Datatype.List (Datatype.Pair (Partition.Key) (Domain))
module StoredResult =
Datatype.Triple
@@ -145,7 +145,7 @@ module Make
else expand_inputs_with_relations (count - 1) kf expanded_bases state
let store_computed_call kf input_state args
- (call_result: Domain.t list Bottom.or_bottom) =
+ (call_result: (Partition.key * Domain.t) list) =
match Transfer_stmt.current_kf_inout () with
| None -> ()
| Some inout ->
@@ -196,10 +196,8 @@ module Make
let all_output_bases =
Extlib.opt_fold Base.Hptset.add return_base all_output_bases
in
- let clear state = Domain.filter kf `Post all_output_bases state in
- let call_result = match call_result with
- | `Bottom -> []
- | `Value list -> list
+ let clear (key,state) =
+ key, Domain.filter kf `Post all_output_bases state
in
let outputs = List.map clear call_result in
let call_number = current_counter () in
@@ -248,7 +246,8 @@ module Make
let bases, outputs, i = Domain.Hashtbl.find hstates st_filtered in
(* We have found a previous execution, in which the outputs are
[outputs]. Copy them in [state] and return this result. *)
- let process output =
+ let process (key,output) =
+ key,
Domain.reuse kf bases ~current_input:state ~previous_output:output
in
let outputs = List.map process outputs in
@@ -268,7 +267,7 @@ module Make
| Not_found -> None
| Result_found (outputs, i) ->
let call_result = outputs in
- Some (Bottom.bot_of_list call_result, i)
+ Some (call_result, i)
end
diff --git a/src/plugins/value/engine/mem_exec.mli b/src/plugins/value/engine/mem_exec.mli
index afc29371ac5..cb2a641032a 100644
--- a/src/plugins/value/engine/mem_exec.mli
+++ b/src/plugins/value/engine/mem_exec.mli
@@ -41,7 +41,7 @@ module Make
to be reused in subsequent calls *)
val store_computed_call:
kernel_function -> Domain.t -> Value.t or_bottom list ->
- Domain.t list or_bottom ->
+ (Partition.key * Domain.t) list ->
unit
(** [reuse_previous_call kf init_state args] searches amongst the previous
@@ -52,7 +52,7 @@ module Make
by the plugins that have registered Value callbacks.) *)
val reuse_previous_call:
kernel_function -> Domain.t -> Value.t or_bottom list ->
- (Domain.t list or_bottom * int) option
+ ((Partition.key * Domain.t) list * int) option
end
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index 5e782e06f03..955d7456f84 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -564,10 +564,10 @@ module Make
evaluates the assigns, and finally reduces by the post-conditions.
[warn] is false for the specification of cvalue builtins — in this case,
some warnings are disabled, such as warnings about new garbled mixes. *)
- let compute_using_specification ~warn kinstr call spec state =
+ let compute_using_specification ~warn kinstr call spec (key,state) =
let vi = Kernel_function.get_vi call.kf in
if Cil.hasAttribute "noreturn" vi.vattr
- then `Bottom
+ then []
else
(* Initializes the variable returned by the function. *)
let state = match call.return with
@@ -582,8 +582,6 @@ module Make
let states =
compute_specification ~warn kinstr call.kf call.return spec state
in
- if States.is_empty states
- then `Bottom
- else `Value (States.to_list states)
+ List.map (fun x -> key,x) (States.to_list states)
end
diff --git a/src/plugins/value/engine/transfer_specification.mli b/src/plugins/value/engine/transfer_specification.mli
index 06af47c468c..4c5a61b7767 100644
--- a/src/plugins/value/engine/transfer_specification.mli
+++ b/src/plugins/value/engine/transfer_specification.mli
@@ -35,6 +35,6 @@ module Make
val compute_using_specification:
warn:bool ->
kinstr -> (Abstract.Loc.location, Abstract.Val.t) call -> spec ->
- Abstract.Dom.t -> Abstract.Dom.t list or_bottom
+ (Partition.key * Abstract.Dom.t) -> (Partition.key * Abstract.Dom.t) list
end
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 1ce8dd5d91e..48c36f6d513 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -25,26 +25,28 @@ open Cil_datatype
open Eval
module type S = sig
+ type pkey = Partition.key
type state
type value
type loc
val assign: state -> kinstr -> lval -> exp -> state or_bottom
val assume: state -> stmt -> exp -> bool -> state or_bottom
val call:
- stmt -> lval option -> exp -> exp list -> state ->
- state list or_bottom * Eval.cacheable
+ stmt -> lval option -> exp -> exp list -> pkey -> state ->
+ (pkey*state) list * Eval.cacheable
val check_unspecified_sequence:
stmt ->
state -> (stmt * lval list * lval list * lval list * stmt ref list) list ->
unit or_bottom
val enter_scope: kernel_function -> varinfo list -> state -> state
type call_result = {
- states: state list or_bottom;
+ states: (pkey * state) list;
cacheable: Eval.cacheable;
builtin: bool;
}
val compute_call_ref:
- (stmt -> (loc, value) call -> recursion option ->state -> call_result) ref
+ (stmt -> (loc, value) call -> recursion option -> pkey -> state ->
+ call_result) ref
end
(* Reference filled in by the callwise-inout callback *)
@@ -119,6 +121,7 @@ module Make (Abstract: Abstractions.Eva) = struct
module Domain = Abstract.Dom
module Eval = Abstract.Eval
+ type pkey = Partition.key
type state = Domain.t
type value = Value.t
type loc = Location.location
@@ -296,19 +299,20 @@ module Make (Abstract: Abstractions.Eva) = struct
(* ------------------------------------------------------------------------ *)
type call_result = {
- states: state list or_bottom;
+ states: (pkey * state) list;
cacheable: cacheable;
builtin: bool;
}
(* Forward reference to [Eval_funs.compute_call] *)
let compute_call_ref :
- (stmt -> (loc, value) call -> recursion option -> state -> call_result) ref
+ (stmt -> (loc, value) call -> recursion option -> pkey -> state ->
+ call_result) ref
= ref (fun _ -> assert false)
(* Returns the result of a call, and a boolean that indicates whether a
builtin has been used to interpret the call. *)
- let process_call stmt call recursion valuation state =
+ let process_call stmt call recursion valuation pkey state =
Value_util.push_call_stack call.kf (Kstmt stmt);
let cleanup () =
Value_util.pop_call_stack ();
@@ -322,9 +326,9 @@ module Make (Abstract: Abstractions.Eva) = struct
match Domain.start_call stmt call recursion domain_valuation state with
| `Value state ->
Domain.Store.register_initial_state (Value_util.call_stack ()) state;
- !compute_call_ref stmt call recursion state
+ !compute_call_ref stmt call recursion pkey state
| `Bottom ->
- { states = `Bottom; cacheable = Cacheable; builtin=false }
+ { states = []; cacheable = Cacheable; builtin=false }
in
cleanup ();
res
@@ -455,13 +459,11 @@ module Make (Abstract: Abstractions.Eva) = struct
Kernel_function.get_formals kf @ locals
(* Do the call to one function. *)
- let do_one_call valuation stmt lv call recursion state =
+ let do_one_call valuation stmt lv call recursion key state =
let kf_callee = call.kf in
let pre = state in
(* Process the call according to the domain decision. *)
- let call_result = process_call stmt call recursion valuation state in
- call_result.cacheable,
- call_result.states >>- fun result ->
+ let call_result = process_call stmt call recursion valuation key state in
let leaving_vars = leaving_vars kf_callee in
(* Do not try to reduce concrete arguments if a builtin was used. *)
let gather_reduced_arguments =
@@ -488,11 +490,11 @@ module Make (Abstract: Abstractions.Eva) = struct
in
let states =
List.fold_left
- (fun acc return -> Bottom.add_to_list (process return) acc)
- [] result
+ (fun acc (k,x) -> Bottom.add_to_list (process x >>-: fun y -> k,y) acc)
+ [] call_result.states
in
InOutCallback.clear ();
- Bottom.bot_of_list states
+ call_result.cacheable, states
(* ------------------- Evaluation of the arguments ------------------------ *)
@@ -737,7 +739,7 @@ module Make (Abstract: Abstractions.Eva) = struct
(* --------------------- Process the call statement ---------------------- *)
- let call stmt lval_option funcexp args state =
+ let call stmt lval_option funcexp args pkey state =
let ki_call = Kstmt stmt in
let subdivnb = subdivide_stmt stmt in
(* Resolve [funcexp] into the called kernel functions. *)
@@ -747,39 +749,39 @@ module Make (Abstract: Abstractions.Eva) = struct
Alarmset.emit ki_call alarms;
let cacheable = ref Cacheable in
let eval =
- functions >>- fun functions ->
+ functions >>-: fun functions ->
let current_kf = Value_util.current_kf () in
let process_one_function kf valuation =
(* The special Frama_C_ functions to print states are handled here. *)
if apply_special_directives ~subdivnb kf args state
then
let () = apply_cvalue_callback kf ki_call state in
- `Value ([state])
+ [(pkey,state)]
else
(* Create the call. *)
let eval, alarms = make_call ~subdivnb kf args valuation state in
Alarmset.emit ki_call alarms;
- eval >>- fun (call, recursion, valuation) ->
- (* Register the call. *)
- Value_results.add_kf_caller call.kf ~caller:(current_kf, stmt);
- (* Do the call. *)
- let c, states =
- do_one_call valuation stmt lval_option call recursion state
+ let states = eval >>-: fun (call, recursion, valuation) ->
+ (* Register the call. *)
+ Value_results.add_kf_caller call.kf ~caller:(current_kf, stmt);
+ (* Do the call. *)
+ let c, states =
+ do_one_call valuation stmt lval_option call recursion pkey state
+ in
+ (* If needed, propagate that callers cannot be cached. *)
+ if c = NoCacheCallers then
+ cacheable := NoCacheCallers;
+ states
in
- (* If needed, propagate that callers cannot be cached. *)
- if c = NoCacheCallers then
- cacheable := NoCacheCallers;
- states
+ Bottom.list_of_bot states
in
(* Process each possible function apart, and append the result list. *)
let process acc (kf, valuation) =
- let res = process_one_function kf valuation in
- (Bottom.list_of_bot res) @ acc
+ process_one_function kf valuation @ acc
in
- let states_list = List.fold_left process [] functions in
- Bottom.bot_of_list states_list
+ List.fold_left process [] functions
in
- eval, !cacheable
+ Bottom.list_of_bot eval, !cacheable
(* ------------------------------------------------------------------------ *)
(* Unspecified Sequence *)
diff --git a/src/plugins/value/engine/transfer_stmt.mli b/src/plugins/value/engine/transfer_stmt.mli
index 87c505e2411..4be96180e16 100644
--- a/src/plugins/value/engine/transfer_stmt.mli
+++ b/src/plugins/value/engine/transfer_stmt.mli
@@ -27,6 +27,7 @@ val current_kf_inout: unit -> Inout_type.t option
module type S = sig
+ type pkey = Partition.key
type state
type value
type loc
@@ -36,8 +37,8 @@ module type S = sig
val assume: state -> stmt -> exp -> bool -> state or_bottom
val call:
- stmt -> lval option -> exp -> exp list -> state ->
- state list or_bottom * Eval.cacheable
+ stmt -> lval option -> exp -> exp list -> pkey -> state ->
+ (pkey*state) list * Eval.cacheable
val check_unspecified_sequence:
Cil_types.stmt ->
@@ -49,13 +50,13 @@ module type S = sig
val enter_scope: kernel_function -> varinfo list -> state -> state
type call_result = {
- states: state list or_bottom;
+ states: (pkey * state) list;
cacheable: Eval.cacheable;
builtin: bool;
}
val compute_call_ref:
- (stmt -> (loc, value) call -> recursion option -> state -> call_result) ref
+ (stmt -> (loc, value) call -> recursion option -> pkey -> state -> call_result) ref
end
module Make (Abstract: Abstractions.Eva)
diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml
index 1867b8a0720..6919f7e7e73 100644
--- a/src/plugins/value/partitioning/partition.ml
+++ b/src/plugins/value/partitioning/partition.ml
@@ -34,6 +34,38 @@ let new_monitor ~split_limit = {
split_values = Datatype.Integer.Set.empty;
}
+module SplitMonitor = Datatype.Make_with_collections (
+ struct
+ open Datatype
+ include Serializable_undefined
+
+ module Values = Integer.Set
+
+ type t = split_monitor
+
+ let name = "Partition.SplitMonitor"
+
+ let reprs = [ new_monitor ~split_limit:0 ]
+
+ let structural_descr =
+ Structural_descr.t_record [| Int.packed_descr; Values.packed_descr |]
+
+ let compare m1 m2 =
+ let c = Int.compare m1.split_limit m2.split_limit in
+ if c <> 0 then c else Values.compare m1.split_values m2.split_values
+
+ let equal = from_compare
+
+ let pretty fmt m =
+ Format.fprintf fmt "%d/%d" (Values.cardinal m.split_values) m.split_limit
+
+ let hash m =
+ FCHashtbl.hash (Int.hash m.split_limit, Values.hash m.split_values)
+
+ let copy m =
+ { m with split_values = m.split_values }
+ end)
+
(* --- Stamp rationing --- *)
(* Stamps used to label states according to slevel.
@@ -57,24 +89,45 @@ type split_term = Eva_annotations.split_term =
| Expression of Cil_types.exp
| Predicate of Cil_types.predicate
-module SplitTerm = struct
- type t = split_term
- let compare x y =
- match x, y with
- | Expression e1, Expression e2 -> Cil_datatype.ExpStructEq.compare e1 e2
- | Predicate p1, Predicate p2 -> Logic_utils.compare_predicate p1 p2
- | Expression _, Predicate _ -> 1
- | Predicate _, Expression _ -> -1
-
- let pretty fmt = function
- | Expression e -> Printer.pp_exp fmt e
- | Predicate p -> Printer.pp_predicate fmt p
-end
+module SplitTerm = Datatype.Make_with_collections (struct
+ open Datatype
+ include Serializable_undefined
-module SplitMap = Map.Make (SplitTerm)
-module IntPair = Datatype.Pair (Datatype.Int) (Datatype.Int)
-module LoopList = Datatype.List (IntPair)
-module BranchList = Datatype.List (Datatype.Int)
+ module Expressions = Cil_datatype.ExpStructEq
+ module Predicates = Cil_datatype.PredicateStructEq
+
+ type t = split_term
+
+ let name = "Partition.SplitTerm"
+
+ let reprs =
+ Stdlib.List.map (fun e -> Expression e) Expressions.reprs @
+ Stdlib.List.map (fun p -> Predicate p) Predicates.reprs
+
+ let structural_descr =
+ Structural_descr.t_sum [|
+ [| Expressions.packed_descr |] ;
+ [| Predicates.packed_descr |] |]
+
+ let compare x y =
+ match x, y with
+ | Expression e1, Expression e2 -> Expressions.compare e1 e2
+ | Predicate p1, Predicate p2 -> Logic_utils.compare_predicate p1 p2
+ | Expression _, Predicate _ -> 1
+ | Predicate _, Expression _ -> -1
+
+ let equal = from_compare
+
+ let pretty fmt = function
+ | Expression e -> Printer.pp_exp fmt e
+ | Predicate p -> Printer.pp_predicate fmt p
+
+ let hash = function
+ | Expression e -> FCHashtbl.hash (1,Expressions.hash e)
+ | Predicate p -> FCHashtbl.hash (2,Predicates.hash p)
+ end)
+
+module SplitMap = SplitTerm.Map
type branch = int
@@ -110,7 +163,14 @@ type key = {
module Key =
struct
- type t = key
+ open Datatype
+
+ module IntPair = Pair (Int) (Int)
+ module Stamp = Option (IntPair)
+ module BranchList = List (Int)
+ module LoopList = List (IntPair)
+ module Splits = SplitMap.Make (Integer)
+ module DSplits = SplitMap.Make (SplitMonitor)
(* Initial key, before any partitioning *)
let zero = {
@@ -121,43 +181,88 @@ struct
dynamic_splits = SplitMap.empty;
}
- let compare k1 k2 =
- let (<?>) c (cmp,x,y) =
- if c = 0 then cmp x y else c
- in
- Option.compare IntPair.compare k1.ration_stamp k2.ration_stamp
- <?> (LoopList.compare, k1.loops, k2.loops)
- <?> (SplitMap.compare Integer.compare, k1.splits, k2.splits)
- <?> (SplitMap.compare (fun _ _ -> 0), k1.dynamic_splits, k2.dynamic_splits)
- <?> (BranchList.compare, k1.branches, k2.branches)
-
- let pretty fmt key =
- begin match key.ration_stamp with
- | Some (n,_) -> Format.fprintf fmt "#%d" n
- | None -> ()
- end;
- Pretty_utils.pp_list ~pre:"[@[" ~sep:" ;@ " ~suf:"@]]"
- Format.pp_print_int
- fmt
- key.branches;
- Pretty_utils.pp_list ~pre:"(@[" ~sep:" ;@ " ~suf:"@])"
- (fun fmt (i,_j) -> Format.pp_print_int fmt i)
- fmt
- key.loops;
- Pretty_utils.pp_list ~pre:"{@[" ~sep:" ;@ " ~suf:"@]}"
- (fun fmt (t, i) -> Format.fprintf fmt "%a:%a"
- SplitTerm.pretty t
- (Integer.pretty ~hexa:false) i)
- fmt
- (SplitMap.bindings key.splits)
+ include Make_with_collections (struct
+ include Serializable_undefined
+
+ type t = key
+
+ let name = "Partition.Key"
+
+ let reprs = [ zero ]
+
+ let structural_descr =
+ Structural_descr.t_record [|
+ Stamp.packed_descr;
+ BranchList.packed_descr;
+ LoopList.packed_descr;
+ Splits.packed_descr;
+ DSplits.packed_descr;
+ |]
+
+ let compare k1 k2 =
+ let (<?>) c (cmp,x,y) =
+ if c = 0 then cmp x y else c
+ in
+ Stamp.compare k1.ration_stamp k2.ration_stamp
+ <?> (LoopList.compare, k1.loops, k2.loops)
+ <?> (Splits.compare, k1.splits, k2.splits)
+ (* Ignore monitors in comparison *)
+ <?> (SplitMap.compare (fun _ _ -> 0), k1.dynamic_splits, k2.dynamic_splits)
+ <?> (BranchList.compare, k1.branches, k2.branches)
+
+ let equal = from_compare
+
+ let hash k =
+ Stdlib.Hashtbl.hash (
+ Stamp.hash k.ration_stamp,
+ BranchList.hash k.branches,
+ LoopList.hash k.loops,
+ Splits.hash k.splits,
+ DSplits.hash k.dynamic_splits) (* Monitors probably shouldn't be hashed *)
+
+ let pretty fmt key =
+ begin match key.ration_stamp with
+ | Some (n,_) -> Format.fprintf fmt "#%d" n
+ | None -> ()
+ end;
+ Pretty_utils.pp_list ~pre:"[@[" ~sep:" ;@ " ~suf:"@]]"
+ Format.pp_print_int
+ fmt
+ key.branches;
+ Pretty_utils.pp_list ~pre:"(@[" ~sep:" ;@ " ~suf:"@])"
+ (fun fmt (i,_j) -> Format.pp_print_int fmt i)
+ fmt
+ key.loops;
+ Pretty_utils.pp_list ~pre:"{@[" ~sep:" ;@ " ~suf:"@]}"
+ (fun fmt (t, i) -> Format.fprintf fmt "%a:%a"
+ SplitTerm.pretty t
+ Integer.pretty i)
+ fmt
+ (SplitMap.bindings key.splits)
+ end)
let exceed_rationing key = key.ration_stamp = None
+
+ let recombine k1 k2 =
+ let merge_split _ v1 v2 =
+ match v1, v2 with
+ | None, None -> None
+ | Some v, None | None, Some v -> Some v
+ | Some _v1, Some v2 -> Some v2 (* Keep the newest split value *)
+ in {
+ ration_stamp = k2.ration_stamp;
+ branches = k2.branches @ k1.branches;
+ loops = k1.loops;
+ splits = SplitMap.merge merge_split k1.splits k2.splits;
+ dynamic_splits =
+ SplitMap.merge merge_split k1.dynamic_splits k2.dynamic_splits;
+ }
end
(* --- Partitions --- *)
-module KMap = Map.Make (Key)
+module KMap = Key.Map
type 'a partition = 'a KMap.t
@@ -171,8 +276,8 @@ let map = KMap.map
let filter = KMap.filter
let merge = KMap.merge
-let to_list (p : 'a partition) : 'a list =
- KMap.fold (fun _k x l -> x :: l) p []
+let to_list (p : 'a partition) : (key*'a) list =
+ KMap.fold (fun k x l -> (k,x) :: l) p []
(* --- Partitioning actions --- *)
@@ -511,20 +616,20 @@ struct
in
map_keys transfer p
- let transfer_states (f : state -> state list) (p : t) : t =
+ let transfer (f : (key * state) -> (key*state) list) (p : t) : t =
let n = ref 0 in
let transfer acc (k,x) =
- let add =
+ let add l (k,y) =
match k.ration_stamp with
(* No ration stamp, just add the state to the list *)
- | None -> fun l y -> (k,y) :: l
+ | None -> (k,y) :: l
(* There is a ration stamp, set the second part of the stamp to a unique transfer number *)
- | Some (s,_) -> fun l y ->
+ | Some (s,_) ->
let k' = { k with ration_stamp = Some (s, !n) } in
incr n;
(k',y) :: l
in
- List.fold_left add acc (f x)
+ List.fold_left add acc (f (k,x))
in
List.fold_left transfer [] p
diff --git a/src/plugins/value/partitioning/partition.mli b/src/plugins/value/partitioning/partition.mli
index fe3dc9f303f..662995e4053 100644
--- a/src/plugins/value/partitioning/partition.mli
+++ b/src/plugins/value/partitioning/partition.mli
@@ -42,10 +42,10 @@
type key
module Key : sig
- val zero : key (** Initial key: no partitioning. *)
- val compare : key -> key -> int
- val pretty : Format.formatter -> key -> unit
- val exceed_rationing: key -> bool
+ include Datatype.S_with_collections with type t = key
+ val zero : t (** Initial key: no partitioning. *)
+ val exceed_rationing: t -> bool
+ val recombine : t -> t -> t (** Recombinaison of keys after a call *)
end
(** Collection of states, each identified by a unique key. *)
@@ -54,7 +54,7 @@ type 'state partition
val empty : 'a partition
val is_empty : 'a partition -> bool
val size : 'a partition -> int
-val to_list : 'a partition -> 'a list
+val to_list : 'a partition -> (key*'a) list
val find : key -> 'a partition -> 'a
val replace : key -> 'a -> 'a partition -> 'a partition
val merge : (key -> 'a option -> 'b option -> 'c option) -> 'a partition ->
@@ -182,8 +182,8 @@ sig
val union : t -> t -> t
+ val transfer : ((key * state) -> (key * state) list) -> t -> t
val transfer_keys : t -> action -> t
- val transfer_states : (state -> state list) -> t -> t
val iter : (state -> unit) -> t -> unit
val filter_map: (key -> state -> state option) -> t -> t
diff --git a/src/plugins/value/partitioning/trace_partitioning.ml b/src/plugins/value/partitioning/trace_partitioning.ml
index 9ba46bb5eef..d70eaeb3ded 100644
--- a/src/plugins/value/partitioning/trace_partitioning.ml
+++ b/src/plugins/value/partitioning/trace_partitioning.ml
@@ -112,13 +112,13 @@ struct
(* Accessors *)
- let expanded (s : store) : state list =
+ let expanded (s : store) : (key*state) list =
Partition.to_list s.store_partition
let smashed (s : store) : state or_bottom =
match expanded s with
| [] -> `Bottom
- | v1 :: l -> `Value (List.fold_left Domain.join v1 l)
+ | (_k,v1) :: l -> `Value (List.fold_left Domain.join v1 (List.map snd l))
let contents (flow : flow) : state list =
Flow.to_list flow
@@ -210,7 +210,7 @@ struct
in
into.tank_states <- Partition.merge join into.tank_states new_states
- let transfer = Flow.transfer_states
+ let transfer = Flow.transfer
let output_slevel : int -> unit =
let slevel_display_step = Value_parameters.ShowSlevel.get () in
@@ -239,7 +239,8 @@ struct
in
(* Get every source flow *)
let sources_states =
- match sources with
+ (* Is there more than one non-empty incomming flow ? *)
+ match List.filter (fun (_b,f) -> not (Flow.is_empty f)) sources with
| [(_,flow)] -> [flow]
| sources ->
(* Several branches -> partition according to the incoming branch *)
diff --git a/src/plugins/value/partitioning/trace_partitioning.mli b/src/plugins/value/partitioning/trace_partitioning.mli
index 0fbd96f2888..5c208d99b80 100644
--- a/src/plugins/value/partitioning/trace_partitioning.mli
+++ b/src/plugins/value/partitioning/trace_partitioning.mli
@@ -50,7 +50,7 @@ sig
(* --- Accessors --- *)
- val expanded : store -> state list
+ val expanded : store -> (Partition.key * state) list
val smashed : store -> state or_bottom
val contents : flow -> state list
val is_empty_store : store -> bool
@@ -91,7 +91,8 @@ sig
val fill : into:tank -> flow -> unit
(** Apply a transfer function to all the states of a propagation. *)
- val transfer : (state -> state list) -> flow -> flow
+ val transfer : ((Partition.key * state) -> (Partition.key * state) list) ->
+ flow -> flow
(** Join all incoming propagations into the given store. This function returns
a set of states which still need to be propagated past the store.
diff --git a/tests/value/oracle/partitioning-annots.2.res.oracle b/tests/value/oracle/partitioning-annots.2.res.oracle
index da1dee03a86..5c65066b2aa 100644
--- a/tests/value/oracle/partitioning-annots.2.res.oracle
+++ b/tests/value/oracle/partitioning-annots.2.res.oracle
@@ -11,9 +11,6 @@
[eva] tests/value/partitioning-annots.c:127:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva] computing for function Frama_C_interval <- test_loop_split.
- Called from tests/value/partitioning-annots.c:127.
-[eva] Done for function Frama_C_interval
[eva] tests/value/partitioning-annots.c:125: starting to merge loop iterations
[eva] computing for function Frama_C_interval <- test_loop_split.
Called from tests/value/partitioning-annots.c:127.
diff --git a/tests/value/oracle/partitioning-interproc.0.res.oracle b/tests/value/oracle/partitioning-interproc.0.res.oracle
index 8fdc67327c5..32cae5f4258 100644
--- a/tests/value/oracle/partitioning-interproc.0.res.oracle
+++ b/tests/value/oracle/partitioning-interproc.0.res.oracle
@@ -12,9 +12,9 @@
[eva] Done for function Frama_C_nondet
[eva] Recording results for cassign
[eva] Done for function cassign
-[eva:alarm] tests/value/partitioning-interproc.c:25: Warning:
- accessing uninitialized left-value. assert \initialized(&x);
[eva] tests/value/partitioning-interproc.c:26: Frama_C_show_each: {1}
+[eva] tests/value/partitioning-interproc.c:30:
+ Reusing old results for call to cassign
[eva] computing for function cassign <- cassign_test.
Called from tests/value/partitioning-interproc.c:30.
[eva] computing for function Frama_C_nondet <- cassign <- cassign_test.
@@ -22,15 +22,6 @@
[eva] Done for function Frama_C_nondet
[eva] Recording results for cassign
[eva] Done for function cassign
-[eva] computing for function cassign <- cassign_test.
- Called from tests/value/partitioning-interproc.c:30.
-[eva] computing for function Frama_C_nondet <- cassign <- cassign_test.
- Called from tests/value/partitioning-interproc.c:11.
-[eva] Done for function Frama_C_nondet
-[eva] Recording results for cassign
-[eva] Done for function cassign
-[eva:alarm] tests/value/partitioning-interproc.c:31: Warning:
- accessing uninitialized left-value. assert \initialized(&x);
[eva] tests/value/partitioning-interproc.c:32: Frama_C_show_each: {1}
[eva] tests/value/partitioning-interproc.c:32: Frama_C_show_each: {1}
[eva] Recording results for cassign_test
diff --git a/tests/value/oracle/partitioning-interproc.1.res.oracle b/tests/value/oracle/partitioning-interproc.1.res.oracle
index a2bde102b39..dfd3684a605 100644
--- a/tests/value/oracle/partitioning-interproc.1.res.oracle
+++ b/tests/value/oracle/partitioning-interproc.1.res.oracle
@@ -14,7 +14,7 @@
[eva:final-states] Values at end of function fabs:
__retres ∈ [-0. .. 1.79769313486e+308]
[eva:final-states] Values at end of function fabs_test:
- x ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ x ∈ [-1. .. 1.]
[from] Computing for function fabs
[from] Done for function fabs
[from] Computing for function fabs_test
diff --git a/tests/value/oracle/split_return.0.res.oracle b/tests/value/oracle/split_return.0.res.oracle
index 3c39daac772..7606908946d 100644
--- a/tests/value/oracle/split_return.0.res.oracle
+++ b/tests/value/oracle/split_return.0.res.oracle
@@ -32,8 +32,8 @@
Called from tests/value/split_return.i:51.
[eva] Recording results for f2
[eva] Done for function f2
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5; 7}, {5}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
[eva] tests/value/split_return.i:54: assertion got status valid.
[eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {5; 7}, {5}
[eva] tests/value/split_return.i:57: assertion got status valid.
@@ -72,8 +72,8 @@
Called from tests/value/split_return.i:120.
[eva] Recording results for f5
[eva] Done for function f5
-[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {-2}, {0}
[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {7}, {5}
+[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {-2}, {0}
[eva] tests/value/split_return.i:123: assertion got status valid.
[eva] tests/value/split_return.i:125: assertion got status valid.
[eva] Recording results for main5
diff --git a/tests/value/oracle/split_return.1.res.oracle b/tests/value/oracle/split_return.1.res.oracle
index e161e8a2114..7410bd57efb 100644
--- a/tests/value/oracle/split_return.1.res.oracle
+++ b/tests/value/oracle/split_return.1.res.oracle
@@ -34,8 +34,8 @@
Called from tests/value/split_return.i:51.
[eva] Recording results for f2
[eva] Done for function f2
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5; 7}, {5}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
[eva] tests/value/split_return.i:54: assertion got status valid.
[eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {5; 7}, {5}
[eva] tests/value/split_return.i:57: assertion got status valid.
@@ -47,8 +47,8 @@
Called from tests/value/split_return.i:76.
[eva] Recording results for f3
[eva] Done for function f3
-[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2}, {0}
[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2}, {0}
[eva] tests/value/split_return.i:79: assertion got status valid.
[eva] tests/value/split_return.i:81: assertion got status valid.
[eva] Recording results for main3
@@ -59,8 +59,8 @@
Called from tests/value/split_return.i:97.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
[eva] tests/value/split_return.i:100: assertion got status valid.
[eva] tests/value/split_return.i:102: assertion got status valid.
[eva] Recording results for main4
@@ -71,8 +71,8 @@
Called from tests/value/split_return.i:120.
[eva] Recording results for f5
[eva] Done for function f5
-[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {-2}, {0}
[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {7}, {5}
+[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {-2}, {0}
[eva] tests/value/split_return.i:123: assertion got status valid.
[eva] tests/value/split_return.i:125: assertion got status valid.
[eva] Recording results for main5
@@ -104,8 +104,8 @@
Called from tests/value/split_return.i:174.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:175: 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 9751f1d7147..cbcd6482358 100644
--- a/tests/value/oracle/split_return.4.res.oracle
+++ b/tests/value/oracle/split_return.4.res.oracle
@@ -472,8 +472,8 @@
Called from tests/value/split_return.i:51.
[eva] Recording results for f2
[eva] Done for function f2
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5; 7}, {5}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
[eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {5; 7}, {5}
[eva] Recording results for main2
[eva] Done for function main2
diff --git a/tests/value/partitioning-interproc.c b/tests/value/partitioning-interproc.c
index 034c5223034..1b42df1bfba 100644
--- a/tests/value/partitioning-interproc.c
+++ b/tests/value/partitioning-interproc.c
@@ -1,7 +1,7 @@
/* run.config*
GCC:
STDOPT: #"-main cassign_test -eva-partition-history 1"
- STDOPT: #"-main fabs_test -eva-partition-history 1 -eva-equality-domain"
+ STDOPT: #"-main fabs_test -eva-partition-history 1 -eva-domains equality"
*/
#include "__fc_builtin.h"
--
GitLab