diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index a516c832f44173842b923ef402ec00659e1a440e..4ebbdafe88313a0e6b675b4f7b5735295569c2fb 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -3900,7 +3900,6 @@ division in the program, stating that the divisor is not zero:
\sscodeidx{Cil\_types}{binop}{Mod}
\scodeidx{Logic\_utils}{expr\_to\_term}
\scodeidx{Logic\_const}{prel}
-\scodeidx{Extlib}{the}
\sscodeidx{Cil}{cilVisitor}{get\_filling\_actions}
\sscodeidx{Cil}{visitAction}{DoChildren}
\scodeidx{File}{create\_project\_from\_visitor}
diff --git a/doc/developer/examples/syntactic_check.ml b/doc/developer/examples/syntactic_check.ml
index 74c141bde198eb34d54e978d903d87f3237b3746..f99b0921fc07f060eabba009751658119adab29b 100644
--- a/doc/developer/examples/syntactic_check.ml
+++ b/doc/developer/examples/syntactic_check.ml
@@ -43,7 +43,7 @@ class non_zero_divisor prj = object (self)
| Kglobal -> assert false
| Kstmt s -> s
in
- let kf = Extlib.the self#current_kf in
+ let kf = Option.get self#current_kf in
(* The above statement and function are related to the original project. We
need to attach the new assertion to the corresponding statement and
function of the new project. Cil provides functions to convert a
diff --git a/doc/training/developer/annotations.tex b/doc/training/developer/annotations.tex
index e2ae5aab3057b692d43978d7e18b249a3d23671b..7d412db1a0226c684eac5fbc45ad8e933eafa6b8 100644
--- a/doc/training/developer/annotations.tex
+++ b/doc/training/developer/annotations.tex
@@ -95,8 +95,8 @@ let _ = object
method vcode_annot =
let ppts =
Property.ip_of_code_annot
- (Extlib.the self#current_kf)
- (Extlib.the self#current_stmt)
+ (Option.get self#current_kf)
+ (Option.get self#current_stmt)
in
Pretty_utils.pp_list "%a"
Property.pretty ppts;
diff --git a/doc/training/developer/project.tex b/doc/training/developer/project.tex
index 715f8361c58345aa08b289ac2e78aec428389735..98e08c503c07304da355bff6274bb29fbcde8398 100644
--- a/doc/training/developer/project.tex
+++ b/doc/training/developer/project.tex
@@ -146,7 +146,7 @@ let _ = object (self)
_args,
_loc) ->
My_callstack.set
- ((Extlib.the self#current_stmt,
+ ((Option.get self#current_stmt,
Globals.Functions.get v)
:: (My_callstack.get ()));
Cil.SkipChildren
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index bd263dc584ee882bb09ce53af8699955c10eb333..703a2ea9f3b3548161133d0236d1928de8340b5d 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5554,7 +5554,7 @@ and makeCompType ghost (isstruct: bool)
(if comp.cstruct then "struct" else "union");
List.iter check flds;
if comp.cfields <> None then begin
- let old_fields = Extlib.the comp.cfields in
+ let old_fields = Option.get comp.cfields in
(* This appears to be a multiply defined structure. This can happen from
* a construct like "typedef struct foo { ... } A, B;". This is dangerous
* because at the time B is processed some forward references in { ... }
diff --git a/tests/crowbar/complete_type.ml b/tests/crowbar/complete_type.ml
index 5a6a8f18c9088b3c46c7c7d530821e40e0a2ee18..3cae6790456519071aa9351c84a579e9a6c67317 100644
--- a/tests/crowbar/complete_type.ml
+++ b/tests/crowbar/complete_type.ml
@@ -42,7 +42,7 @@ let mk_array_type (is_gcc, typ, types, kind) length =
| Complete, Some _ -> Complete
in
let length =
- Extlib.opt_map (Cil.kinteger ~loc Cil.(theMachine.kindOfSizeOf)) length
+ Option.map (Cil.kinteger ~loc Cil.(theMachine.kindOfSizeOf)) length
in
(is_gcc, TArray (typ, length, { scache = Not_Computed }, []), types, kind)
diff --git a/tests/misc/add_assigns.ml b/tests/misc/add_assigns.ml
index 42afdad88cf132574af23ec8b86df63525688d14..3b1412f0f1c2247bb67865aef6fbb01b48bdb825 100644
--- a/tests/misc/add_assigns.ml
+++ b/tests/misc/add_assigns.ml
@@ -26,7 +26,7 @@ let main () =
(fun b -> b.b_name = Cil.default_behavior_name)
(Annotations.behaviors kf)
in
- let ip = Extlib.the (Property.ip_assigns_of_behavior kf Kglobal [] bhv) in
+ let ip = Option.get (Property.ip_assigns_of_behavior kf Kglobal [] bhv) in
Property_status.(emit emitter ~hyps:[] ip True)
end
diff --git a/tests/misc/exception.ml b/tests/misc/exception.ml
index 83d0a204e5ece3883c436f054be6f6f4793e8871..b057828398230dd11276504b14b858067a38e390 100644
--- a/tests/misc/exception.ml
+++ b/tests/misc/exception.ml
@@ -125,7 +125,7 @@ let add_exn ast =
| GVar(v,_,_) when v.vname = "x" -> glob := Some v
| GFun(f,_) ->
change_body
- (Extlib.the !my_exn) (Extlib.the !my_exn2) (Extlib.the !glob) f
+ (Option.get !my_exn) (Option.get !my_exn2) (Option.get !glob) f
| _ -> ()
in
List.iter treat_glob ast.globals
diff --git a/tests/misc/find_enclosing_loop.ml b/tests/misc/find_enclosing_loop.ml
index 382ab2abc0fc9a2d6062fbd2ead967df1512592b..cc510ae91eb510e392f836f279022ba05f39aab0 100644
--- a/tests/misc/find_enclosing_loop.ml
+++ b/tests/misc/find_enclosing_loop.ml
@@ -17,7 +17,7 @@ object(self)
let has_loop =
try
Some
- (Kernel_function.find_enclosing_loop (Extlib.the self#current_kf) s)
+ (Kernel_function.find_enclosing_loop (Option.get self#current_kf) s)
with Not_found -> None
in
(match has_loop with
diff --git a/tests/misc/my_visitor.ml b/tests/misc/my_visitor.ml
index 09545f270ae554bcbfd5e1120ce60e7cc051fa12..4afb3e92f0862a5bc4e3b28f8b1023022a933cb6 100644
--- a/tests/misc/my_visitor.ml
+++ b/tests/misc/my_visitor.ml
@@ -55,7 +55,7 @@ class foo = object (self)
method! vstmt_aux stmt =
let loc = Cil.CurrentLoc.get () in
- add_assert loc (Extlib.the self#current_kf) stmt;
+ add_assert loc (Option.get self#current_kf) stmt;
DoChildren
method! vglob_aux _ = DoChildren
diff --git a/tests/misc/static.ml b/tests/misc/static.ml
index 9a5a73fdf89422ae513a2b0bb2bfdf2d929bb2f2..7b6f77aa5f8f1d7d362de123ec827c53e052bd70 100644
--- a/tests/misc/static.ml
+++ b/tests/misc/static.ml
@@ -3,7 +3,7 @@ open Cil_types
let find_x f =
let kf = Globals.Functions.find_by_name f in
let stmt = Kernel_function.find_return kf in
- Extlib.the (Globals.Syntactic_search.find_in_scope "x" (Block_scope stmt))
+ Option.get (Globals.Syntactic_search.find_in_scope "x" (Block_scope stmt))
let run () =
Ast.compute ();
@@ -11,7 +11,7 @@ let run () =
let x_g = find_x "g" in
let x_main = find_x "main" in
let x_glob =
- Extlib.the (Globals.Syntactic_search.find_in_scope "x" Program)
+ Option.get (Globals.Syntactic_search.find_in_scope "x" Program)
in
if not (Cil_datatype.Varinfo.equal x_main x_glob) then
Kernel.fatal "in main, global variable x should be in scope";
diff --git a/tests/misc/vis_spec.ml b/tests/misc/vis_spec.ml
index 720539a727bbbe9e03b4d4670ab6d2acbea6f531..ec8a33e2c84821e0734a0b22d7e61a51c96bd235 100644
--- a/tests/misc/vis_spec.ml
+++ b/tests/misc/vis_spec.ml
@@ -7,7 +7,7 @@ object(self)
method! vspec sp =
Format.printf "Considering spec of function %s@."
- (Kernel_function.get_name (Extlib.the self#current_kf));
+ (Kernel_function.get_name (Option.get self#current_kf));
(match self#current_func with
| Some f ->
if f.svar.vname ="f" then (
diff --git a/tests/spec/location_char.ml b/tests/spec/location_char.ml
index 981839b0ba83e12967bdd4dbfe54949bb2561409..335700d2f5108e080ce20cdfef723dc76ed0d324 100644
--- a/tests/spec/location_char.ml
+++ b/tests/spec/location_char.ml
@@ -9,7 +9,7 @@ class print_term = object(self)
inherit Visitor.frama_c_inplace
method private should_print =
- let n = Kernel_function.get_name (Extlib.the self#current_kf) in
+ let n = Kernel_function.get_name (Option.get self#current_kf) in
n = "f" || n = "main"
method! vterm v =
diff --git a/tests/spec/logic_functions_sets.ml b/tests/spec/logic_functions_sets.ml
index 68aead8c98f74e3723b06d2498ef78cd93af3f71..f4b2847fec3e10ff5d3b6fd673406b363e403ffd 100644
--- a/tests/spec/logic_functions_sets.ml
+++ b/tests/spec/logic_functions_sets.ml
@@ -2,7 +2,7 @@ open Cil_types
let check = function
| Dfun_or_pred (li, _) ->
- let decl_type = Extlib.the li.l_type in
+ let decl_type = Option.get li.l_type in
let body_type = match li.l_body with
| LBterm t -> t.term_type
| _ -> assert false
diff --git a/tests/spec/property_test.ml b/tests/spec/property_test.ml
index 443e8cefd62dc590c13935476210378f744f6037..9be9b8114bedc86a765e346bb25cafc41490f591 100644
--- a/tests/spec/property_test.ml
+++ b/tests/spec/property_test.ml
@@ -8,7 +8,7 @@ class visit prj =
object(self)
inherit Visitor.frama_c_copy prj
method! vbehavior b =
- let kf = Extlib.the self#current_kf in
+ let kf = Option.get self#current_kf in
if Kernel_function.get_name kf = "main" then begin
let x = Globals.Vars.find_from_astinfo "X" VGlobal in
let x = Cil.cvar_to_lvar x in
@@ -35,7 +35,7 @@ class visit prj =
method! vstmt_aux stmt =
match stmt.skind with
| Return _ ->
- let kf = Extlib.the self#current_kf in
+ let kf = Option.get self#current_kf in
let requires = [ Logic_const.new_predicate (Logic_const.ptrue) ] in
let post_cond =
[ Normal, Logic_const.new_predicate (Logic_const.pfalse) ]
diff --git a/tests/syntax/copy_visitor_bts_1073.ml b/tests/syntax/copy_visitor_bts_1073.ml
index a8bf07b17d614fc3f967f5aebdc594039b47403d..d057ae1f8327c8b9dc043b61cc4fe3feb1133837 100644
--- a/tests/syntax/copy_visitor_bts_1073.ml
+++ b/tests/syntax/copy_visitor_bts_1073.ml
@@ -7,7 +7,7 @@ object(self)
method! vglob_aux g =
match g with
| GFun (f,loc) ->
- let my_kf = Extlib.the self#current_kf in
+ let my_kf = Option.get self#current_kf in
let f1 = Visitor.visitFramacFunction (self:>Visitor.frama_c_visitor) f
in
let v2 = Cil.copyVarinfo f.svar (f.svar.vname ^ "1") in
diff --git a/tests/syntax/transient_block.ml b/tests/syntax/transient_block.ml
index 0938b72d74627597f86fd7fe7c6070c363e36bac..79a9fc9d24574aa3c8154e3e0e57aeda1f7360d4 100644
--- a/tests/syntax/transient_block.ml
+++ b/tests/syntax/transient_block.ml
@@ -10,7 +10,7 @@ class vis prj = object(self)
let b = Cil.mkBlock [s1] in
if create then begin
let f = Visitor_behavior.Get.fundec
- self#behavior (Extlib.the self#current_func) in
+ self#behavior (Option.get self#current_func) in
let y = Cil.makeLocalVar f ~scope:b "y" (TInt(IInt,[])) in
my_var <- Some y;
let loc = Cil_datatype.Location.unknown in
@@ -33,8 +33,8 @@ class vis prj = object(self)
Kernel.feedback "transient_block fatal error on %a as expected"
Printer.pp_instr instr;
let f = Visitor_behavior.Get.fundec
- self#behavior (Extlib.the self#current_func) in
- let y = Extlib.the my_var in
+ self#behavior (Option.get self#current_func) in
+ let y = Option.get my_var in
f.slocals <-
List.filter
(fun v -> not (Cil_datatype.Varinfo.equal v y)) f.slocals;
diff --git a/tests/syntax/visit_create_local.ml b/tests/syntax/visit_create_local.ml
index a81f0c35900d00dfec7bdf027d7b349a22ccbfab..1ae5cabb9a4890af488d4f583f8d4f40639b4dbf 100644
--- a/tests/syntax/visit_create_local.ml
+++ b/tests/syntax/visit_create_local.ml
@@ -4,7 +4,7 @@ open Cil
class cF = object(self) inherit Visitor.frama_c_inplace
method! vstmt s =
-let fd = (Extlib.the self#current_func) in
+let fd = (Option.get self#current_func) in
match s.skind with
| Instr (Set (lv,e,loc)) ->
let vi = makeLocalVar fd "varbidon" (typeOf e) in