diff --git a/bin/migration_scripts/titanium2vanadium.sh b/bin/migration_scripts/titanium2vanadium.sh
index 55b1d33d5443b3e264d88da1c095933fc7e49c8a..bca1c6f017987b7a9a6af8b164b4a1060d563579 100755
--- a/bin/migration_scripts/titanium2vanadium.sh
+++ b/bin/migration_scripts/titanium2vanadium.sh
@@ -103,7 +103,9 @@ process_file ()
-e 's/Extlib\.opt_map/Option.map/g' \
-e 's/Extlib\.has_some/Option.is_some/g' \
-e 's/Extlib\.opt_bind/Option.bind/g' \
- -e 's/Extlib\.the \([^~]\)/Option.get \1/g'
+ -e 's/Extlib\.the \([^~]\)/Option.get \1/g' \
+ -e 's/Extlib\.opt_equal/Option.equal/g' \
+ -e 's/Extlib\.opt_compare/Option.compare/g'
}
apply_one_dir ()
diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index 5c57e0dde86e573fd52f90a075c3f1184510269c..095c1b9cef30592a727e57fd69af31aeb6640c8b 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -66,7 +66,7 @@ module Validity = Datatype.Make
| Unknown (b1, m1, e1), Unknown (b2, m2, e2) ->
let c = Int.compare b1 b2 in
if c = 0 then
- let c = Extlib.opt_compare Int.compare m1 m2 in
+ let c = Option.compare Int.compare m1 m2 in
if c = 0 then Int.compare e1 e2 else c
else c
| Variable v1, Variable v2 ->
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index 0785ae1209cce4dd3abdff0d0c71b3f6185c396f..eefbda4d0b28f0b9c96d180dd9057dad295006d4 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -138,13 +138,13 @@ module D =
if n = 0 then Lval.compare lv1 lv2 else n
| Index_out_of_bound(e11, e12), Index_out_of_bound(e21, e22) ->
let n = Exp.compare e11 e21 in
- if n = 0 then Extlib.opt_compare Exp.compare e12 e22 else n
+ if n = 0 then Option.compare Exp.compare e12 e22 else n
| Invalid_pointer e1, Invalid_pointer e2 -> Exp.compare e1 e2
| Invalid_shift(e1, n1), Invalid_shift(e2, n2) ->
let n = Exp.compare e1 e2 in
- if n = 0 then Extlib.opt_compare Datatype.Int.compare n1 n2 else n
+ if n = 0 then Option.compare Datatype.Int.compare n1 n2 else n
| Pointer_comparison(e11, e12), Pointer_comparison(e21, e22) ->
- let n = Extlib.opt_compare Exp.compare e11 e21 in
+ let n = Option.compare Exp.compare e11 e21 in
if n = 0 then Exp.compare e12 e22 else n
| Overflow(s1, e1, n1, b1), Overflow(s2, e2, n2, b2) ->
let n = Stdlib.compare s1 s2 in
@@ -188,7 +188,7 @@ module D =
| Function_pointer (e1, l1), Function_pointer (e2, l2) ->
let n = Exp.compare e1 e2 in
if n <> 0 then n
- else Extlib.opt_compare (Extlib.list_compare Exp.compare) l1 l2
+ else Option.compare (Extlib.list_compare Exp.compare) l1 l2
| Invalid_bool lv1, Invalid_bool lv2 -> Lval.compare lv1 lv2
| _, (Division_by_zero _ | Memory_access _ |
Index_out_of_bound _ | Invalid_pointer _ |
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index f647488d6c33c49f62bb40c46f80dc632d742d7b..20cfa49ccc1af5984386ab78c5f6230577d7e716 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -591,7 +591,7 @@ include Datatype.Make_with_collections
Kf.equal f1 f2 && Kinstr.equal ki1 ki2
| IPReachable {ir_kf=kf1; ir_kinstr=ki1; ir_program_point=ba1},
IPReachable {ir_kf=kf2; ir_kinstr=ki2; ir_program_point=ba2} ->
- Extlib.opt_equal Kf.equal kf1 kf2 && Kinstr.equal ki1 ki2 && ba1 = ba2
+ Option.equal Kf.equal kf1 kf2 && Kinstr.equal ki1 ki2 && ba1 = ba2
| IPBehavior {ib_kf=f1; ib_kinstr=k1; ib_active=a1; ib_bhv=b1},
IPBehavior {ib_kf=f2; ib_kinstr=k2; ib_active=a2; ib_bhv=b2} ->
Kf.equal f1 f2
@@ -665,7 +665,7 @@ include Datatype.Make_with_collections
if n = 0 then Kinstr.compare ki1 ki2 else n
| IPReachable {ir_kf=kf1; ir_kinstr=ki1; ir_program_point=ba1},
IPReachable {ir_kf=kf2; ir_kinstr=ki2; ir_program_point=ba2} ->
- let n = Extlib.opt_compare Kf.compare kf1 kf2 in
+ let n = Option.compare Kf.compare kf1 kf2 in
if n = 0 then
let n = Kinstr.compare ki1 ki2 in
if n = 0 then Stdlib.compare ba1 ba2 else n
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 003b99cce16b41df6e8882febaad8c7c182092a4..82f5d57783837ad5cbfdb91000694700c0dd9ce7 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -467,9 +467,9 @@ and compare_array_sizes e1o e2o =
match i1, i2 with
| None, None -> (* inconclusive. do not return 0 *)
!compare_exp_struct_eq e1 e2
- | _ -> Extlib.opt_compare Integer.compare i1 i2
+ | _ -> Option.compare Integer.compare i1 i2
in
- Extlib.opt_compare compare_non_empty_size e1o e2o
+ Option.compare compare_non_empty_size e1o e2o
and compare_type config t1 t2 =
if t1 == t2 then 0
@@ -521,7 +521,7 @@ and compare_type config t1 t2 =
index_typ a1 - index_typ a2
and compare_arg_list config l1 l2 =
- Extlib.opt_compare
+ Option.compare
(compare_list
(fun (_n1, t1, l1) (_n2, t2, l2) ->
(compare_chain (compare_type config) t1 t2
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index f602bf07dcbe541966723f30099c0e4fd8d7cce7..339744070b2ce9c7b7f58482accc4c2b03a2ca7b 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -211,7 +211,7 @@ module Value = struct
(fun l ->
if
not
- (Extlib.opt_equal ListArgs.equal (Some l) (FunArgs.get_option ()))
+ (Option.equal ListArgs.equal (Some l) (FunArgs.get_option ()))
then begin
!initial_state_changed ();
FunArgs.set l
@@ -241,7 +241,7 @@ module Value = struct
Db.Value.globals_set_initial_state\" : _ -> unit)"
(Datatype.func Cvalue.Model.ty Datatype.unit)
(fun state ->
- if not (Extlib.opt_equal Cvalue.Model.equal
+ if not (Option.equal Cvalue.Model.equal
(Some state)
(VGlobals.get_option ()))
then begin
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index a2ce1c72e39a2115017d7b4a0619014144b8abe7..cb613d9f70fea864b32f8dd7eabf445ab238b4f3 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -641,7 +641,7 @@ struct
if a == b then 0 else
let cmp = cmp_struct compare a b in
if cmp <> 0 then cmp else
- Extlib.opt_compare Tau.compare a.tau b.tau
+ Option.compare Tau.compare a.tau b.tau
end
@@ -715,7 +715,7 @@ struct
| NOT p,NOT q -> p==q
| CMP(c,a,b),CMP(c',a',b') -> c=c' && a==a' && b==b'
| FUN(f,xs,t) , FUN(g,ys,t') -> Fun.equal f g && Hcons.equal_list (==) xs ys
- && Extlib.opt_equal Tau.equal t t'
+ && Option.equal Tau.equal t t'
| _ -> false
end)
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index e67fd3a8484f1b08c24608dc1718b8a08d7b4eb5..543688032b0413be769eeb7218dbadf009597c92 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -77,8 +77,8 @@ module G = struct
(opt2 fmin bmin1 bmin2, opt2 fmax bmax1 bmax2)
let equal (bmin1, bmax1: t) (bmin2, bmax2: t) =
- Extlib.opt_equal Integer.equal bmin1 bmin2 &&
- Extlib.opt_equal Integer.equal bmax1 bmax2
+ Option.equal Integer.equal bmin1 bmin2 &&
+ Option.equal Integer.equal bmax1 bmax2
let is_included (bmin1, bmax1: t) (bmin2, bmax2: t) =
(match bmin1, bmin2 with
@@ -161,7 +161,7 @@ module G = struct
widening of Ival. *)
let widen ?threshold (min1, max1: t) (min2, max2: t) : t =
let widen_unstable_min b1 b2 =
- if Extlib.opt_equal Integer.equal b1 b2 then b1 else None
+ if Option.equal Integer.equal b1 b2 then b1 else None
in
let widen_unstable_max b1 b2 =
match threshold with
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index 89dd2edae3a5c43ba1e03d5cec48605337bf40f7..6006597e3a143f45b6b8c79988f9786bc30980df 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -145,7 +145,7 @@ end = struct
if c <> 0 then c else
let c = Extlib.list_compare ExpStructEq.compare es1 es2 in
if c <> 0 then c else
- Extlib.opt_compare Lval.compare lv1 lv2
+ Option.compare Lval.compare lv1 lv2
| Msg s1, Msg s2 ->
String.compare s1 s2
| Loop (stmt1, s1, g1), Loop (stmt2, s2, g2) ->
diff --git a/src/plugins/value/gui_files/gui_callstacks_manager.ml b/src/plugins/value/gui_files/gui_callstacks_manager.ml
index 03e7da9770d54803a55eb0eefbe2163b4d899b7d..10331bacd8e173dfa5e8479d97af336b19c5ca30 100644
--- a/src/plugins/value/gui_files/gui_callstacks_manager.ml
+++ b/src/plugins/value/gui_files/gui_callstacks_manager.ml
@@ -428,7 +428,7 @@ module Make (Input: Input) = struct
model.hidden_columns <- [];
in
let start_session loc ~multiple =
- if not (multiple && Extlib.opt_equal gui_loc_equal (Some loc) model.loc)
+ if not (multiple && Option.equal gui_loc_equal (Some loc) model.loc)
then begin
clear_model ();
model.loc <- Some loc;
diff --git a/src/plugins/value/gui_files/gui_types.ml b/src/plugins/value/gui_files/gui_types.ml
index d8eea3776d22e9ad7c044a67bc97f808888f7862..e6b64d5a8e73e16f6e43b4dfbfc6f70458b5b6ee 100644
--- a/src/plugins/value/gui_files/gui_types.ml
+++ b/src/plugins/value/gui_files/gui_types.ml
@@ -148,10 +148,10 @@ module Make (V: Abstractions.Value) = struct
| GR_Empty, GR_Empty -> true
| GR_Offsm (o1, typ1), GR_Offsm (o2, typ2) ->
equal_gui_offsetmap_res o1 o2 &&
- Extlib.opt_equal Cil_datatype.Typ.equal typ1 typ2
+ Option.equal Cil_datatype.Typ.equal typ1 typ2
| GR_Value (v1, typ1), GR_Value (v2, typ2) ->
Eval.Flagged_Value.equal V.equal v1 v2 &&
- Extlib.opt_equal Cil_datatype.Typ.equal typ1 typ2
+ Option.equal Cil_datatype.Typ.equal typ1 typ2
| GR_Status s1, GR_Status s2 -> Extlib.compare_basic s1 s2 = 0
| GR_Zone z1, GR_Zone z2 -> Locations.Zone.equal z1 z2
| (GR_Empty | GR_Offsm _ | GR_Value _ | GR_Status _ | GR_Zone _), _ -> false
diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml
index 977dce271f250ef31d7da65a587b79bb650753f6..f51bc89c5e108f5a29c2a3b8751d5141d6cf050a 100644
--- a/src/plugins/value/partitioning/partition.ml
+++ b/src/plugins/value/partitioning/partition.ml
@@ -109,7 +109,7 @@ struct
let compare_split (i1,_m1) (i2,_m2) =
Integer.compare i1 i2
in
- Extlib.opt_compare IntPair.compare k1.ration_stamp k2.ration_stamp
+ Option.compare IntPair.compare k1.ration_stamp k2.ration_stamp
<?> (LoopList.compare, k1.loops, k2.loops)
<?> (ExpMap.compare compare_split, k1.static_split, k2.static_split)
<?> (ExpMap.compare compare_split, k1.dynamic_split, k2.dynamic_split)
diff --git a/src/plugins/wp/CfgCompiler.ml b/src/plugins/wp/CfgCompiler.ml
index 1f2ac5926e4856407771f511f887f60966e53947..5c445134f3cd8ab06163481f63a13d3397ad68d2 100644
--- a/src/plugins/wp/CfgCompiler.ml
+++ b/src/plugins/wp/CfgCompiler.ml
@@ -814,7 +814,7 @@ struct
| Branch (c,n1,n2) ->
let n1' = Option.map find n1 in
let n2' = Option.map find n2 in
- if Extlib.opt_equal Node.equal n1 n1' && Extlib.opt_equal Node.equal n2 n2'
+ if Option.equal Node.equal n1 n1' && Option.equal Node.equal n2 n2'
then Some e
else Some (Branch(c,n1',n2'))
| Either l ->