From cb17c58ba2a5b55e4a275ab846897a00dd10a835 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 21 Jan 2021 16:00:29 +0100
Subject: [PATCH] replace missed occurrences of Extlib functions with Option
---
doc/developer/advance.tex | 1 -
doc/developer/examples/syntactic_check.ml | 2 +-
doc/training/developer/annotations.tex | 4 ++--
doc/training/developer/project.tex | 2 +-
src/kernel_internals/typing/cabs2cil.ml | 2 +-
tests/crowbar/complete_type.ml | 2 +-
tests/misc/add_assigns.ml | 2 +-
tests/misc/exception.ml | 2 +-
tests/misc/find_enclosing_loop.ml | 2 +-
tests/misc/my_visitor.ml | 2 +-
tests/misc/static.ml | 4 ++--
tests/misc/vis_spec.ml | 2 +-
tests/spec/location_char.ml | 2 +-
tests/spec/logic_functions_sets.ml | 2 +-
tests/spec/property_test.ml | 4 ++--
tests/syntax/copy_visitor_bts_1073.ml | 2 +-
tests/syntax/transient_block.ml | 6 +++---
tests/syntax/visit_create_local.ml | 2 +-
18 files changed, 22 insertions(+), 23 deletions(-)
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index a516c832f44..4ebbdafe883 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 74c141bde19..f99b0921fc0 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 e2ae5aab305..7d412db1a02 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 715f8361c58..98e08c503c0 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 bd263dc584e..703a2ea9f3b 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 5a6a8f18c90..3cae6790456 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 42afdad88cf..3b1412f0f1c 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 83d0a204e5e..b0578283982 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 382ab2abc0f..cc510ae91eb 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 09545f270ae..4afb3e92f08 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 9a5a73fdf89..7b6f77aa5f8 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 720539a727b..ec8a33e2c84 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 981839b0ba8..335700d2f51 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 68aead8c98f..f4b2847fec3 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 443e8cefd62..9be9b8114be 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 a8bf07b17d6..d057ae1f832 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 0938b72d746..79a9fc9d245 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 a81f0c35900..1ae5cabb9a4 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
--
GitLab