Skip to content
Snippets Groups Projects
Commit 145e07f9 authored by David Bühler's avatar David Bühler
Browse files

[Eva] In partition.ml, renames initial key [zero] to [empty].

parent b9bf8d9b
No related branches found
No related tags found
No related merge requests found
...@@ -312,7 +312,7 @@ module Make (Abstract: Abstractions.Eva) = struct ...@@ -312,7 +312,7 @@ module Make (Abstract: Abstractions.Eva) = struct
Builtins.apply_builtin builtin cvalue_call ~pre:cvalue_state ~post Builtins.apply_builtin builtin cvalue_call ~pre:cvalue_state ~post
in in
let insert cvalue_state = let insert cvalue_state =
Partition.Key.zero, Partition.Key.empty,
Abstract.Dom.set Cvalue_domain.State.key cvalue_state final_state Abstract.Dom.set Cvalue_domain.State.key cvalue_state final_state
in in
let states = List.map insert cvalue_states in let states = List.map insert cvalue_states in
......
...@@ -582,6 +582,6 @@ module Make ...@@ -582,6 +582,6 @@ module Make
let states = let states =
compute_specification ~warn kinstr call.kf call.return spec state compute_specification ~warn kinstr call.kf call.return spec state
in in
List.map (fun s -> Partition.Key.zero, s) (States.to_list states) List.map (fun s -> Partition.Key.empty, s) (States.to_list states)
end end
...@@ -753,7 +753,7 @@ module Make (Abstract: Abstractions.Eva) = struct ...@@ -753,7 +753,7 @@ module Make (Abstract: Abstractions.Eva) = struct
if apply_special_directives ~subdivnb kf args state if apply_special_directives ~subdivnb kf args state
then then
let () = apply_cvalue_callback kf ki_call state in let () = apply_cvalue_callback kf ki_call state in
[(Partition.Key.zero,state)] [(Partition.Key.empty, state)]
else else
(* Create the call. *) (* Create the call. *)
let eval, alarms = make_call ~subdivnb kf args valuation state in let eval, alarms = make_call ~subdivnb kf args valuation state in
......
...@@ -177,7 +177,7 @@ struct ...@@ -177,7 +177,7 @@ struct
module DSplits = SplitMap.Make (SplitMonitor) module DSplits = SplitMap.Make (SplitMonitor)
(* Initial key, before any partitioning *) (* Initial key, before any partitioning *)
let zero = { let empty = {
ration_stamp = None; ration_stamp = None;
branches = []; branches = [];
loops = []; loops = [];
...@@ -192,7 +192,7 @@ struct ...@@ -192,7 +192,7 @@ struct
let name = "Partition.Key" let name = "Partition.Key"
let reprs = [ zero ] let reprs = [ empty ]
let structural_descr = let structural_descr =
Structural_descr.t_record [| Structural_descr.t_record [|
...@@ -324,7 +324,7 @@ struct ...@@ -324,7 +324,7 @@ struct
let empty = [] let empty = []
let initial (p : 'a list) : t = let initial (p : 'a list) : t =
List.map (fun state -> Key.zero, state) p List.map (fun state -> Key.empty, state) p
let to_list (f : t) : state list = let to_list (f : t) : state list =
List.map snd f List.map snd f
......
...@@ -50,7 +50,7 @@ type call_return_policy = { ...@@ -50,7 +50,7 @@ type call_return_policy = {
module Key : sig module Key : sig
include Datatype.S_with_collections with type t = key include Datatype.S_with_collections with type t = key
val zero : t (** Initial key: no partitioning. *) val empty : t (** Initial key: no partitioning. *)
val exceed_rationing: t -> bool val exceed_rationing: t -> bool
val combine : policy:call_return_policy -> caller:t -> callee:t -> t val combine : policy:call_return_policy -> caller:t -> callee:t -> t
(** Recombinaison of keys after a call *) (** Recombinaison of keys after a call *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment