From 11fc7b51a768a9874279393de6cb4d71d9ae5f0b Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 12 Sep 2022 16:57:30 +0200
Subject: [PATCH] [Extlib] removed opt_fold (Option.fold)
---
src/kernel_services/ast_data/annotations.ml | 8 +++++---
src/libraries/stdlib/extlib.ml | 5 -----
src/libraries/stdlib/extlib.mli | 3 ---
src/plugins/dive/dive_graph.ml | 3 ++-
src/plugins/eva/domains/cvalue/cvalue_domain.ml | 7 +++----
src/plugins/eva/domains/gauges/gauges_domain.ml | 3 ++-
src/plugins/eva/domains/offsm_domain.ml | 3 ++-
src/plugins/eva/domains/simple_memory.ml | 9 ++++++---
src/plugins/eva/domains/symbolic_locs.ml | 3 ++-
src/plugins/eva/engine/mem_exec.ml | 3 ++-
src/plugins/eva/engine/transfer_stmt.ml | 3 ++-
11 files changed, 26 insertions(+), 24 deletions(-)
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index e1d697bb238..480675355fe 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -694,12 +694,14 @@ let fold_disjoint f =
(fun f l acc -> List.fold_left (Fun.flip f) acc l)
f
+let fold_opt_spec f opt default =
+ Option.fold ~some:(fun v -> f v default) ~none:default opt
+
let fold_terminates f =
- fold_spec_gen
- (fun s -> s.spec_terminates) Extlib.opt_fold f
+ fold_spec_gen (fun s -> s.spec_terminates) fold_opt_spec f
let fold_decreases f =
- fold_spec_gen (fun s -> s.spec_variant) Extlib.opt_fold f
+ fold_spec_gen (fun s -> s.spec_variant) fold_opt_spec f
let fold_bhv_gen get fold f kf b acc =
let get spec =
diff --git a/src/libraries/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml
index 301f71af912..0ce56cce839 100644
--- a/src/libraries/stdlib/extlib.ml
+++ b/src/libraries/stdlib/extlib.ml
@@ -220,11 +220,6 @@ let list_slice ?(first = 0) ?last l =
(** {2 Options} *)
(* ************************************************************************* *)
-let opt_fold f o b =
- match o with
- | None -> b
- | Some a -> f a b
-
let merge_opt f k o1 o2 =
match o1,o2 with
| None, None -> None
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index 2173d5cf200..c641d93e5f3 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -177,9 +177,6 @@ val list_slice: ?first:int -> ?last:int -> 'a list -> 'a list
(** {2 Options} *)
(* ************************************************************************* *)
-val opt_fold: ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
-(** @since Oxygen-20120901 *)
-
(** [merge f k a b] returns
- [None] if both [a] and [b] are [None]
- [Some a'] (resp. [b'] if [b] (resp [a]) is [None]
diff --git a/src/plugins/dive/dive_graph.ml b/src/plugins/dive/dive_graph.ml
index 4f16e8c40ff..736d4eb7df4 100644
--- a/src/plugins/dive/dive_graph.ml
+++ b/src/plugins/dive/dive_graph.ml
@@ -124,8 +124,9 @@ let edges g =
let update_node_values node new_values typ =
+ let join n = Cvalue.V.join n new_values in
node.node_values <-
- Some (Extlib.opt_fold Cvalue.V.join node.node_values new_values);
+ Some (Option.fold ~some:join ~none:new_values node.node_values);
node.node_range <-
Node_range.(upper_bound node.node_range (evaluate new_values typ))
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index 68d1f194f99..87574b29cf8 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -270,11 +270,10 @@ module State = struct
let (pre, clob) = pre in
let (post, post_clob) = post in
Locals_scoping.(remember_bases_with_locals clob post_clob.clob);
- let post =
- Extlib.opt_fold
- (finalize_recursive_call stmt call ~pre:(pre, clob))
- recursion post
+ let finalize a =
+ finalize_recursive_call stmt call ~pre:(pre, clob) a post
in
+ let post = Option.fold ~some:finalize ~none:post recursion in
Cvalue_transfer.finalize_call stmt call recursion ~pre ~post
>>-: fun state ->
state, clob
diff --git a/src/plugins/eva/domains/gauges/gauges_domain.ml b/src/plugins/eva/domains/gauges/gauges_domain.ml
index 829afa08364..0345dca18f3 100644
--- a/src/plugins/eva/domains/gauges/gauges_domain.ml
+++ b/src/plugins/eva/domains/gauges/gauges_domain.ml
@@ -1221,7 +1221,8 @@ module D : Abstract_domain.Leaf
match function_calls_handling with
| FullInterprocedural ->
update valuation state >>-: fun state ->
- Extlib.opt_fold start_recursive_call recursion state
+ let start_recursive_call r = start_recursive_call r state in
+ Option.fold ~some:start_recursive_call ~none:state recursion
| IntraproceduralAll
| IntraproceduralNonReferenced -> `Value G.empty
in
diff --git a/src/plugins/eva/domains/offsm_domain.ml b/src/plugins/eva/domains/offsm_domain.ml
index 396598578c7..56278f16b37 100644
--- a/src/plugins/eva/domains/offsm_domain.ml
+++ b/src/plugins/eva/domains/offsm_domain.ml
@@ -164,7 +164,8 @@ module D : Abstract_domain.Leaf
let start_call _stmt _call recursion valuation state =
update valuation state >>-: fun state ->
- Extlib.opt_fold start_recursive_call recursion state
+ let start_recursive_call r = start_recursive_call r state in
+ Option.fold ~some:start_recursive_call ~none:state recursion
let extract_expr ~oracle:_ _context _state _exp =
`Value (Offsm_value.Offsm.top, None), Alarmset.all
diff --git a/src/plugins/eva/domains/simple_memory.ml b/src/plugins/eva/domains/simple_memory.ml
index a0ba820a46f..833f2ee7072 100644
--- a/src/plugins/eva/domains/simple_memory.ml
+++ b/src/plugins/eva/domains/simple_memory.ml
@@ -266,14 +266,16 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
abstraction of the domain itself. *)
let assume _stmt _expr _pos = update
- let start_recusive_call recursion state =
+ let start_recursive_call recursion state =
let state = remove_variables recursion.withdrawal state in
(* No collision should occur in the substitution. *)
let decide _key _v1 _v2 = assert false in
snd (replace_key ~decide recursion.base_substitution state)
let start_call _stmt call recursion _valuation state =
- let state = Extlib.opt_fold start_recusive_call recursion state in
+ let state =
+ let start_recursive_call r = start_recursive_call r state in
+ Option.fold ~some:start_recursive_call ~none:state recursion in
let bind_argument state argument =
let typ = argument.formal.vtype in
let loc = Main_locations.PLoc.eval_varinfo argument.formal in
@@ -292,7 +294,8 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
let finalize_call _stmt call recursion ~pre ~post =
let kf_name = Kernel_function.get_name call.kf in
- let post = Extlib.opt_fold (finalize_recursive_call ~pre) recursion post in
+ let finalize a = finalize_recursive_call ~pre a post in
+ let post = Option.fold ~some:finalize ~none:post recursion in
match find_builtin kf_name, call.return with
| None, _ | _, None -> `Value post
| Some f, Some return ->
diff --git a/src/plugins/eva/domains/symbolic_locs.ml b/src/plugins/eva/domains/symbolic_locs.ml
index 5ab410de611..f1cf77a8110 100644
--- a/src/plugins/eva/domains/symbolic_locs.ml
+++ b/src/plugins/eva/domains/symbolic_locs.ml
@@ -570,7 +570,8 @@ module D : Abstract_domain.Leaf
let start_call _stmt _call recursion valuation state =
update valuation state >>-: fun state ->
- Extlib.opt_fold start_recursive_call recursion state
+ let start_recursive_call r = start_recursive_call r state in
+ Option.fold ~some:start_recursive_call ~none:state recursion
let finalize_call _stmt _call _recursion ~pre:_ ~post = `Value post
diff --git a/src/plugins/eva/engine/mem_exec.ml b/src/plugins/eva/engine/mem_exec.ml
index cf8268830c4..afc4d3c6c05 100644
--- a/src/plugins/eva/engine/mem_exec.ml
+++ b/src/plugins/eva/engine/mem_exec.ml
@@ -193,8 +193,9 @@ module Make
output_bases. *)
let return_varinfo = Library_functions.get_retres_vi kf in
let return_base = Option.map Base.of_varinfo return_varinfo in
+ let add b = Base.Hptset.add b all_output_bases in
let all_output_bases =
- Extlib.opt_fold Base.Hptset.add return_base all_output_bases
+ Option.fold ~some:add ~none:all_output_bases return_base
in
let clear (key,state) =
key, Domain.filter (`Post kf) all_output_bases state
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 09bcb4f40fc..32a76a84692 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -579,7 +579,8 @@ module Make (Abstract: Abstractions.Eva) = struct
>>=: fun (args, valuation) ->
let call = create_call stmt kf args in
let recursion = Recursion.make call in
- let call = Extlib.opt_fold replace_recursive_call recursion call in
+ let replace a = replace_recursive_call a call in
+ let call = Option.fold ~some:replace ~none:call recursion in
call, recursion, valuation
(* ----------------- show_each and dump_each directives ------------------- *)
--
GitLab