diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index e1d697bb2386de590f466fd3ff2ea83fec339199..480675355fe95555a4b80e902deb9def6454b80f 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 301f71af9128babd1e31b073d1dd98707d442bc1..0ce56cce8396b6288638839fe49ba4e33ff581d1 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 2173d5cf2006596f95e1eccb6ac838be663241ca..c641d93e5f379f9cfc360c580aec17dbddda726b 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 4f16e8c40ff105ee5022b049c70c9c47301567a8..736d4eb7df4977cc4acc74863add651286e3d155 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 68d1f194f995758cef798ecbed61fbfd4c22ce52..87574b29cf8747b96e16c42d3cf64343d9b009e4 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 829afa083647c8d8e174c8e8c3a1303b840df1c9..0345dca18f3e9f21244683633b12aa460cee64e8 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 396598578c7eb76547068d810671bdde1078ab3b..56278f16b372c9cd474a2bf7d49836a4b479105b 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 a0ba820a46fc63cde8dd2449ba2787a536ac2c76..833f2ee70725949cc8cfa4c11dda47af780e39a3 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 5ab410de611174dfee0f7a2ec1e9c1b20f128cea..f1cf77a8110ff90e0a1aaa406ce13f91155ff211 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 cf8268830c4cdfa967b46f8527067d1a27423d03..afc4d3c6c05a324ed8b3247358461578bd11d3d3 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 09bcb4f40fc720fe7c09bcbe9c2692eb2c10fc34..32a76a8469259eea572599ef7a2ff8b71297da31 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 ------------------- *)