diff --git a/bin/migration_scripts/titanium2vanadium.sh b/bin/migration_scripts/titanium2vanadium.sh
index 37d8f329351c81aa94acaccda53d2edc87f9be62..55b1d33d5443b3e264d88da1c095933fc7e49c8a 100755
--- a/bin/migration_scripts/titanium2vanadium.sh
+++ b/bin/migration_scripts/titanium2vanadium.sh
@@ -100,7 +100,10 @@ process_file ()
-e 's/Extlib\.may_map /Option.fold ~some:/g' \
-e 's/~dft:/~none:/g' \
-e 's/Extlib\.may /Option.iter /g' \
- -e 's/Extlib\.opt_map/Option.map/g'
+ -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'
}
apply_one_dir ()
diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml
index c551601327ab35cb037eccf50ef168e2f1413662..a841b52040557d15f88774c4f07f1a99193a75d9 100644
--- a/src/kernel_internals/typing/asm_contracts.ml
+++ b/src/kernel_internals/typing/asm_contracts.ml
@@ -104,7 +104,7 @@ let extract_mem_term ~loc acc tlv =
match Logic_utils.unroll_type (Cil.typeOfTermLval tlv) with
| Ctype (TPtr _ ) -> access_ptr_elts ~loc tlv :: acc
| Ctype (TArray(_,e,_,_)) ->
- let size = Extlib.opt_bind (Cil.constFoldToInt ~machdep:true) e in
+ let size = Option.bind e (Cil.constFoldToInt ~machdep:true) in
access_elts ~loc ?size tlv :: acc
| _ -> acc
@@ -116,8 +116,8 @@ class visit_assembly =
inherit Visitor.frama_c_inplace
method! vinst i =
- let stmt = Extlib.the self#current_stmt in
- let kf = Extlib.the self#current_kf in
+ let stmt = Option.get self#current_stmt in
+ let kf = Option.get self#current_kf in
match i with
| Asm(_, _, Some { asm_outputs; asm_inputs; asm_clobbers }, loc) ->
let lv_out, lv_from = find_out_lval asm_outputs in
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 294370c2ee1627a9126eb1e6626046c8056f3402..727739689d1c62ef91ffab7e51bf0d75ed78cd04 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -3719,7 +3719,7 @@ let fieldsToInit
in
let found, r = add_comp NoOffset comp (designator = None, []) in
begin if not found then
- let fn = Extlib.the designator in
+ let fn = Option.get designator in
Kernel.fatal ~current:true "Cannot find designated field %s" fn;
end;
List.rev r
@@ -4247,11 +4247,11 @@ let append_chunk_to_annot ~ghost annot_chunk current_chunk =
match current_chunk.stmts with
| [(s1, m1, w1, r1, c1); (s2, m2, w2, r2, c2)] ->
Extlib.swap
- Extlib.opt_bind
- (collapseCallCast (s2,s1)) (* the chunk list is reversed.*)
+ Option.bind
(function
| [ s1' ] -> Some (s1', m1 @ m2, w1 @ w2, r1 @ r2, c1 @ c2)
| _ -> None (* should not happen. *))
+ (collapseCallCast (s2,s1)) (* the chunk list is reversed.*)
| _ -> None
in
match res with
@@ -8114,7 +8114,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
(* ISO 6.7.8 para 14: final NUL added only if no size specified, or
* if there is room for it; btw, we can't rely on zero-init of
* globals, since this array might be a local variable *)
- if ((not (Extlib.has_some leno)) ||
+ if ((not (Option.is_some leno)) ||
((String.length s) < (integerArrayLength leno)))
then ref [init Int64.zero]
else ref []
@@ -8192,7 +8192,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
(* ISO 6.7.8 para 14: final NUL added only if no size specified, or
* if there is room for it; btw, we can't rely on zero-init of
* globals, since this array might be a local variable *)
- if (not (Extlib.has_some leno)
+ if (not (Option.is_some leno)
|| ((List.length s) < (integerArrayLength leno)))
then [init Int64.zero]
else [])
@@ -8527,7 +8527,7 @@ and createGlobal ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool * A
if inite != A.NO_INIT then
Kernel.error ~once:true ~current:true
"Function declaration with initializer (%s)\n" vi.vname;
- end else if Extlib.has_some logic_spec then begin
+ end else if Option.is_some logic_spec then begin
Kernel.warning ~wkey:Kernel.wkey_annot_error ~current:true ~once:true
"Global variable %s is not a function. It cannot have a contract."
vi.vname
@@ -8717,7 +8717,7 @@ and cleanup_autoreference vi chunk =
method! vinst = function
| Call _ | Local_init(_,ConsInit _,_) ->
- calls := ref (Extlib.the self#current_stmt) :: !calls;
+ calls := ref (Option.get self#current_stmt) :: !calls;
DoChildren
| _ -> DoChildren
diff --git a/src/kernel_internals/typing/ghost_accesses.ml b/src/kernel_internals/typing/ghost_accesses.ml
index 6af1cadc349d690ab660527690bcc8720024b2ca..ae1eceffe9607d029a978c3ef746b07439497f68 100644
--- a/src/kernel_internals/typing/ghost_accesses.ml
+++ b/src/kernel_internals/typing/ghost_accesses.ml
@@ -226,7 +226,7 @@ class visitor = object(self)
if not (ghost_term_type term.term_type) then
Error.assigns_non_ghost_term ~current:true term
in
- let kf = Extlib.the (self#current_kf) in
+ let kf = Option.get (self#current_kf) in
match assigns with
| Writes froms -> List.iter check_assign froms
| WritesAny when not (Kernel_function.has_definition kf) ->
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index a250b523522dbcbd9595128b8555f2da8981ec7d..38c943c79336126cae4616988e18ea68fd9abb85 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -892,12 +892,12 @@ let rec global_annot_pass1 g = match g with
annotation at loc %a. Ignoring new binding."
Cil_printer.pp_identified_term t
pretty_volatile_kind k
- Cil_printer.pp_location (fst (Extlib.the node.nloc))
+ Cil_printer.pp_location (fst (Option.get node.nloc))
in
List.iter
(fun x ->
- if Extlib.has_some rvi then process_term_kind (x,R);
- if Extlib.has_some wvi then process_term_kind (x,W))
+ if Option.is_some rvi then process_term_kind (x,R);
+ if Option.is_some wvi then process_term_kind (x,W))
hs
| Daxiomatic(id,decls,_,l) ->
CurrentLoc.set l;
@@ -1941,7 +1941,7 @@ class renameVisitorClass =
if lv == lv' then DoChildren (* Replacement already done... *)
else ChangeTo lv')
| LVC ->
- let vi = Extlib.the lv.lv_origin in
+ let vi = Option.get lv.lv_origin in
if not vi.vglob then DoChildren
else begin
match PlainMerging.findReplacement true vEq !currentFidx vi.vname
@@ -2387,7 +2387,7 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
| Dvolatile(vi,rd,wr,attr,loc) ->
let is_representative id =
not
- (Extlib.has_some
+ (Option.is_some
(VolatileMerging.findReplacement true lvEq !currentFidx id))
in
let push_volatile l rd wr =
@@ -2415,8 +2415,8 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
annotation can be used as is (i.e. does not overlap with a
preceding annotation.
*)
- let reads = not (Extlib.has_some rd) || is_representative (v,R) in
- let writes = not (Extlib.has_some wr) || is_representative (v,W) in
+ let reads = not (Option.is_some rd) || is_representative (v,R) in
+ let writes = not (Option.is_some wr) || is_representative (v,W) in
if reads then
if writes then
no_drop, v::full_representative, only_reads, only_writes
@@ -2433,8 +2433,8 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
if no_drop then mergePushGlobals (visitCilGlobal renameVisitor g)
else begin
push_volatile full_representative rd wr;
- if Extlib.has_some rd then push_volatile only_reads rd None;
- if Extlib.has_some wr then push_volatile only_writes None wr
+ if Option.is_some rd then push_volatile only_reads rd None;
+ if Option.is_some wr then push_volatile only_writes None wr
end
| Daxiomatic(n,l,_,loc) ->
begin
@@ -2964,7 +2964,7 @@ let oneFilePass2 (f: file) =
(* Restore the formals from the old definition. We always have
Some l from getFormalsDecl
in case of a defined function. *)
- Cil.setFormals fdec (Extlib.the defn_formals);
+ Cil.setFormals fdec (Option.get defn_formals);
(* previous was found *)
if (curSum = prevSum) then
Kernel.warning ~current:true
diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unroll_loops.ml
index 95f70fdfa069f86b24590edfee7e5dadf9b8d834..2ef5c657b18fb1ffc3bd7c32eac702fd0482aa17 100644
--- a/src/kernel_internals/typing/unroll_loops.ml
+++ b/src/kernel_internals/typing/unroll_loops.ml
@@ -39,7 +39,7 @@ let empty_info =
let update_info global_find_init emitter info spec =
match spec with
| {term_type=typ} when Logic_typing.is_integral_type typ ->
- if Extlib.has_some info.unroll_number && not info.ignore_unroll then begin
+ if Option.is_some info.unroll_number && not info.ignore_unroll then begin
Kernel.warning ~once:true ~current:true
"ignoring unrolling directive (directive already defined)";
info
@@ -65,7 +65,7 @@ let update_info global_find_init emitter info spec =
end
| {term_node=TConst (LStr "done") } -> { info with ignore_unroll = true }
| {term_node=TConst (LStr "completely") } ->
- if Extlib.has_some info.total_unroll then begin
+ if Option.is_some info.total_unroll then begin
Kernel.warning ~once:true ~current:true
"found two total unroll pragmas";
info
@@ -187,7 +187,7 @@ let copy_annotations kf assoc labelled_stmt_tbl (break_continue_must_change, stm
begin
try
let vi'= snd (List.find (fun (x,_) -> x.vid = vi.vid) assoc) in
- ChangeTo (Extlib.the vi'.vlogic_var_assoc)
+ ChangeTo (Option.get vi'.vlogic_var_assoc)
with Not_found -> SkipChildren
| Invalid_argument _ ->
Kernel.abort
@@ -610,7 +610,7 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self)
let f sloop =
Kernel.debug ~dkey
"Unrolling loop stmt %d (%d times) inside function %a@."
- sloop.sid number Kernel_function.pretty (Extlib.the self#current_kf);
+ sloop.sid number Kernel_function.pretty (Option.get self#current_kf);
file_has_unrolled_loop <- true ;
has_unrolled_loop <- true ;
match sloop.skind with
@@ -644,14 +644,14 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self)
let switch_label_action = if i = number-1 then Move else Ignore in
let new_block, new_switch_cases =
copy_block
- (Extlib.the self#current_kf)
+ (Option.get self#current_kf)
switch_label_action
((Some break_lbl_stmt),(Some !current_continue))
block
in
cases <- new_switch_cases @ cases;
current_continue := mk_continue ();
- update_loop_current (Extlib.the self#current_kf) !current_continue new_block;
+ update_loop_current (Option.get self#current_kf) !current_continue new_block;
(match new_block.blocals with
[] -> new_stmts:= new_block.bstmts @ !new_stmts;
| _ -> (* keep the block in order to preserve locals decl *)
@@ -660,7 +660,7 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self)
let new_stmt = match !new_stmts with
| [ s ] -> s
| l ->
- List.iter (update_loop_entry (Extlib.the self#current_kf) !current_continue) l;
+ List.iter (update_loop_entry (Option.get self#current_kf) !current_continue) l;
let l = if is_referenced !current_continue l then !current_continue :: l else l in
let new_stmts = l @ [break_lbl_stmt] in
let new_block = mkBlock new_stmts in
@@ -687,7 +687,7 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self)
(AInvariant ([],true,Logic_const.(toplevel_predicate pfalse)))
in
Annotations.add_code_annot
- emitter ~kf:(Extlib.the self#current_kf) sloop annot;
+ emitter ~kf:(Option.get self#current_kf) sloop annot;
new_stmts
in
let h sloop new_stmts = (* To indicate that the unrolling has been done *)
@@ -699,7 +699,7 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self)
Logic_const.new_code_annotation (APragma (Loop_pragma specs))
in
Annotations.add_code_annot
- Emitter.end_user ~kf:(Extlib.the self#current_kf) sloop annot;
+ Emitter.end_user ~kf:(Option.get self#current_kf) sloop annot;
new_stmts
in
let fgh sloop = h sloop (g sloop (f sloop)) in
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index a0086d83efdca7ccc94c05824d0a10f8d9fb166f..840592615b1dde78505a3caeda6cb92e066b1d79 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -837,8 +837,8 @@ type overflow_float_to_int =
let cast_float_to_int_non_nan ~signed ~size (min, max) =
let all = create_all_values ~size ~signed in
- let min_all = Extlib.the (min_int all) in
- let max_all = Extlib.the (max_int all) in
+ let min_all = Option.get (min_int all) in
+ let max_all = Option.get (max_int all) in
let conv f =
try
(* truncate_to_integer returns an integer that fits in a 64 bits
diff --git a/src/kernel_services/abstract_interp/tr_offset.ml b/src/kernel_services/abstract_interp/tr_offset.ml
index 36376d3393e27214ed22b83b70e079d0855aab9b..f923d0914630844a230b41835bfb09ef3409bfb9 100644
--- a/src/kernel_services/abstract_interp/tr_offset.ml
+++ b/src/kernel_services/abstract_interp/tr_offset.ml
@@ -52,7 +52,7 @@ let reduce_offset_by_validity origin ival size validity =
| None ->
let min, max, _r, modu = Ival.min_max_r_mod reduced_ival in
(* The bounds are finite thanks to the narrow with the valid range. *)
- let min = Extlib.the min and max = Extlib.the max in
+ let min = Option.get min and max = Option.get max in
if Int.lt modu size
then Overlap (min, Int.add max (Int.pred size), origin)
else Interval (min, max, modu)
diff --git a/src/kernel_services/analysis/destructors.ml b/src/kernel_services/analysis/destructors.ml
index 24a664faad73c180f9e2b37ad3dc4e7597e41629..99e2cef1c2ea23922820e87c639dfb55749c480d 100644
--- a/src/kernel_services/analysis/destructors.ml
+++ b/src/kernel_services/analysis/destructors.ml
@@ -244,7 +244,7 @@ class vis flag = object(self)
Kernel.fatal ~current:true
"%a in function %a is expected to have a single successor"
Printer.pp_stmt s
- Kernel_function.pretty (Extlib.the self#current_kf)
+ Kernel_function.pretty (Option.get self#current_kf)
in
let treat_succ_open kind s succ =
(* The jump must not bypass a vla initialization in the opened blocks. *)
diff --git a/src/kernel_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml
index 77f22868e99db3bb1db048e1eea22873889e7c0e..6c1568a7051e44207129266ad9a6e9560c1531dc 100644
--- a/src/kernel_services/analysis/exn_flow.ml
+++ b/src/kernel_services/analysis/exn_flow.ml
@@ -457,10 +457,10 @@ class erase_exn =
List.find (fun fi -> fi.fname = name) (Option.(get (get exn_struct).cfields))
method private exn_field name =
- Var (Extlib.the exn_var), Field(self#exn_field_off name, NoOffset)
+ Var (Option.get exn_var), Field(self#exn_field_off name, NoOffset)
method private exn_field_term name =
- TVar(Cil.cvar_to_lvar (Extlib.the exn_var)),
+ TVar(Cil.cvar_to_lvar (Option.get exn_var)),
TField(self#exn_field_off name, TNoOffset)
method private exn_obj_field = self#exn_field exn_obj_name
@@ -516,7 +516,7 @@ class erase_exn =
if Stack.is_empty catch_all_label then begin
(* no catch-all clause in the function: just go up in the stack. *)
fct_can_throw <- true;
- let kf = Extlib.the self#current_kf in
+ let kf = Option.get self#current_kf in
let ret = Kernel_function.find_return kf in
let rtyp = Kernel_function.get_return_type kf in
if ret.labels = [] then
@@ -594,7 +594,7 @@ class erase_exn =
in
b.bstmts <- s :: b.bstmts
in
- let f = Extlib.the self#current_func in
+ let f = Option.get self#current_func in
let update_locals v b =
if not (List.memq v b.blocals) then b.blocals <- v::b.blocals;
if not (List.memq v f.slocals) then f.slocals <- v::f.slocals
@@ -638,7 +638,7 @@ class erase_exn =
method private modify_current () =
modified_funcs <-
- Cil_datatype.Fundec.Set.add (Extlib.the self#current_func) modified_funcs;
+ Cil_datatype.Fundec.Set.add (Option.get self#current_func) modified_funcs;
method private aux_handler_goto target (v,b) =
let loc = v.vdecl in
@@ -696,7 +696,7 @@ class erase_exn =
method private clean_catch_clause (bind,b as handler) acc =
let remove_local v =
let f =
- Visitor_behavior.Get.fundec self#behavior (Extlib.the self#current_func)
+ Visitor_behavior.Get.fundec self#behavior (Option.get self#current_func)
in
let v = Visitor_behavior.Get.varinfo self#behavior v in
f.slocals <- List.filter (fun v' -> v!=v') f.slocals;
@@ -776,7 +776,7 @@ class erase_exn =
| Throw (None,loc) ->
self#modify_current ();
let s1 = self#set_uncaught_flag loc true in
- let t = purify (Extlib.the exn_var).vtype in
+ let t = purify (Option.get exn_var).vtype in
let rv = self#jumps_to_handler loc t in
let b = mkBlock (s1 :: rv) in
s.skind <- Block b;
diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index e6481385d818b53f624ccf8af72e5d293ab57f99..c9aaadb66a7c12712cfd657b9fdc7e0d2fdc2433 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -385,11 +385,11 @@ let build_automaton ~annotations kf =
control.src
| Break _ ->
- add_jump control.src (Extlib.the control.break) stmt;
+ add_jump control.src (Option.get control.break) stmt;
control.src
| Continue _ ->
- add_jump control.src (Extlib.the control.continue) stmt;
+ add_jump control.src (Option.get control.continue) stmt;
control.src
| If (exp, then_block, else_block, _) ->
@@ -741,7 +741,7 @@ module MakeDot
| `Vertex -> htmllabel "%a" V.pretty v
in
let vertex_attributes =
- if head && Extlib.has_some subgraph
+ if head && Option.is_some subgraph
then [`Shape `Invtriangle ; label]
else [label]
in
diff --git a/src/kernel_services/analysis/logic_interp.ml b/src/kernel_services/analysis/logic_interp.ml
index 28216959c2aa85e137fa6f0d7bfb33f5881c9965..06a027ae6107987adb4143b0eb3879b2c455fbde 100644
--- a/src/kernel_services/analysis/logic_interp.ml
+++ b/src/kernel_services/analysis/logic_interp.ml
@@ -154,9 +154,9 @@ let code_annot kf stmt s =
end) in
let loc = Stmt.loc stmt in
let pa =
- Extlib.opt_bind
- (function (_, Logic_ptree.Acode_annot (_,a)) -> Some a | _ -> None)
+ Option.bind
(Logic_lexer.annot (fst loc,s))
+ (function (_, Logic_ptree.Acode_annot (_,a)) -> Some a | _ -> None)
in
let parse pa =
LT.code_annot
@@ -954,13 +954,13 @@ to function contracts."
(* WARNING this is obsolete *)
(* [JS 2010/09/02] TODO: so what is the right way to do? *)
(* to preserve the interpretation of the loop invariant *)
- get_zone_from_pred (Extlib.the loop_body_opt) pred.tp_statement;
+ get_zone_from_pred (Option.get loop_body_opt) pred.tp_statement;
| AInvariant (_behav,false,pred) -> (* code invariant *)
(* to preserve the interpretation of the code invariant *)
get_zone_from_pred ki pred.tp_statement;
| AVariant (term,_) ->
(* to preserve the interpretation of the variant *)
- get_zone_from_term (Extlib.the loop_body_opt) term;
+ get_zone_from_term (Option.get loop_body_opt) term;
| APragma (Loop_pragma (Unroll_specs terms))
| APragma (Loop_pragma (Widen_hints terms))
| APragma (Loop_pragma (Widen_variables terms)) ->
@@ -973,14 +973,14 @@ to function contracts."
| AAllocation (_,FreeAllocAny) -> ();
| AAllocation (_,FreeAlloc(f,a)) ->
let get_zone x =
- get_zone_from_term (Extlib.the loop_body_opt) x.it_content
+ get_zone_from_term (Option.get loop_body_opt) x.it_content
in
List.iter get_zone f ;
List.iter get_zone a
| AAssigns (_, WritesAny) -> ()
| AAssigns (_, Writes l) -> (* loop assigns *)
let get_zone x =
- get_zone_from_term (Extlib.the loop_body_opt) x.it_content
+ get_zone_from_term (Option.get loop_body_opt) x.it_content
in
List.iter
(fun (zone,deps) ->
diff --git a/src/kernel_services/analysis/loop.ml b/src/kernel_services/analysis/loop.ml
index 3a8e04081f1e843edfff5c336ce93c001b3e1a67..491d5cd0aea81b52b9e55f3ab3080de1043fc36a 100644
--- a/src/kernel_services/analysis/loop.ml
+++ b/src/kernel_services/analysis/loop.ml
@@ -109,7 +109,7 @@ let get_non_naturals kf =
if Stmt.Hashtbl.mem visited s then begin
(* pred always contains something except when entering the recursion,
when visited is empty. *)
- let pred = Extlib.the pred in
+ let pred = Option.get pred in
if Stmt.Hashtbl.mem current s && not (is_back_edge kf pred s) then begin
res := Stmt.Set.add s !res;
Kernel.warning ~once:true ~source:(fst (Cil_datatype.Stmt.loc s))
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index d6468bf0903daf55cade44927582937c54b22038..f647488d6c33c49f62bb40c46f80dc632d742d7b 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -1404,7 +1404,7 @@ let ip_from_of_behavior kf st ~active b =
| From _ ->
let a = Datatype.String.Set.of_list active in
let ip =
- Extlib.the (ip_of_from kf st (Id_contract (a,b)) (out, froms))
+ Option.get (ip_of_from kf st (Id_contract (a,b)) (out, froms))
in
ip :: acc
in
@@ -1424,7 +1424,7 @@ let ip_from_of_code_annot kf st ca = match ca.annot_content with
let treat_from acc (out, froms) = match froms with FromAny -> acc
| From _ ->
let ip =
- Extlib.the (ip_of_from kf st (Id_loop ca) (out, froms))
+ Option.get (ip_of_from kf st (Id_loop ca) (out, froms))
in
ip::acc
in
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index bd1fa410041bf8bac9a1852b9e87e0eefba3ec6a..3479c49f1de700aba627c3e58b669b296bab5c16 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -289,7 +289,7 @@ struct
match current_ca with
None ->
let active = Datatype.String.Set.of_list active_behaviors in
- Property.Id_contract (active ,Extlib.the self#current_behavior)
+ Property.Id_contract (active ,Option.get self#current_behavior)
| Some ca -> Property.Id_loop ca
(* When [stmt] is a call, this method "inlines" the preconditions of the
@@ -345,7 +345,7 @@ struct
if Tag.unfold current
then self#preconditions_at_call fmt current;
Format.fprintf fmt "@{<%s>%a@}"
- (Tag.create (PStmt (Extlib.the self#current_kf,current)))
+ (Tag.create (PStmt (Option.get self#current_kf,current)))
(super#next_stmt next) current
method! lval fmt lv =
@@ -418,8 +418,8 @@ struct
| AAssert _ | AInvariant _ | APragma _ | AVariant _ ->
let ip =
Property.ip_of_code_annot_single
- (Extlib.the self#current_kf)
- (Extlib.the self#current_stmt)
+ (Option.get self#current_kf)
+ (Option.get self#current_stmt)
ca
in
Format.fprintf fmt "@{<%s>%a@}"
@@ -463,10 +463,10 @@ struct
super#requires p;
method! requires fmt p =
- let b = Extlib.the self#current_behavior in
+ let b = Option.get self#current_behavior in
let ip =
Property.ip_of_requires
- (Extlib.the self#current_kf) self#current_kinstr b p
+ (Option.get self#current_kf) self#current_kinstr b p
in
self#requires_aux fmt (ip, p)
@@ -474,7 +474,7 @@ struct
Format.fprintf fmt "@{<%s>%a@}"
(self#tag_property
(Property.ip_of_behavior
- (Extlib.the self#current_kf)
+ (Option.get self#current_kf)
self#current_kinstr
active_behaviors b))
super#behavior b
@@ -483,21 +483,21 @@ struct
Format.fprintf fmt "@{<%s>%a@}"
(self#tag_property
(Property.ip_of_decreases
- (Extlib.the self#current_kf) self#current_kinstr t))
+ (Option.get self#current_kf) self#current_kinstr t))
super#decreases t;
method! terminates fmt t =
Format.fprintf fmt "@{<%s>%a@}"
(self#tag_property
(Property.ip_of_terminates
- (Extlib.the self#current_kf) self#current_kinstr t))
+ (Option.get self#current_kf) self#current_kinstr t))
super#terminates t;
method! complete_behaviors fmt t =
Format.fprintf fmt "@{<%s>%a@}"
(self#tag_property
(Property.ip_of_complete
- (Extlib.the self#current_kf)
+ (Option.get self#current_kf)
self#current_kinstr
active_behaviors
t))
@@ -507,31 +507,31 @@ struct
Format.fprintf fmt "@{<%s>%a@}"
(self#tag_property
(Property.ip_of_disjoint
- (Extlib.the self#current_kf)
+ (Option.get self#current_kf)
self#current_kinstr
active_behaviors
t))
super#disjoint_behaviors t
method! assumes fmt p =
- let b = Extlib.the self#current_behavior in
+ let b = Option.get self#current_behavior in
Format.fprintf fmt "@{<%s>%a@}"
(self#tag_property
(Property.ip_of_assumes
- (Extlib.the self#current_kf) self#current_kinstr b p))
+ (Option.get self#current_kf) self#current_kinstr b p))
super#assumes p;
method! post_cond fmt pc =
- let b = Extlib.the self#current_behavior in
+ let b = Option.get self#current_behavior in
Format.fprintf fmt "@{<%s>%a@}"
(self#tag_property
(Property.ip_of_ensures
- (Extlib.the self#current_kf) self#current_kinstr b pc))
+ (Option.get self#current_kf) self#current_kinstr b pc))
super#post_cond pc;
method! assigns s fmt a =
match
- Property.ip_of_assigns (Extlib.the self#current_kf) self#current_kinstr
+ Property.ip_of_assigns (Option.get self#current_kf) self#current_kinstr
self#current_behavior_or_loop a
with
None -> super#assigns s fmt a
@@ -546,7 +546,7 @@ struct
let ip =
Extlib.the
(Property.ip_of_from
- (Extlib.the self#current_kf) self#current_kinstr
+ (Option.get self#current_kf) self#current_kinstr
self#current_behavior_or_loop from)
in
Format.fprintf fmt "@{<%s>%a@}"
@@ -561,7 +561,7 @@ struct
method! allocation ~isloop fmt a =
match
- Property.ip_of_allocation (Extlib.the self#current_kf) self#current_kinstr
+ Property.ip_of_allocation (Option.get self#current_kf) self#current_kinstr
self#current_behavior_or_loop a
with
None -> super#allocation ~isloop fmt a
@@ -572,8 +572,8 @@ struct
method! stmtkind sattr next fmt sk =
(* Special tag denoting the start of the statement, WITHOUT any ACSL
assertion/statement contract, etc. *)
- let s = Extlib.the self#current_stmt in
- let f = Extlib.the self#current_kf in
+ let s = Option.get self#current_stmt in
+ let f = Option.get self#current_kf in
let tag = Tag.create (PStmtStart(f,s)) in
Format.fprintf fmt "@{<%s>%a@}" tag (super#stmtkind sattr next) sk
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index b5c9ae9c9bc75e2a668c9062539fe7569d7f1225..4342827a938e1b64fc3c85c07864b9cbf2191e3c 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -1735,7 +1735,7 @@ and visitCilLogicVarUse vis lv =
we target the current project, builtins are by definition already
tied to logic_infos and should not be copied.
*)
- not (Project.is_current (Extlib.the vis#project)) &&
+ not (Project.is_current (Option.get vis#project)) &&
Logic_env.is_builtin_logic_function lv.lv_name
then begin
(* Do as if the variable has been declared.
@@ -4449,7 +4449,7 @@ and fieldBitsOffset (f : fieldinfo) : int * int =
(Option.value ~default:[] f.fcomp.cfields)
);
end;
- Extlib.the f.foffset_in_bits, Extlib.the f.fsize_in_bits
+ Option.get f.foffset_in_bits, Option.get f.fsize_in_bits
end
and bitsOffset (baset: typ) (off: offset) : int * int =
@@ -6056,7 +6056,7 @@ let foldLeftCompound
Works because [initl] is sorted by Cabs2cil.*)
let good_offset i off = match off with
| Index (i', NoOffset) ->
- Integer.(equal (Extlib.the (constFoldToInt i')) (of_int i))
+ Integer.(equal (Option.get (constFoldToInt i')) (of_int i))
| _ -> Kernel.fatal ~current:true
"Invalid initializer"
in
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index c09cbcdf03392984aea89aba2f3ec7e13ccef2d0..bf305b358d728b3abdf4148586ccb989287efb7c 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -537,7 +537,7 @@ let parse_cabs cpp_command_no_output = function
Datatype.Filepath.pretty f;
Frontc.parse f ()
| NeedCPP (f, cmdl, is_gnu_like) ->
- let cpp_command, ppf, supported_cpp_arch_args = Extlib.the cpp_command_no_output in
+ let cpp_command, ppf, supported_cpp_arch_args = Option.get cpp_command_no_output in
Kernel.feedback "Parsing %a (with preprocessing)"
Datatype.Filepath.pretty f;
if Sys.command cpp_command <> 0 then begin
@@ -1631,7 +1631,7 @@ let prepare_from_c_files () =
let init_project_from_visitor ?(reorder=false) prj
(vis:Visitor.frama_c_visitor) =
if not (Visitor_behavior.is_copy vis#behavior)
- || not (Project.equal prj (Extlib.the vis#project))
+ || not (Project.equal prj (Option.get vis#project))
then
Kernel.fatal
"Visitor does not copy or does not operate on correct project.";
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index 44f8bea56cbba1ece41fee93f16f9fe63dffb614..d3d0c5d68d33eaa27461efbbbb0f5261d8c1ea6d 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -246,7 +246,7 @@ module Base_checker = struct
self#push_behavior_stack ();
(* Initial AST does not have kf *)
if is_normalized then begin
- let kf = Extlib.the self#current_kf in
+ let kf = Option.get self#current_kf in
if not (Kernel_function.is_definition kf) then
check_abort
"Kernel function %a is supposed to be a prototype, but it has a body"
@@ -307,7 +307,7 @@ module Base_checker = struct
| Some _ -> (* can only happen in normalized mode. *)
check_abort
"Function %a does not have a return statement in its body"
- Kernel_function.pretty (Extlib.the self#current_kf));
+ Kernel_function.pretty (Option.get self#current_kf));
let check_one_stmt stmt _ =
let check_cfg_edge stmt' =
try
@@ -409,7 +409,7 @@ module Base_checker = struct
self#add_spec_behavior_names spec
| _ -> assert false (* filter should prevent anything else. *))
contracts;
- let kf = Extlib.the self#current_kf in
+ let kf = Option.get self#current_kf in
let s',kf' =
try
Kernel_function.find_from_sid s.sid
@@ -495,12 +495,12 @@ module Base_checker = struct
| None ->
check_abort
"Found a second return statement in body of function %a"
- Kernel_function.pretty (Extlib.the self#current_kf)
+ Kernel_function.pretty (Option.get self#current_kf)
| Some s' when s != s' ->
check_abort
"Function %a is supposed to have as return statement %d:@\n%a@\n\
Found in its body statement %d:@\n%a@\n"
- Kernel_function.pretty (Extlib.the self#current_kf)
+ Kernel_function.pretty (Option.get self#current_kf)
s'.sid Printer.pp_stmt s'
s.sid Printer.pp_stmt s
| Some _ -> return_stmt <- None
@@ -512,7 +512,7 @@ module Base_checker = struct
let prefix fmt =
Format.fprintf fmt "Local variable %a(%d) in function %a"
Printer.pp_varinfo v v.vid
- Printer.pp_varinfo (Extlib.the self#current_func).svar
+ Printer.pp_varinfo (Option.get self#current_func).svar
in
if v.vglob then check_abort "%t is marked as global" prefix;
if v.vformal then check_abort "%t is marked as formal" prefix;
@@ -529,7 +529,7 @@ module Base_checker = struct
Format.fprintf fmt
"Local variable %a(%d) in function %a"
Printer.pp_varinfo v v.vid
- Printer.pp_varinfo (Extlib.the self#current_func).svar
+ Printer.pp_varinfo (Option.get self#current_func).svar
in
if not v.vglob then
check_abort
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 99110d4f5caf86f9e070ee20ec6034281883dd03..9cc3ddbd61863c0bf1cc3354dbc8222987f1217d 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -327,7 +327,7 @@ module Lenv = struct
}
let string_of_current_label env =
- Extlib.opt_bind (
+ Option.bind env.current_logic_label (
function
| FormalLabel _ -> None
| BuiltinLabel Init -> Some "Init"
@@ -345,7 +345,6 @@ module Lenv = struct
| None -> None
| Some (Label (lab,_,_)) -> Some lab
| Some _ -> None))
- env.current_logic_label
let fresh_var env name kind typ =
let name =
@@ -1809,7 +1808,7 @@ struct
let conditional_conversion loc env rel t1 t2 =
- let is_rel = Extlib.has_some rel in
+ let is_rel = Option.is_some rel in
(* a comparison is mainly a function of type 'a -> 'a -> Bool/Prop.
performs the needed unifications on both sides.*)
let var = fresh_type_var "cmp" in
@@ -1843,7 +1842,7 @@ struct
else if isArithmeticType ty1 && isArithmeticType ty2 then begin
if is_same_type lty1 lty2 then begin
if is_rel then begin
- let rel = Extlib.the rel in
+ let rel = Option.get rel in
let kind =
match Cil.unrollType ty1 with
| TFloat (FFloat,_) -> "float"
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 1c6ad6e42edee54bc38398b71ff62daa79b08a36..04ac8d298cd8d688c4ec6d8a2c6f7ddc78a1a534 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -2578,8 +2578,8 @@ and bitsLogicOffset ltyp off : Integer.t * Integer.t =
(* Force the computation of the fields fsize_in_bits and
foffset_in_bits *)
ignore (Cil.bitsOffset typ (Field (f, NoOffset)));
- let size = Integer.of_int (Extlib.the f.fsize_in_bits) in
- let offset_f = Integer.of_int (Extlib.the f.foffset_in_bits) in
+ let size = Integer.of_int (Option.get f.fsize_in_bits) in
+ let offset_f = Integer.of_int (Option.get f.foffset_in_bits) in
loopOff f.ftype size (Integer.add start offset_f) off
end
else
@@ -2611,7 +2611,7 @@ let rec fold_itv f b e acc =
let find_init_by_index init i =
let same_offset (off, _) = match off with
| Index (i', NoOffset) ->
- Integer.equal i (Extlib.the (Cil.isInteger i'))
+ Integer.equal i (Option.get (Cil.isInteger i'))
| _ -> false
in
snd (List.find same_offset init)
diff --git a/src/kernel_services/ast_transformations/filter.ml b/src/kernel_services/ast_transformations/filter.ml
index 14923fcc954b7837aa9ca14b2b49c2bea758e121..15ed737f258de617c9d4fed302381f640325299d 100644
--- a/src/kernel_services/ast_transformations/filter.ml
+++ b/src/kernel_services/ast_transformations/filter.ml
@@ -354,7 +354,7 @@ end = struct
in ok
| _ -> false
- method private get_finfo () = Extlib.the fi
+ method private get_finfo () = Option.get fi
method private add_stmt_keep stmt =
keep_stmts <- Stmt.Set.add stmt keep_stmts
@@ -435,7 +435,7 @@ end = struct
Option.iter Cil.CurrentLoc.set (Cil_datatype.Code_annotation.loc v);
let stmt =
Visitor_behavior.Get_orig.stmt
- self#behavior (Extlib.the self#current_stmt)
+ self#behavior (Option.get self#current_stmt)
in
debug "[annotation] stmt %d : %a @."
stmt.sid Printer.pp_code_annotation v;
@@ -712,7 +712,7 @@ end = struct
Varinfo.Hashtbl.clear local_visible;
Varinfo.Hashtbl.add spec_table f.svar
(visitCilFunspec (self:>Cil.cilVisitor)
- (Annotations.funspec ~populate:false (Extlib.the self#current_kf)));
+ (Annotations.funspec ~populate:false (Option.get self#current_kf)));
SkipChildren
method private visit_pred p =
@@ -776,7 +776,7 @@ end = struct
method! vspec spec =
debug "@[[vspec] for %a @\n@]@."
- Kernel_function.pretty (Extlib.the self#current_kf);
+ Kernel_function.pretty (Option.get self#current_kf);
let finfo = self#get_finfo () in
let b = Cil.visitCilBehaviors (self:>Cil.cilVisitor) spec.spec_behavior in
let b = List.filter (not $ Cil.is_empty_behavior) b in
@@ -808,7 +808,7 @@ end = struct
*)
method private build_proto is_first finfo loc =
- let kf = Extlib.the self#current_kf in
+ let kf = Option.get self#current_kf in
fi <- Some finfo;
let new_var = ff_var fun_vars kf finfo in
(* we're building a prototype. *)
@@ -888,9 +888,9 @@ end = struct
end
method private compute_fct_prototypes (_fct_var,loc) =
- let finfo_list = Info.fct_info pinfo (Extlib.the self#current_kf) in
+ let finfo_list = Info.fct_info pinfo (Option.get self#current_kf) in
debug "@[[compute_fct_prototypes] for %a (x%d)@\n@]@."
- Kernel_function.pretty (Extlib.the self#current_kf)
+ Kernel_function.pretty (Option.get self#current_kf)
(List.length finfo_list);
let build_cil_proto is_first finfo =
self#build_proto is_first finfo loc
@@ -904,7 +904,7 @@ end = struct
method private compute_fct_definitions f loc =
let fvar = f.Cil_types.svar in
- let kf = Extlib.the self#current_kf in
+ let kf = Option.get self#current_kf in
let finfo_list = Info.fct_info pinfo kf in
debug "@[[compute_fct_definitions] for %a (x%d)@\n@]@."
Kernel_function.pretty kf (List.length finfo_list);
@@ -927,7 +927,7 @@ end = struct
Varinfo.Hashtbl.add fi_table new_fct_var finfo;
debug "@[[build_cil_fct] -> %s@\n@]@."
(Info.fct_name
- (Kernel_function.get_vi (Extlib.the self#current_kf)) finfo);
+ (Kernel_function.get_vi (Option.get self#current_kf)) finfo);
let action () =
Queue.add
(fun () ->
diff --git a/src/kernel_services/ast_transformations/inline.ml b/src/kernel_services/ast_transformations/inline.ml
index 6c5bbf9293e348132b99047bd4dd3ab23efc70e8..5d6c4d4b1ffcaf0d283c5e605ed12468ff3cbf80 100644
--- a/src/kernel_services/ast_transformations/inline.ml
+++ b/src/kernel_services/ast_transformations/inline.ml
@@ -231,7 +231,7 @@ let inliner functions_to_inline = object (self)
let scope = Stack.top block_stack in
let v =
Cil.makeLocalVar
- (Extlib.the self#current_func)
+ (Option.get self#current_func)
~scope ~temp:true "__inline_tmp" rt
in
true, Some (Cil.var v), args
@@ -241,7 +241,7 @@ let inliner functions_to_inline = object (self)
let scope = Stack.top block_stack in
let v =
Cil.makeLocalVar
- (Extlib.the self#current_func)
+ (Option.get self#current_func)
~scope ~temp:true "__inline_tmp" t
in
true, Some (Cil.var v), args
@@ -258,7 +258,7 @@ let inliner functions_to_inline = object (self)
let block =
inline_call
(Cil_datatype.Stmt.loc stmt)
- (Extlib.the self#current_kf)
+ (Option.get self#current_kf)
callee return_aux args
in
let fun_name = Kernel_function.get_name callee in
diff --git a/src/kernel_services/visitors/visitor.ml b/src/kernel_services/visitors/visitor.ml
index f367157a04f2a16ed416cd75e3ed1a815ac4f4ad..dbda6a580bb29b8324390d9e9f2c99a5eef13238 100644
--- a/src/kernel_services/visitors/visitor.ml
+++ b/src/kernel_services/visitors/visitor.ml
@@ -114,7 +114,7 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
in
let change_stmt stmt (add, remove) =
if (add <> [] || remove <> []) then begin
- let kf = Extlib.the self#current_kf in
+ let kf = Option.get self#current_kf in
let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
Queue.add
(fun () ->
@@ -159,7 +159,7 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
method vglob_aux _ = DoChildren
method private vbehavior_annot ?e b =
- let kf = Extlib.the self#current_kf in
+ let kf = Option.get self#current_kf in
let treat_elt emit elt acc =
match e with
| None -> (emit, elt) :: acc
@@ -387,7 +387,7 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
| DoChildrenPost f -> visit_clauses self f
method private vfunspec_annot () =
- let kf = Extlib.the self#current_kf in
+ let kf = Option.get self#current_kf in
let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
let old_behaviors =
Annotations.fold_behaviors (fun e b acc -> (e,b)::acc) kf []
@@ -671,7 +671,7 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
let get_spec () = match g with
| GFun _ | GFunDecl _ when Ast.is_def_or_last_decl g ->
let spec =
- Annotations.funspec ~populate:false (Extlib.the self#current_kf)
+ Annotations.funspec ~populate:false (Option.get self#current_kf)
in
Some (Cil.visitCilFunspec self#plain_copy_visitor spec)
| _ -> None
@@ -721,7 +721,7 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
self#get_filling_actions;
if
Cil_datatype.Varinfo.equal v
- (Kernel_function.get_vi new_kf) && Extlib.has_some spec
+ (Kernel_function.get_vi new_kf) && Option.is_some spec
then
Queue.add
(fun () ->
@@ -776,7 +776,7 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
self#get_filling_actions;
if Cil_datatype.Varinfo.equal f.svar
(Kernel_function.get_vi new_kf)
- && Extlib.has_some spec
+ && Option.is_some spec
then
Queue.add
(fun () -> Annotations.register_funspec ~force:true new_kf)
diff --git a/src/libraries/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml
index 17adae5adc6ce45b1e2fe3610fc2214d0fe60c6d..5502d9f81c0a46a0d16ea781adf52d1ff188b2eb 100644
--- a/src/libraries/stdlib/extlib.ml
+++ b/src/libraries/stdlib/extlib.ml
@@ -246,8 +246,6 @@ let array_existsi f a =
(** {2 Options} *)
(* ************************************************************************* *)
-let has_some = function None -> false | Some _ -> true
-
let opt_if b v = if b then None else Some v
let opt_fold f o b =
@@ -261,10 +259,6 @@ let merge_opt f k o1 o2 =
| Some x, None | None, Some x -> Some x
| Some x1, Some x2 -> Some (f k x1 x2)
-let opt_bind f = function
- | None -> None
- | Some x -> f x
-
let opt_filter f = function
| None -> None
| (Some x) as o -> if f x then o else None
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index dfbfd5728b1b1aa3908052a197cd3d30ea9c332e..06924f16a1144c897333fc48034487558deae32c 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -195,10 +195,6 @@ val array_existsi: (int -> 'a -> bool) -> 'a array -> bool
(** {2 Options} *)
(* ************************************************************************* *)
-(** [true] iff its argument is [Some x]
- @since Nitrogen-20111001 *)
-val has_some: 'a option -> bool
-
val opt_if: bool -> 'a -> 'a option
(** [opt_if cond v] returns [Some v] if [cond] is [true] and
[None] otherwise *)
@@ -219,12 +215,6 @@ val opt_fold: ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
val merge_opt:
('a -> 'b -> 'b -> 'b) -> 'a -> 'b option -> 'b option -> 'b option
-(** [opt_bind f x] returns [None] if [x] is [None] and [f y] if is [Some y]
- (monadic bind)
- @since Nitrogen-20111001
-*)
-val opt_bind: ('a -> 'b option) -> 'a option -> 'b option
-
val opt_filter: ('a -> bool) -> 'a option -> 'a option
val the: ?exn:exn -> 'a option -> 'a
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index d73cb2c8b83e9d923e51c5a610aa32de6095c8aa..7bae8b34ad4fab3c19e3179626a316d3b725b09a 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -222,7 +222,8 @@ let isCrossableAtInit tr func =
match base with
| TVar v ->
(try
- Extlib.opt_bind
+ Option.bind
+ v.lv_origin
(fun v ->
let init = Globals.Vars.find v in
let init = match init.Cil_types.init with
@@ -230,7 +231,6 @@ let isCrossableAtInit tr func =
| Some i -> i
in
aux_init off init)
- v.lv_origin
with Not_found -> None)
| TMem t ->
(match (aux t).term_node with
@@ -931,7 +931,7 @@ class visit_decl_loops_init () =
match stmt.skind with
| Loop _ ->
let scope = Kernel_function.find_enclosing_block stmt in
- let f = Extlib.the self#current_func in
+ let f = Option.get self#current_func in
let name = Data_for_aorai.loopInit ^ "_" ^ (string_of_int stmt.sid) in
let typ =
Cil.typeAddAttributes
@@ -1270,13 +1270,13 @@ let action_assigns trans =
(Cil.typeOfTermLval (host,my_off)))
acc
| Pebble_init(_,v,c) ->
- let cc = Extlib.the c.lv_origin in
- let cv = Extlib.the v.lv_origin in
+ let cc = Option.get c.lv_origin in
+ let cv = Option.get v.lv_origin in
add_if_needed cv (Logic_const.tvar v)
(add_if_needed cc (Logic_const.tvar c) acc)
| Pebble_move(_,v1,_,v2) ->
- let cv1 = Extlib.the v1.lv_origin in
- let cv2 = Extlib.the v2.lv_origin in
+ let cv1 = Option.get v1.lv_origin in
+ let cv2 = Option.get v2.lv_origin in
add_if_needed cv1 (Logic_const.tvar v1)
(add_if_needed cv2 (Logic_const.tvar v2) acc)
in
@@ -1284,7 +1284,7 @@ let action_assigns trans =
let empty_pebble =
match trans.start.multi_state, trans.stop.multi_state with
| Some(_,aux), None ->
- let caux = Extlib.the aux.lv_origin in
+ let caux = Option.get aux.lv_origin in
add_if_needed caux (Logic_const.tvar aux) empty
| _ -> empty
in
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index 65c1781695d9075dc4dc77ce2108c188d842c7d6..f771e84066947d6ff88d6a21fa480a390b6aa254 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -121,7 +121,7 @@ class visit_adding_code_for_synchronisation =
method! vglob_aux g =
match g with
| GFun (fundec,loc) ->
- let kf = Extlib.the self#current_kf in
+ let kf = Option.get self#current_kf in
let vi = Kernel_function.get_vi kf in
let vi_pre = Cil_const.copy_with_new_vid vi in
vi_pre.vname <- Data_for_aorai.get_fresh (vi_pre.vname ^ "_pre_func");
@@ -208,7 +208,7 @@ class visit_adding_code_for_synchronisation =
method! vstmt_aux stmt =
match stmt.skind with
| Return (res,loc) ->
- let kf = Extlib.the self#current_kf in
+ let kf = Option.get self#current_kf in
let vi = Kernel_function.get_vi kf in
let current_function = vi.vname in
if not (Data_for_aorai.isIgnoredFunction current_function) then begin
@@ -907,7 +907,7 @@ class visit_adding_pre_post_from_buch treatloops =
method private leave_block () = !(Stack.pop has_call)
method! vfunc f =
- let my_kf = Extlib.the self#current_kf in
+ let my_kf = Option.get self#current_kf in
let vi = Kernel_function.get_vi my_kf in
let spec = Annotations.funspec my_kf in
let loc = Kernel_function.get_location my_kf in
@@ -940,7 +940,7 @@ class visit_adding_pre_post_from_buch treatloops =
method! vglob_aux g =
match g with
| GFun(f,_) ->
- let my_kf = Extlib.the self#current_kf in
+ let my_kf = Option.get self#current_kf in
(* don't use get_spec, as we'd generate default assigns,
while we'll fill the spec just below. *)
let vi = Kernel_function.get_vi my_kf in
@@ -981,7 +981,7 @@ class visit_adding_pre_post_from_buch treatloops =
| _ -> DoChildren;
method! vstmt_aux stmt =
- let kf = Extlib.the self#current_kf in
+ let kf = Option.get self#current_kf in
let treat_loop body_ref stmt =
let init_state = Data_for_aorai.get_loop_init_state stmt in
let inv_state = Data_for_aorai.get_loop_invariant_state stmt in
@@ -1105,7 +1105,7 @@ class visit_adding_pre_post_from_buch treatloops =
List.iter
(update_assigns
(Cil_datatype.Stmt.loc stmt)
- (Extlib.the self#current_kf)
+ (Option.get self#current_kf)
(Kstmt stmt))
specs;
s
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index eb6a9d98a5182c2f4b8e96633ab1ed7ded20825d..ec4242b8b794db748713326beae4166d7c5ea4fa 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -306,7 +306,7 @@ let update_condition vi1 vi2 cond =
let pebble_set_at li lab =
assert (li.l_profile = []);
let labels = List.map (fun _ -> lab) li.l_labels in
- Logic_const.term (Tapp (li,labels,[])) (Extlib.the li.l_type)
+ Logic_const.term (Tapp (li,labels,[])) (Option.get li.l_type)
let memo_multi_state st =
match st.multi_state with
@@ -327,8 +327,8 @@ let memo_multi_state st =
| Some multi_state -> multi_state
let change_bound_var st1 st2 cond =
- if Extlib.has_some st1.multi_state then begin
- let (_,idx1) = Extlib.the st1.multi_state in
+ if Option.is_some st1.multi_state then begin
+ let (_,idx1) = Option.get st1.multi_state in
let (_,idx2) = memo_multi_state st2 in
update_condition idx1 idx2 cond
end else cond
@@ -987,7 +987,7 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
in
let might_be_zero =
is_opt ||
- (match Extlib.the elt.min_rep with PCst _ -> false | _ -> true)
+ (match Option.get elt.min_rep with PCst _ -> false | _ -> true)
in
let at_most_one =
is_opt &&
@@ -1021,7 +1021,7 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
let guard_exit_loop env current counter =
if is_opt then TTrue
else
- let e = Extlib.the elt.min_rep in
+ let e = Option.get elt.min_rep in
let _,e,_ = type_expr metaenv env ?current e in
(* If we have done at least the lower bound of cycles, we can exit
the loop. *)
@@ -1195,7 +1195,7 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
if needs_pebble then Some curr_start else None
in
let _,t,_ =
- type_expr metaenv env ?current (Extlib.the elt.min_rep)
+ type_expr metaenv env ?current (Option.get elt.min_rep)
in
TRel (Cil_types.Req, t, Logic_const.tinteger ~loc 0)
in
@@ -1302,7 +1302,7 @@ let type_trans auto metaenv env tr =
match tr.cross with
| Seq seq ->
let default_state = find_otherwise_trans auto tr.start in
- let has_default_state = Extlib.has_some default_state in
+ let has_default_state = Option.is_some default_state in
let env,states, transitions,_,_ =
type_seq has_default_state tr metaenv env needs_pebble tr.start tr.stop seq
in
diff --git a/src/plugins/callgraph/cg.ml b/src/plugins/callgraph/cg.ml
index 36c3434ae1d7c3dc0cefaa377c56291fda6d6ee8..57bfa6b1fb80c79f4800df286fcfe6f84bd0cab3 100644
--- a/src/plugins/callgraph/cg.ml
+++ b/src/plugins/callgraph/cg.ml
@@ -133,7 +133,7 @@ let syntactic_compute g =
(* add defined functions into the graph *)
method !vfunc _f =
- G.add_vertex g (Extlib.the self#current_kf);
+ G.add_vertex g (Option.get self#current_kf);
Cil.DoChildren
(* add edges from callers to callees into the graph *)
@@ -144,17 +144,17 @@ let syntactic_compute g =
try Globals.Functions.get vi
with Not_found -> assert false
in
- let caller = Extlib.the self#current_kf in
- G.add_edge_e g (caller, Extlib.the self#current_stmt, callee);
+ let caller = Option.get self#current_kf in
+ G.add_edge_e g (caller, Option.get self#current_stmt, callee);
Cil.SkipChildren
| Call _ ->
(* call via a function pointer: add an edge from each function which
the address is taken to this callee. *)
let pointed = get_pointed_kfs () in
- let caller = Extlib.the self#current_kf in
+ let caller = Option.get self#current_kf in
List.iter
(fun callee ->
- G.add_edge_e g (caller, Extlib.the self#current_stmt, callee))
+ G.add_edge_e g (caller, Option.get self#current_stmt, callee))
pointed;
Cil.SkipChildren
| Local_init (_,ConsInit(v,_,_),_) ->
@@ -162,8 +162,8 @@ let syntactic_compute g =
try Globals.Functions.get v
with Not_found -> assert false
in
- let caller = Extlib.the self#current_kf in
- G.add_edge_e g (caller, Extlib.the self#current_stmt, callee);
+ let caller = Option.get self#current_kf in
+ G.add_edge_e g (caller, Option.get self#current_stmt, callee);
Cil.SkipChildren
| Local_init (_, AssignInit _, _) | Set _
| Skip _ | Asm _ | Code_annot _ ->
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 95af8d3219d414edd77bcb548a3b2a39f3e70214..03f14617e46e368c6765897f96219deb88b58b03 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -339,7 +339,7 @@ let build_node_writes context node =
match Node_kind.get_base node.node_kind with
(* TODO refine formal dependency computation for non-scalar formals *)
| Some vi when vi.vformal ->
- let kf = Extlib.the (Kernel_function.find_defining_kf vi) in
+ let kf = Option.get (Kernel_function.find_defining_kf vi) in
let pos = Kernel_function.get_formal_position vi kf in
let callsites =
match Callstack.pop callstack with
diff --git a/src/plugins/dive/node_kind.ml b/src/plugins/dive/node_kind.ml
index b52dd75817443a29118981186e3396a1b9db6304..20fd1656ee2d13e4954a0465476855e110dbcfaa 100644
--- a/src/plugins/dive/node_kind.ml
+++ b/src/plugins/dive/node_kind.ml
@@ -122,7 +122,7 @@ let to_lval = function
let pretty fmt = function
| (Scalar _ | Composite _ | Scattered _ | Unknown _) as kind ->
- Cil_printer.pp_lval fmt (Extlib.the (to_lval kind))
+ Cil_printer.pp_lval fmt (Option.get (to_lval kind))
| Alarm (_stmt,alarm) ->
Cil_printer.pp_predicate fmt (Alarms.create_predicate alarm)
| AbsoluteMemory ->
diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml
index 746d8b7281066902fde2a49e568efc8f8129de36..7d2efc4861d4abbbff5f8d286f2798c288d75d3c 100644
--- a/src/plugins/dive/server_interface.ml
+++ b/src/plugins/dive/server_interface.ml
@@ -267,8 +267,8 @@ let finalize' context node_opt =
may_explore Build.explore_backward !global_window.perception.backward;
may_explore Build.explore_forward !global_window.perception.forward;
let horizon = !global_window.horizon in
- if Extlib.has_some horizon.forward ||
- Extlib.has_some horizon.backward
+ if Option.is_some horizon.forward ||
+ Option.is_some horizon.backward
then
Build.reduce_to_horizon context horizon node
end;
diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.ml b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
index 278131df75937d9e65476fe1fdc040976a7744b0..cfb1f9aae8c5e55f86ca9ff094a149d0e763df88 100644
--- a/src/plugins/e-acsl/src/analyses/memory_tracking.ml
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
@@ -646,7 +646,7 @@ end = struct
List.iter
(fun s ->
let old =
- try Extlib.the (Stmt.Hashtbl.find tbl s)
+ try Option.get (Stmt.Hashtbl.find tbl s)
with Not_found -> assert false
in
Stmt.Hashtbl.replace
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index c2c575ec46b538c264be6ed63cf325baebe2e2c9..55bec5e40a5738218b6d8d9e48985c596e420b34 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -485,8 +485,8 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
in
List.iter2 typ_arg li.l_profile args;
(* [li.l_type is [None] for predicate only: not possible here.
- Thus using [Extlib.the] is fine *)
- dup (ty_of_logic_ty (Extlib.the li.l_type))
+ Thus using [Option.get] is fine *)
+ dup (ty_of_logic_ty (Option.get li.l_type))
else begin
(* TODO: what if the type of the parameter is smaller than the infered
type of the argument? For now, it is silently ignored (both
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index aed6379b6099850953beedf31464bd93aa368a3b..960cddb412e78a632121512474dde0894afc113a 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -656,7 +656,7 @@ and context_insensitive_term_to_exp kf env t =
env
kf
(Some t)
- (Misc.cty (Extlib.the li.l_type))
+ (Misc.cty (Option.get li.l_type))
(fun vi _ ->
[ Smart_stmt.rtl_call ~loc
~result:(Cil.var vi)
diff --git a/src/plugins/gui/analyses_manager.ml b/src/plugins/gui/analyses_manager.ml
index b87ee5a899a8c4f278e49ea93341f32f9f0d2929..1a94f476eb1a85a0844111949cf3092e6945d02e 100644
--- a/src/plugins/gui/analyses_manager.ml
+++ b/src/plugins/gui/analyses_manager.ml
@@ -72,7 +72,7 @@ let insert (main_ui: Design.main_window_extension_points) =
]
in
default_analyses_items.(0)#add_accelerator `CONTROL 'r';
- let stop_button = Extlib.the default_analyses_items.(2)#tool_button in
+ let stop_button = Option.get default_analyses_items.(2)#tool_button in
Gtk_helper.register_locking_machinery
~lock_last:true
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index 24526c43e651994c896d6c0f15f7fdd0ef6ff282..c5a986d5802ee1663188d80d51817a05a251fdc8 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -602,7 +602,7 @@ let to_do_on_select
(if vi.vaddrof then "" else "not ")
end else begin
main_ui#view_original vi.vdecl;
- let kf = Extlib.the kf in
+ let kf = Option.get kf in
main_ui#pretty_information
"This is the declaration of %s %a in function %a%t@."
(formal_or_local vi) Varinfo.pretty vi
@@ -1040,7 +1040,7 @@ class main_window () : main_window_extension_points =
m
| Some s ->
s
- method file_tree = Extlib.the file_tree
+ method file_tree = Option.get file_tree
method file_tree_view = file_tree_view
method annot_window = annot_window
diff --git a/src/plugins/gui/filetree.ml b/src/plugins/gui/filetree.ml
index afa164d4dee000ad3c92173574aa2b5f1ac55ce9..48f9fe8717e8c69848fb9326da7415b0abce54f8 100644
--- a/src/plugins/gui/filetree.ml
+++ b/src/plugins/gui/filetree.ml
@@ -830,7 +830,7 @@ let make (tree_view:GTree.view) =
in
try
let {MODEL.finfo=t} =
- Extlib.the (model_custom#custom_get_iter path) in
+ Option.get (model_custom#custom_get_iter path) in
let selected_node = MYTREE.storage_type t in
let was_activated = match current_node with
| None -> false
@@ -882,7 +882,7 @@ let make (tree_view:GTree.view) =
expand_to_path tree_view path;
tree_view#selection#select_path path;
(* set_cursor updates the keyboard cursor and scrolls to the element *)
- tree_view#set_cursor path (Extlib.the name_column);
+ tree_view#set_cursor path (Option.get name_column);
tree_view#misc#grab_focus ()
(* TODO: keep the structure of the tree, ie. reexpand all the nodes that
diff --git a/src/plugins/gui/pretty_source.ml b/src/plugins/gui/pretty_source.ml
index fae7a1f6c75b9dad6da3f7d676e01af913aca608..91255b5d6f2a4565d67d889f5f9e2206b079970a 100644
--- a/src/plugins/gui/pretty_source.ml
+++ b/src/plugins/gui/pretty_source.ml
@@ -477,7 +477,7 @@ class pos_to_localizable =
| _ -> false
in
if not skip then
- self#add_range (Stmt.loc s) (PStmt (Extlib.the self#current_kf, s));
+ self#add_range (Stmt.loc s) (PStmt (Option.get self#current_kf, s));
begin
match s.skind with
| If (exp, _, _, _) ->
diff --git a/src/plugins/inout/derefs.ml b/src/plugins/inout/derefs.ml
index e321993b1f00aea074068129cdc9533ab608f521..4cc972c9bfa94669b66323bb16d31f7ca5e8bdf3 100644
--- a/src/plugins/inout/derefs.ml
+++ b/src/plugins/inout/derefs.ml
@@ -41,7 +41,7 @@ class virtual do_it_ = object(self)
| Var _ -> ()
| Mem e ->
let state =
- Db.Value.get_state (Kstmt (Extlib.the self#current_stmt))
+ Db.Value.get_state (Kstmt (Option.get self#current_stmt))
in
let r = !Db.Value.eval_expr state e in
let loc = loc_bytes_to_loc_bits r in
diff --git a/src/plugins/markdown-report/eva_info.ml b/src/plugins/markdown-report/eva_info.ml
index 6c1ee9d5a9abfd4645c4ea0412abe8c8326991e0..5df8dbbefda486fe5918bb38ab77b3b981c1bbf4 100644
--- a/src/plugins/markdown-report/eva_info.ml
+++ b/src/plugins/markdown-report/eva_info.ml
@@ -113,7 +113,7 @@ class eva_coverage_vis ~from_entry_point = object(self)
end;
Cil.SkipChildren
| Call(_,{ enode = Lval (Mem _,NoOffset)},_,_) ->
- let s = Extlib.the self#current_stmt in
+ let s = Option.get self#current_stmt in
let kfs = Db.Value.call_to_kernel_function s in
let handle_one kf =
let vi = Kernel_function.get_vi kf in
diff --git a/src/plugins/markdown-report/sarif_gen.ml b/src/plugins/markdown-report/sarif_gen.ml
index eef65f58e28959cb41e13400b5d33111dda3af21..37fd6b824e300ae8820e6581f6eea17ac26aa84a 100644
--- a/src/plugins/markdown-report/sarif_gen.ml
+++ b/src/plugins/markdown-report/sarif_gen.ml
@@ -189,7 +189,7 @@ let gen_results remarks =
rules, List.rev content
let is_alarm = function
- | Property.(IPCodeAnnot { ica_ca }) -> Extlib.has_some (Alarms.find ica_ca)
+ | Property.(IPCodeAnnot { ica_ca }) -> Option.is_some (Alarms.find ica_ca)
| _ -> false
let make_ip_message ip =
diff --git a/src/plugins/metrics/metrics_gui.ml b/src/plugins/metrics/metrics_gui.ml
index 698610666657f1044faa798300d2be53a37714cc..c544bf91e8efdc3ab3b85c591bd1a45cbb6207e7 100644
--- a/src/plugins/metrics/metrics_gui.ml
+++ b/src/plugins/metrics/metrics_gui.ml
@@ -116,7 +116,7 @@ let coerce_panel_to_ui panel_box _main_ui = "Metrics", panel_box#coerce, None ;;
let register_metrics ?(apply=false) name display_function =
add_panel_action (name, display_function);
let metrics_panel = get_panel () in
- GEdit.text_combo_add (Extlib.the metrics_panel.top) name;
+ GEdit.text_combo_add (Option.get metrics_panel.top) name;
if apply
- then display_function (Extlib.the metrics_panel.bottom);
+ then display_function (Option.get metrics_panel.bottom);
;;
diff --git a/src/plugins/metrics/register_gui.ml b/src/plugins/metrics/register_gui.ml
index 8674e439cd21e72d233cceeb08354ca8df2b8e26..c953b64590a9659c26d59c262533b625709bd449 100644
--- a/src/plugins/metrics/register_gui.ml
+++ b/src/plugins/metrics/register_gui.ml
@@ -239,7 +239,7 @@ module ValueCoverageGUI = struct
end;
Metrics_coverage.compute_coverage_by_fun ();
!update_filetree `Contents;
- Extlib.the !result
+ Option.get !result
let decorate_filetree (main_ui: Design.main_window_extension_points) =
let compute get = function
diff --git a/src/plugins/occurrence/register_gui.ml b/src/plugins/occurrence/register_gui.ml
index d7b8da68dfc8abe36b54c7f5c9b0073c70a51d49..749c7fcfa329c7b8fee8dc6347b53d0be93e87a8 100644
--- a/src/plugins/occurrence/register_gui.ml
+++ b/src/plugins/occurrence/register_gui.ml
@@ -233,7 +233,7 @@ let file_tree_decorate (file_tree:Filetree.t) =
match ki with
| Kglobal -> false
| Kstmt _ ->
- let kf = Extlib.the kf in
+ let kf = Option.get kf in
let v0 = Kernel_function.get_vi kf in
List.exists
(fun glob -> match glob with
diff --git a/src/plugins/report/scan.ml b/src/plugins/report/scan.ml
index 22a116f5a246a1f423a1d30870112e723e582094..20b39c16207619626ee929685e26f1d25c2d5bdb 100644
--- a/src/plugins/report/scan.ml
+++ b/src/plugins/report/scan.ml
@@ -166,13 +166,13 @@ class visit_properties (phi : Property.t -> unit) =
method! vspec fspec =
Property.ip_of_spec
- (Extlib.the self#current_kf) self#current_kinstr ~active:[] fspec |>
+ (Option.get self#current_kf) self#current_kinstr ~active:[] fspec |>
List.iter phi ;
Cil.DoChildren
method! vcode_annot ca =
Property.ip_of_code_annot
- (Extlib.the self#current_kf) (Extlib.the self#current_stmt) ca |>
+ (Option.get self#current_kf) (Option.get self#current_stmt) ca |>
List.iter phi ;
Cil.DoChildren
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index 36c092b8a7ca1adc1f69f5179f552820a8e5644d..5d8f2564def70f0b69f299d634a23fb4fc02d2bf 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -106,7 +106,7 @@ class annot_visitor kf flags on_alarm = object (self)
flags.Flags.bool_value && not (Generator.Bool_value.is_computed kf)
method private queue_stmt_spec spec =
- let stmt = Extlib.the (self#current_stmt) in
+ let stmt = Option.get (self#current_stmt) in
Queue.add
(fun () ->
let annot = Logic_const.new_code_annotation (AStmtSpec ([], spec)) in
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index 1fb31afa260c5dd460f811a9024fede3e1ee27cb..481a00d4773639fdf3837ed580365eb5c6441e06 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -571,10 +571,10 @@ class check_annot_visitor = object(self)
method proven () = proven
method! vcode_annot annot =
- let kf = Extlib.the self#current_kf in
+ let kf = Option.get self#current_kf in
let stmt =
Visitor_behavior.Get_orig.stmt
- self#behavior (Extlib.the self#current_stmt)
+ self#behavior (Option.get self#current_stmt)
in
begin match annot.annot_content with
| AAssert _ ->
@@ -591,7 +591,7 @@ class check_annot_visitor = object(self)
method! vglob_aux g = match g with
| GFun (fdec, _loc) when
- !Db.Value.is_called (Extlib.the self#current_kf) &&
+ !Db.Value.is_called (Option.get self#current_kf) &&
not (!Db.Value.no_results fdec)
->
Cil.DoChildren
diff --git a/src/plugins/slicing/printSlice.ml b/src/plugins/slicing/printSlice.ml
index a02e5d882ccc7ec22407c6c56f7e339bd2ff6d26..8c4bae8bc798a259e19c413ffccffd05d5e508df 100644
--- a/src/plugins/slicing/printSlice.ml
+++ b/src/plugins/slicing/printSlice.ml
@@ -90,7 +90,7 @@ class printerClass optional_ff = object(self)
else
Format.fprintf fmt "@[/* %s */@]" str_m
in
- let s = Extlib.the self#current_stmt in
+ let s = Option.get self#current_stmt in
try
Format.fprintf fmt "@[<v>%a@ %a@]"
stmt_info s
@@ -104,7 +104,7 @@ class printerClass optional_ff = object(self)
let label_info = match opt_ff with
| None -> "label"
| Some ff ->
- let m = Fct_slice.get_label_mark ff (Extlib.the self#current_stmt) l in
+ let m = Fct_slice.get_label_mark ff (Option.get self#current_stmt) l in
SlicingMarks.mark_to_string m
in
Format.fprintf fmt "@[<hv>/* %s */@ %a@]"
diff --git a/src/plugins/sparecode/spare_marks.ml b/src/plugins/sparecode/spare_marks.ml
index de47a8f85f358f7929385770aab6172e3e6cbd4c..409c6b654ea44638112fcdd277d358d4e2918674 100644
--- a/src/plugins/sparecode/spare_marks.ml
+++ b/src/plugins/sparecode/spare_marks.ml
@@ -305,7 +305,7 @@ class annot_visitor ~filter pdg = object (self)
let () =
if filter annot then
try
- let stmt = Extlib.the self#current_stmt in
+ let stmt = Option.get self#current_stmt in
debug 1 "selecting annotation : %a @."
Printer.pp_code_annotation annot;
let info = !Db.Pdg.find_code_annot_nodes pdg stmt annot in
diff --git a/src/plugins/studia/writes.ml b/src/plugins/studia/writes.ml
index a877d0735c9ee35a217da30e03876f9e4fcee3ee..938c3f01dae0f66c54c4551dd469b895f224c5a4 100644
--- a/src/plugins/studia/writes.ml
+++ b/src/plugins/studia/writes.ml
@@ -56,7 +56,7 @@ class find_write zlval = object (self)
val mutable res = ([] : (stmt * effects) list)
method! vinst i =
- let stmt = Extlib.the self#current_stmt in
+ let stmt = Option.get self#current_stmt in
begin
let aux_call lvopt _kf _args _loc =
(* Direct effect through the writing of [lvopt], or indirect inside
diff --git a/src/plugins/value/alarmset.ml b/src/plugins/value/alarmset.ml
index 4a88c3eee32a50a552c5ebe5c42ef36845f68844..3f94efd96e9bb25f502870f9e30110caef784d15 100644
--- a/src/plugins/value/alarmset.ml
+++ b/src/plugins/value/alarmset.ml
@@ -229,7 +229,7 @@ let local_printer: Printer.extensible_printer =
method private pp_temporaries fmt =
let pp_var fmt vi =
- Format.fprintf fmt "%s from@ @[%s@]" vi.vname (Extlib.the vi.vdescr)
+ Format.fprintf fmt "%s from@ @[%s@]" vi.vname (Option.get vi.vdescr)
in
Pretty_utils.pp_iter Cil_datatype.Varinfo.Set.iter
~pre:"" ~suf:"" ~sep:",@ " pp_var fmt temporaries
diff --git a/src/plugins/value/domains/cvalue/builtins.ml b/src/plugins/value/domains/cvalue/builtins.ml
index e8478f7c7f85c0dd5a0c5952b8ce024ff93d5480..ba5c2f99bb99deed6fa3ad25c6140ab5359c25db 100644
--- a/src/plugins/value/domains/cvalue/builtins.ml
+++ b/src/plugins/value/domains/cvalue/builtins.ml
@@ -195,7 +195,7 @@ let prepare_builtins () =
(* Overrides builtins attribution according to the -eva-builtin option. *)
Value_parameters.BuiltinsOverrides.iter
(fun (kf, name) ->
- let builtin_name = Extlib.the name in
+ let builtin_name = Option.get name in
let f, typ, _, _ = Hashtbl.find table builtin_name in
prepare_builtin kf builtin_name f typ)
diff --git a/src/plugins/value/domains/cvalue/builtins_string.ml b/src/plugins/value/domains/cvalue/builtins_string.ml
index 7774f234d473f4c1fb5a5d7c2b942e827e18d6ad..f5ecbc9c136338a14d037c771107aee4a1a9c3db 100644
--- a/src/plugins/value/domains/cvalue/builtins_string.ml
+++ b/src/plugins/value/domains/cvalue/builtins_string.ml
@@ -52,7 +52,7 @@ type acc =
from: Ival.t; (* The offsets from which the current search has begun. *)
stop: bool; } (* True if the search is completely done. *)
-let the_max_int ival = Extlib.the (Ival.max_int ival)
+let the_max_int ival = Option.get (Ival.max_int ival)
let pos_min_int ival =
match Ival.min_int ival with
@@ -230,7 +230,7 @@ let search_offsm kind ~validity ~offset ~rem offsetmap =
| Base.Valid_range (Some (_min, max)) -> max
in
(* Uses [kind.limit] to bound the read. *)
- let limit_max = Extlib.opt_bind Ival.max_int kind.limit in
+ let limit_max = Option.bind kind.limit Ival.max_int in
let max = match Ival.max_int offset, limit_max with
| Some max_start, Some max_limit ->
let max = Integer.(add max_start (pred max_limit)) in
diff --git a/src/plugins/value/domains/cvalue/cvalue_init.ml b/src/plugins/value/domains/cvalue/cvalue_init.ml
index 285e4157d85df23a91bfd3bdc17e7aed1f0088af..b3552f45e727f9556dbf6d4a04e73060d7b85155 100644
--- a/src/plugins/value/domains/cvalue/cvalue_init.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_init.ml
@@ -251,7 +251,7 @@ let initialize_var_using_type varinfo state =
The periodicity of the contents may be smaller than the size
of a cell; take this into account. *)
let v, modu, offset =
- Extlib.the (Cvalue.V_Offsetmap.fold
+ Option.get (Cvalue.V_Offsetmap.fold
(fun _itv v _ -> Some v) offsm_joined None)
in
assert (Abstract_interp.Rel.(equal offset zero));
diff --git a/src/plugins/value/domains/cvalue/cvalue_specification.ml b/src/plugins/value/domains/cvalue/cvalue_specification.ml
index b67f8a616e24dae7757ca8322d4a7135c7c24355..84609e39c11e60890e0e4a020dd948ffd8e514b7 100644
--- a/src/plugins/value/domains/cvalue/cvalue_specification.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_specification.ml
@@ -127,7 +127,7 @@ let check_fct_assigns kf ab ~pre_state found_froms =
| WritesAny -> ()
| Writes(assigns_deps) ->
let bol = Property.Id_contract (Datatype.String.Set.empty,b) in
- let ip = Extlib.the (Property.ip_of_assigns kf Kglobal bol b.b_assigns)
+ let ip = Option.get (Property.ip_of_assigns kf Kglobal bol b.b_assigns)
in
let source = fst (Property.location ip) in
(* First, check the assigns. *)
@@ -163,7 +163,7 @@ let check_fct_assigns kf ab ~pre_state found_froms =
let status_txt, status =
check_from pre_state asgn assigns_zone deps found_froms
in
- let ip = Extlib.the (Property.ip_of_from kf Kglobal bol from) in
+ let ip = Option.get (Property.ip_of_from kf Kglobal bol from) in
let source = fst (asgn.it_content.term_loc) in
msg_status status ~once:true ~source
"%a: \\from ... part in assign clause got status %s.%a%t"
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index b04cd0ffa19955c80a0e67c183af5193509399ff..6475f861d9faca3cd2f4d47ffa940e38e16e1c6b 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -260,7 +260,7 @@ module Make
match Deps.intersects deps zone with
| [] -> equalities, deps, modified_zone
| atoms ->
- let extract_lval h = Extlib.the (HCE.to_lval h) in
+ let extract_lval h = Option.get (HCE.to_lval h) in
let atoms = List.map extract_lval atoms in
let process eq atom = Equality.Set.remove kt atom eq in
let equalities' = List.fold_left process equalities atoms in
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index 5b2a6fb1939c25dfb24f469e80a137f900413747..67159ad19c084c224c05344e3ecb315b9988a4d4 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -280,7 +280,7 @@ module Internal_Value = struct
let restrict_val =
let rec get: type v. v structure -> Value.t -> v = function
- | Leaf (key, _) -> Extlib.the (Value.get key)
+ | Leaf (key, _) -> Option.get (Value.get key)
| Node (s1, s2) ->
let get1 = get s1 and get2 = get s2 in
fun v -> get1 v, get2 v
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index 9353f679736bea92fbf9b1d09ac71aef41624bd0..51439e74e98003d30fd65779367e96e5072b5876 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -1044,7 +1044,7 @@ module Make
if Integer.is_zero size
then `Value index, Alarmset.none
else
- let size_expr = Extlib.the array_size in (* array_size exists *)
+ let size_expr = Option.get array_size in (* array_size exists *)
assume_valid_index ~size ~size_expr ~index_expr index
with
| Cil.LenOfArray -> `Value index, Alarmset.none (* unknown array size *)
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index 3fd1f6245fe8f8228ba0c88a29d97f92e06c5e94..a7862968059399ccb8f624c7bfe34393d633bbc4 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -333,7 +333,7 @@ module Make_Dataflow
match return_exp with
| None -> id
| Some return_exp ->
- let vi_ret = Extlib.the (Library_functions.get_retres_vi kf) in
+ let vi_ret = Option.get (Library_functions.get_retres_vi kf) in
let return_lval = Var vi_ret, NoOffset in
let kstmt = Kstmt stmt in
fun state ->
@@ -399,7 +399,7 @@ module Make_Dataflow
| _ -> flow
in
(* Loop transitions *)
- let the_stmt v = Extlib.the v.vertex_start_of in
+ let the_stmt v = Option.get v.vertex_start_of in
let enter_loop f v =
let f = Partition.enter_loop f (the_stmt v) in
Partition.transfer (lift (Domain.enter_loop (the_stmt v))) f
diff --git a/src/plugins/value/gui_files/gui_callstacks_manager.ml b/src/plugins/value/gui_files/gui_callstacks_manager.ml
index a83ba5f190b87fc09d7df7a69c09028168194528..03e7da9770d54803a55eb0eefbe2163b4d899b7d 100644
--- a/src/plugins/value/gui_files/gui_callstacks_manager.ml
+++ b/src/plugins/value/gui_files/gui_callstacks_manager.ml
@@ -603,7 +603,7 @@ module Make (Input: Input) = struct
in
(* Add 'Unfocus callstacks' option to menu. *)
let add_unfocus_callstacks menu icon =
- if Extlib.has_some model.focused_rev_callstacks then begin
+ if Option.is_some model.focused_rev_callstacks then begin
let unfocus = GMenu.menu_item ~label:"Unfocus callstack(s)" () in
(!!menu)#add unfocus;
ignore (unfocus#connect#activate (callback_focus_unfocus None icon))
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 8f81d533067683ac063e10450357b90e8f41fdcf..462e57405d35859dd5e0aeb0028e6412250685ef 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -548,7 +548,7 @@ let constraint_trange idx size_arr =
match idx.term_node with
| Trange ((None as low), up) | Trange (low, (None as up)) -> begin
let loc = idx.term_loc in
- match Extlib.opt_bind Cil.constFoldToInt size_arr with
+ match Option.bind size_arr Cil.constFoldToInt with
| None -> idx
| Some size ->
let low = match low with (* constrained l.h.s *)
@@ -576,7 +576,7 @@ let apply_logic_builtin builtin env args_list =
match res with
| None -> None
| Some offsm ->
- let v = Extlib.the (Cvalue.V_Offsetmap.single_interval_value offsm) in
+ let v = Option.get (Cvalue.V_Offsetmap.single_interval_value offsm) in
let v = Cvalue.V_Or_Uninitialized.get_v v in
Some (v, alarms)
diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml
index b2db87bd40e588e418ecd2e91043e9f3c73b1927..7fea184b5381034aae7a5889cad6705fdfe740ab 100644
--- a/src/plugins/value/utils/eva_annotations.ml
+++ b/src/plugins/value/utils/eva_annotations.ml
@@ -301,7 +301,7 @@ module Allocation = struct
let get stmt =
match get stmt with
- | [] -> Extlib.the (of_string (Value_parameters.AllocBuiltin.get ()))
+ | [] -> Option.get (of_string (Value_parameters.AllocBuiltin.get ()))
| [x] -> x
| x :: _ ->
Value_parameters.warning ~current:true ~once:true
diff --git a/src/plugins/variadic/format_parser.ml b/src/plugins/variadic/format_parser.ml
index f656b33b44ee33065981770a28da211dd12e9d95..045e562125866e1012f8dbc7f19b82ee0b67018d 100644
--- a/src/plugins/variadic/format_parser.ml
+++ b/src/plugins/variadic/format_parser.ml
@@ -39,7 +39,7 @@ let check_flag spec flag =
let cs = spec.f_conversion_specifier in
match flag, cs with
| FSharp, #has_alternative_form -> true
- | FZero, #integer_specifier when Extlib.has_some spec.f_precision ->
+ | FZero, #integer_specifier when Option.is_some spec.f_precision ->
warn "Flag 0 is ignored when a precision is specified"; false
| FZero, #numeric_specifier when List.mem FMinus spec.f_flags ->
warn "Flag 0 is ignored when flag - is also specified."; false
diff --git a/src/plugins/variadic/standard.ml b/src/plugins/variadic/standard.ml
index 27ed9f5e4baa3bd328d8961603b00d5cc1fa9d40..bd3a6e656999a09ae0bf67088be27fbbe017a165 100644
--- a/src/plugins/variadic/standard.ml
+++ b/src/plugins/variadic/standard.ml
@@ -433,7 +433,7 @@ let build_fun_spec env loc vf format_fun tvparams formals =
let labels = List.map (fun _ -> here) logic_info.l_labels in
let nterm = match precision with
| PStar ->
- let n_vi = List.nth vformals (Extlib.the pos) in
+ let n_vi = List.nth vformals (Option.get pos) in
Logic_utils.numeric_coerce Linteger (Build.tvar ~loc n_vi)
| PInt n -> Cil.lconstant ~loc (Integer.of_int n)
in
diff --git a/src/plugins/wp/Layout.ml b/src/plugins/wp/Layout.ml
index 8c7feafeab961d95a86a48370a0379bf101f88ed..e7246abceb43a05edbd0625d2b67cf9fa7082488 100644
--- a/src/plugins/wp/Layout.ml
+++ b/src/plugins/wp/Layout.ml
@@ -70,7 +70,7 @@ struct
match Cil.unrollType ty with
| TArray(te,n,_,_) ->
begin
- match Extlib.opt_bind Ctypes.get_int n with
+ match Option.bind n Ctypes.get_int with
| None -> failwith "Wp.Layout: unkown array size"
| Some n -> Index(te,n)
end
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 6f5d175e464713b46533a0658a7424483c7795f3..54e5d9d0cbf24f3a2768a07a0f1a8a0dccca85a8 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -284,7 +284,7 @@ struct
let neg = Q.sign q < 0 in
let int,frac,exp = (group 1 s), (group 2 s), (group 3 s) in
let exp = if String.equal exp "" then None else Some exp in
- let ty = Extlib.the (of_tau ~cnv tau) in
+ let ty = Option.get (of_tau ~cnv tau) in
why3_real ty ~radix:16 ~neg ~int ~frac ?exp ()
else raise Not_found
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 3ec42cd39887e304c6853b4a10abd888980836dd..a95b4a864909dffb1047d8539b10948a51d73d00 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -121,12 +121,12 @@ let mk_var_pos_id kf s ca = mk_prop PKVarPos (mk_annot_id kf s ca)
let mk_loop_from_id kf s ca from =
let id = Property.ip_of_from kf (Kstmt s) (Property.Id_loop ca) from in
- mk_prop PKPropLoop (Extlib.the id)
+ mk_prop PKPropLoop (Option.get id)
let mk_bhv_from_id kf ki a bhv from =
let a = Datatype.String.Set.of_list a in
let id = Property.ip_of_from kf ki (Property.Id_contract (a,bhv)) from in
- mk_prop PKProp (Extlib.the id)
+ mk_prop PKProp (Option.get id)
let get_kind_for_tk kf tkind = match tkind with
| Normal ->
@@ -138,7 +138,7 @@ let mk_fct_from_id kf bhv tkind from =
let contract_info = Property.Id_contract(Datatype.String.Set.empty,bhv) in
let id = Property.ip_of_from kf Kglobal contract_info from in
let kind = get_kind_for_tk kf tkind in
- mk_prop kind (Extlib.the id)
+ mk_prop kind (Option.get id)
let mk_disj_bhv_id (kf,ki,active,disj) =
mk_prop PKProp (Property.ip_of_disjoint kf ki active disj)
diff --git a/src/plugins/wp/wpReport.ml b/src/plugins/wp/wpReport.ml
index 6bdd9397a04e55018e96370fa42afd2ce900c248..d555742566b2550c7115616c56d79300cb7f37fa 100644
--- a/src/plugins/wp/wpReport.ml
+++ b/src/plugins/wp/wpReport.ml
@@ -493,7 +493,7 @@ let iter_stat ?first ?sep ?last ~from start next=
| Some app -> app v
in
let next app =
- let item = (Extlib.the !items) in
+ let item = (Option.get !items) in
apply item app;
items := next item
in