diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 711d6633ecfaf337bb9107acdffc1dd9385aefb6..6c81d0d29e333ec420cb92d0b36cc0c1bb438bef 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1263,7 +1263,8 @@ let createCompInfo (iss: bool) (n: string) ~(norig: string) : compinfo * bool =
with Not_found -> begin
(* Create a compinfo. This will have "cdefined" false. *)
let res =
- Cil_const.mkCompInfo iss n ~norig (fun _ -> None) (fc_stdlib_attribute [])
+ Cil_const.mkCompInfo
+ iss n ~norig (fun _ -> None) (fc_stdlib_attribute [])
in
H.add compInfoNameEnv key res;
res, true
@@ -3342,7 +3343,7 @@ let rec setOneInit this o preinit =
| f' :: _ when f'.fname = f.fname -> idx
| _ :: restf -> loop (idx + 1) restf
in
- loop 0 (Extlib.opt_conv [] f.fcomp.cfields), off
+ loop 0 (Option.value ~default:[] f.fcomp.cfields), off
| _ -> abort_context "setOneInit: non-constant index"
in
let pMaxIdx, pArray =
@@ -3519,7 +3520,8 @@ let rec collectInitializer
let rest, reads' = collect (idx+1) reads' restf in
(Field(f, NoOffset), thisi) :: rest, reads'
in
- let init, reads = collect 0 reads (Extlib.opt_conv [] comp.cfields) in
+ let init, reads =
+ collect 0 reads (Option.value ~default:[] comp.cfields) in
CompoundInit (thistype, init), thistype, reads
| TComp (comp, _, _), CompoundPre (pMaxIdx, pArray) when not comp.cstruct ->
@@ -3543,7 +3545,7 @@ let rec collectInitializer
if Cil.msvcMode () && !pMaxIdx != 0 then
Kernel.warning ~current:true
"On MSVC we can initialize only the first field of a union";
- let init, reads = findField 0 (Extlib.opt_conv [] comp.cfields) in
+ let init, reads = findField 0 (Option.value ~default:[] comp.cfields) in
CompoundInit (thistype, [ init ]), thistype, reads
| _ -> Kernel.fatal ~current:true "collectInitializer"
@@ -3684,7 +3686,7 @@ let fieldsToInit
the resulting fields are in reverse order *)
let rec add_comp (offset : offset) (comp : compinfo) acc =
let in_union = not comp.cstruct in
- add_fields offset in_union (Extlib.opt_conv [] comp.cfields) acc
+ add_fields offset in_union (Option.value ~default:[] comp.cfields) acc
and add_fields (offset : offset) (in_union : bool) (l : fieldinfo list) acc =
match l with
| [] -> acc
@@ -3744,7 +3746,9 @@ let find_field_offset cond (fidlist: fieldinfo list) : offset =
| fid :: rest when prefix anonCompFieldName fid.fname -> begin
match unrollType fid.ftype with
| TComp (ci, _, _) ->
- (try let off = search (Extlib.opt_conv [] ci.cfields) in Field(fid,off)
+ (try
+ let off = search (Option.value ~default:[] ci.cfields) in
+ Field(fid,off)
with Not_found -> search rest (* Continue searching *))
| _ ->
abort_context "unnamed field type is not a struct/union"
@@ -3755,7 +3759,7 @@ let find_field_offset cond (fidlist: fieldinfo list) : offset =
let findField n comp =
try
- find_field_offset (fun x -> x.fname = n) (Extlib.opt_conv [] comp.cfields)
+ find_field_offset (fun x -> x.fname = n) (Option.value ~default:[] comp.cfields)
with Not_found ->
abort_context "Cannot find field %s in type %s" n (Cil.compFullName comp)
@@ -5502,7 +5506,7 @@ and makeCompType ghost (isstruct: bool)
end else
List.iter
(fun f -> is_circular f.ftype)
- (Extlib.opt_conv [] comp'.cfields);
+ (Option.value ~default:[] comp'.cfields);
| _ -> ()
in
is_circular ftype;
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index ead5136f1f6c08f40b1163de08ef19dd00873bc9..cfde5abedf94c2bd452b2a1a3e71346214eaf27f 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -1200,8 +1200,8 @@ and matchCompInfo (oldfidx: int) (oldci: compinfo)
let ci = cinode.ndata in
let fidx = cinode.nfidx in
- let old_len = List.length (Extlib.opt_conv [] oldci.cfields) in
- let len = List.length (Extlib.opt_conv [] ci.cfields) in
+ let old_len = List.length (Option.value ~default:[] oldci.cfields) in
+ let len = List.length (Option.value ~default:[] ci.cfields) in
(* It is easy to catch here the case when the new structure is undefined
* and the old one was defined. We just reuse the old *)
(* More complicated is the case when the old one is not defined but the
@@ -2166,29 +2166,29 @@ class renameVisitorClass =
method private update_field f =
(* See if the compinfo was changed *)
- if f.fcomp.creferenced then None
- else begin
- match
- PlainMerging.findReplacement true sEq !currentFidx f.fcomp.cname
- with
- None -> None (* We did not replace it *)
- | Some (ci', _oldfidx) -> begin
- (* First, find out the index of the original field *)
- let rec indexOf (i: int) = function
- | [] -> Kernel.fatal "Cannot find field %s in %s"
- f.fname (compFullName f.fcomp)
- | f' :: _ when f' == f -> i
- | _ :: rest -> indexOf (i + 1) rest
- in
- let index = indexOf 0 (Extlib.opt_conv [] f.fcomp.cfields) in
- let ci'_fields = Extlib.opt_conv [] ci'.cfields in
- if List.length ci'_fields <= index then
- Kernel.fatal "Too few fields in replacement %s for %s"
- (compFullName ci')
- (compFullName f.fcomp);
- Some (List.nth ci'_fields index)
- end
- end
+ if f.fcomp.creferenced then None
+ else begin
+ match
+ PlainMerging.findReplacement true sEq !currentFidx f.fcomp.cname
+ with
+ None -> None (* We did not replace it *)
+ | Some (ci', _oldfidx) -> begin
+ (* First, find out the index of the original field *)
+ let rec indexOf (i: int) = function
+ | [] -> Kernel.fatal "Cannot find field %s in %s"
+ f.fname (compFullName f.fcomp)
+ | f' :: _ when f' == f -> i
+ | _ :: rest -> indexOf (i + 1) rest
+ in
+ let idx = indexOf 0 (Option.value ~default:[] f.fcomp.cfields) in
+ let ci'_fields = Option.value ~default:[] ci'.cfields in
+ if List.length ci'_fields <= idx then
+ Kernel.fatal "Too few fields in replacement %s for %s"
+ (compFullName ci')
+ (compFullName f.fcomp);
+ Some (List.nth ci'_fields idx)
+ end
+ end
(* The Field offset might need to be changed to use new compinfo *)
method! voffs = function
diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index c14292e68d6440f45b897bd63b7ebeed4973c58d..6dcc4e5f08397848a5b95f113653b468a3c98501 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -460,7 +460,7 @@ class markReachableVisitor
(* to recurse, we must ask explicitly *)
let recurse f = ignore (self#vtype f.ftype) in
- List.iter recurse (Extlib.opt_conv [] c.cfields);
+ List.iter recurse (Option.value ~default:[] c.cfields);
self#visitAttrs attrs;
self#visitAttrs c.cattr
end;
diff --git a/src/kernel_services/analysis/bit_utils.ml b/src/kernel_services/analysis/bit_utils.ml
index 00dab3522f4ca3b7ec19dc14a54e2467f8bf038c..90968aed324a5b1a9921a83277f9666bfcf25ce8 100644
--- a/src/kernel_services/analysis/bit_utils.ml
+++ b/src/kernel_services/analysis/bit_utils.ml
@@ -280,7 +280,7 @@ let rec pretty_bits_internal env bfinfo typ ~align ~start ~stop =
else
acc)
[]
- (Extlib.opt_conv [] compinfo.cfields)
+ (Option.value ~default:[] compinfo.cfields)
in
(** find non covered intervals in structs *)
let non_covered,succ_last =
@@ -303,7 +303,7 @@ let rec pretty_bits_internal env bfinfo typ ~align ~start ~stop =
(s,succ_stop_o)
)
(full_fields_to_print,start)
- (Extlib.opt_conv [] compinfo.cfields)
+ (Option.value ~default:[] compinfo.cfields)
else full_fields_to_print, Integer.zero
in
let overflowing =
@@ -577,7 +577,7 @@ let rec find_offset typ ~offset om =
other fields are too far and we abort. *)
find_field q
in
- find_field (Extlib.opt_conv [] ci.cfields)
+ find_field (Option.value ~default:[] ci.cfields)
| _ -> raise NoMatchingOffset
diff --git a/src/kernel_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml
index 75a648f7aa36a4f9a7269ad8e256d6c58168d68a..77f22868e99db3bb1db048e1eea22873889e7c0e 100644
--- a/src/kernel_services/analysis/exn_flow.ml
+++ b/src/kernel_services/analysis/exn_flow.ml
@@ -444,7 +444,7 @@ class erase_exn =
let s = get_type_tag t in
Kernel.debug ~dkey:Kernel.dkey_exn_flow
"Registering %a as possible exn type" Cil_datatype.Typ.pretty t;
- let fi = List.find (fun fi -> fi.fname = s) (Extlib.the union.cfields) in
+ let fi = List.find (fun fi -> fi.fname = s) (Option.get union.cfields) in
Cil_datatype.Typ.Hashtbl.add exn_union t fi
in
Cil_datatype.Typ.Set.iter update_one_binding exns
@@ -454,7 +454,7 @@ class erase_exn =
method private is_thrown t = Cil_datatype.Typ.Hashtbl.mem exn_enum t
method private exn_field_off name =
- List.find (fun fi -> fi.fname = name) (Extlib.(the (the exn_struct).cfields))
+ 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)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 97baf6af68309a830ae5b596ad15400196df425f..6241cb1906b5a728f3dac7de202915cb6bd79758 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1723,7 +1723,7 @@ class cil_printer () = object (self)
self#attributes sto_mod
self#varname n
(Pretty_utils.pp_list ~sep:"@\n" self#fieldinfo)
- (Extlib.opt_conv [] comp.cfields)
+ (Option.value ~default:[] comp.cfields)
self#attributes rest_attr
| GCompTagDecl (comp, l) -> (* This is a declaration of a tag *)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 775a169db92f5db4bd0a68d8a8be6b92976b2d79..235cae0af2ea4a88bdd6c7fc39f72dd61242d94a 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -450,7 +450,7 @@ let typeHasAttributeMemoryBlock a (ty:typ): bool =
| TComp (comp, _, a') -> f a';
List.iter
(fun fi -> f fi.fattr; visit fi.ftype)
- (Extlib.opt_conv [] comp.cfields)
+ (Option.value ~default:[] comp.cfields)
| TVoid a'
| TInt (_, a')
| TFloat (_, a')
@@ -2848,7 +2848,7 @@ let visitCilFieldInfo vis f =
doVisitCil vis (Visitor_behavior.Memo.fieldinfo vis#behavior) vis#vfieldinfo childrenFieldInfo f
let childrenCompInfo vis comp =
- comp.cfields <- Extlib.opt_map (mapNoCopy (visitCilFieldInfo vis)) comp.cfields;
+ comp.cfields <- Option.map (mapNoCopy (visitCilFieldInfo vis)) comp.cfields;
comp.cattr <- visitCilAttributes vis comp.cattr;
comp
@@ -4032,7 +4032,7 @@ let rec bytesAlignOf t =
| f :: rest -> f :: dropZeros (f.fbitfield <> None) rest
| [] -> []
in
- let fields = dropZeros false (Extlib.opt_conv [] c.cfields) in
+ let fields = dropZeros false (Option.value ~default:[] c.cfields) in
List.fold_left
(fun sofar f ->
(* Bitfields with zero width do not contribute to the alignment in
@@ -4355,7 +4355,7 @@ and bitsSizeOf t =
let lastoff =
fold_struct_fields
(fun ~last acc fi -> offsetOfFieldAcc ~last ~fi ~sofar:acc)
- startAcc (Extlib.the comp.cfields) (* Note: we treat None above *)
+ startAcc (Option.get comp.cfields) (* Note: we treat None above *)
in
if msvcMode () && lastoff.oaFirstFree = 0
then
@@ -4377,13 +4377,13 @@ and bitsSizeOf t =
oaPrevBitPack = None;
} in
let fold acc fi =
- let lastoff = offsetOfFieldAcc ?last:None ~fi ~sofar:startAcc in
- if lastoff.oaFirstFree > acc
- then lastoff.oaFirstFree
- else acc
+ let lastoff = offsetOfFieldAcc ?last:None ~fi ~sofar:startAcc in
+ if lastoff.oaFirstFree > acc
+ then lastoff.oaFirstFree
+ else acc
in
- (* Note: we treat None above *)
- let max = List.fold_left fold 0 (Extlib.the comp.cfields) in
+ (* Note: we treat None above *)
+ let max = List.fold_left fold 0 (Option.get comp.cfields) in
(* Add trailing by simulating adding an extra field *)
addTrailing max (8 * bytesAlignOf t))
@@ -4453,7 +4453,7 @@ and fieldBitsOffset (f : fieldinfo) : int * int =
oaLastFieldStart = 0;
oaLastFieldWidth = 0;
oaPrevBitPack = None }
- (Extlib.opt_conv [] f.fcomp.cfields)
+ (Option.value ~default:[] f.fcomp.cfields)
);
end;
Extlib.the f.foffset_in_bits, Extlib.the f.fsize_in_bits
@@ -5751,7 +5751,9 @@ let isIntegerConstant e =
e
let getCompField cinfo fieldName =
- List.find (fun fi -> fi.fname = fieldName) (Extlib.opt_conv [] cinfo.cfields)
+ List.find
+ (fun fi -> fi.fname = fieldName)
+ (Option.value ~default:[] cinfo.cfields)
let mkCastT ?(force=false) ~(e: exp) ~(oldt: typ) ~(newt: typ) =
let loc = e.eloc in
@@ -5925,7 +5927,7 @@ let existsType (f: typ -> existsAction) (t: typ) : bool =
false
else begin
Hashtbl.add memo c.ckey ();
- List.exists (fun f -> loop f.ftype) (Extlib.opt_conv [] c.cfields)
+ List.exists (fun f -> loop f.ftype) (Option.value ~default:[] c.cfields)
end
in
loop t
@@ -5977,7 +5979,7 @@ let rec makeZeroInit ~loc (t: typ) : init =
(Field(f, NoOffset), makeZeroInit ~loc f.ftype) :: acc
else
acc)
- (Extlib.opt_conv [] comp.cfields) []
+ (Option.value ~default:[] comp.cfields) []
in
CompoundInit (t', inits)
| TComp (comp, _, _) when not comp.cstruct ->
diff --git a/src/kernel_services/ast_queries/cil_const.ml b/src/kernel_services/ast_queries/cil_const.ml
index 06e92efec1a6c9ea40cf55407e1b733b2e8c36c0..ebd6fe21fa6b1402e5d6d68aa137c4440e217347 100644
--- a/src/kernel_services/ast_queries/cil_const.ml
+++ b/src/kernel_services/ast_queries/cil_const.ml
@@ -117,7 +117,7 @@ let mkCompInfo
}
in
let flds =
- Extlib.opt_map (List.mapi (fun forder (fn, ft, fb, fa, fl) ->
+ Option.map (List.mapi (fun forder (fn, ft, fb, fa, fl) ->
{ fcomp = comp;
forder;
ftype = ft;
@@ -140,7 +140,7 @@ let copyCompInfo ?(fresh=true) ci cname =
let ci' = { ci with cname; ckey } in
(* Copy the fields and set the new pointers to parents *)
ci'.cfields <-
- Extlib.opt_map (List.map (fun f -> {f with fcomp = ci'})) ci'.cfields;
+ Option.map (List.map (fun f -> {f with fcomp = ci'})) ci'.cfields;
ci'
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index 198f3a6156f4447a9b8512e94d74b4fa3da9b144..529ae80e7999aca4ff5b50c4cfdf4e9e40b14bbc 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -899,7 +899,7 @@ module Base_checker = struct
~dkey:Kernel.dkey_check "Adding fields for type %s(%d)" c.cname c.ckey;
List.iter
(fun x -> Fieldinfo.Hashtbl.add known_fields x x)
- (Extlib.opt_conv [] c.cfields);
+ (Option.value ~default:[] c.cfields);
Cil.DoChildren
method! vfieldinfo f =
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 01b63d0f99208a8533b7657117aa6219a866177a..09f5fbfa178eb6f96ac39785b861d7c39f3bf0ef 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -798,7 +798,9 @@ struct
with Not_found ->
(match Cil.unrollType ty with
| TComp(comp,_,_) ->
- List.exists (fun x -> x.fname = f) (Extlib.opt_conv [] comp.cfields)
+ List.exists
+ (fun x -> x.fname = f)
+ (Option.value ~default:[] comp.cfields)
| _ -> false)
let plain_type_of_c_field loc f ty =
diff --git a/src/kernel_services/visitors/visitor_behavior.ml b/src/kernel_services/visitors/visitor_behavior.ml
index 0629c08802ec3e85a0e65eb33d314fe569c0c75e..3b8cc057eae61061ba8188c6d4cf1e54f7528541 100644
--- a/src/kernel_services/visitors/visitor_behavior.ml
+++ b/src/kernel_services/visitors/visitor_behavior.ml
@@ -531,14 +531,14 @@ let copy_visit_gen fresh prj =
Cil_datatype.Compinfo.Hashtbl.remove compinfos c;
List.iter
(fun f -> Cil_datatype.Fieldinfo.Hashtbl.remove fieldinfos f)
- (Extlib.opt_conv [] c.cfields)
+ (Option.value ~default:[] c.cfields)
in
let temp_unset_orig_compinfo new_c =
Cil_datatype.Compinfo.Hashtbl.remove orig_compinfos new_c;
List.iter
(fun new_f ->
Cil_datatype.Fieldinfo.Hashtbl.remove orig_fieldinfos new_f)
- (Extlib.opt_conv [] new_c.cfields)
+ (Option.value ~default:[] new_c.cfields)
in
let temp_memo_compinfo c =
try Cil_datatype.Compinfo.Hashtbl.find compinfos c
diff --git a/src/plugins/aorai/utils_parser.ml b/src/plugins/aorai/utils_parser.ml
index 7e0ff63e47b7164ca243af6b800359f9f93771d3..53c7e6e52b2cc4957c5f95c08b361a69bf52efc5 100644
--- a/src/plugins/aorai/utils_parser.ml
+++ b/src/plugins/aorai/utils_parser.ml
@@ -75,7 +75,7 @@ let get_new_offset my_host my_offset name=
mc
end
in
- let cfiels = Extlib.opt_conv [] my_comp.Cil_types.cfields in
+ let cfiels = Option.value ~default:[] my_comp.Cil_types.cfields in
let field_info = get_field_info_from_name cfiels name in
Cil_types.Field(field_info,Cil_types.NoOffset)
diff --git a/src/plugins/instantiate/basic_blocks.ml b/src/plugins/instantiate/basic_blocks.ml
index d652f0b11d7f876b5fb1fda817450133c15d48ea..87f9f09c8791f66d593e0ea00dc3f892978f25c5 100644
--- a/src/plugins/instantiate/basic_blocks.ml
+++ b/src/plugins/instantiate/basic_blocks.ml
@@ -257,7 +257,7 @@ and pall_fields_pred ?loc ?(flex_mem_len=None) depth t1 ci pred =
| [ x ] -> [ eq flex_mem_len x ]
| x :: l -> let x' = eq None x in x' :: (eqs_fields l)
in
- pands (eqs_fields (Extlib.the ci.cfields))
+ pands (eqs_fields (Option.get ci.cfields))
let punfold_flexible_struct_pred ?loc the_struct bytes_len pred =
let struct_len = tinteger ?loc (sizeof the_struct.term_type) in
@@ -265,7 +265,7 @@ let punfold_flexible_struct_pred ?loc the_struct bytes_len pred =
| Ctype(TComp(ci, _, _) as t) when Cil.has_flexible_array_member t -> ci
| _ -> Options.fatal "Unfolding flexible on a non flexible structure"
in
- let flex_type = Ctype (Extlib.(last (the ci.cfields))).ftype in
+ let flex_type = Ctype (Extlib.last (Option.get ci.cfields)).ftype in
let flex_len = tminus bytes_len struct_len in
let pall_fields_pred len =
pall_fields_pred ?loc ~flex_mem_len:(Some len) 0 the_struct ci pred
diff --git a/src/plugins/instantiate/stdlib/basic_alloc.ml b/src/plugins/instantiate/stdlib/basic_alloc.ml
index afd085e51aa6fb9400c3a25e97e7d08850520075..f2d749c5442aac162cd5325a85374f66f6a313c5 100644
--- a/src/plugins/instantiate/stdlib/basic_alloc.ml
+++ b/src/plugins/instantiate/stdlib/basic_alloc.ml
@@ -30,7 +30,7 @@ let unexpected = Options.fatal "Stdlib.Basic_alloc: unexpected: %s"
let valid_size ?loc typ size =
let p = match typ with
| TComp (ci, _, _) when Cil.has_flexible_array_member typ ->
- let elem = match (last (opt_conv [] ci.cfields)).ftype with
+ let elem = match (last (Option.value ~default:[] ci.cfields)).ftype with
| TArray(t, _ , _, _) -> tinteger ?loc (Cil.bytesSizeOf t)
| _ -> unexpected "non array last field on flexible structure"
in
diff --git a/src/plugins/rte/rte.ml b/src/plugins/rte/rte.ml
index 8119e56ad1eb2e2c3a6c0d7183d412fa45fdec4d..944641396554ae6394b8268d968003438723ca44 100644
--- a/src/plugins/rte/rte.ml
+++ b/src/plugins/rte/rte.ml
@@ -119,7 +119,7 @@ let lval_initialized_assertion ~remove_trivial:_ ~on_alarm lv =
let llv =
List.map
(fun fi -> Cil.addOffsetLval (Field (fi, NoOffset)) lv)
- (Extlib.the cfields)
+ (Option.get cfields)
in
if default then
on_alarm ~invalid:false (Alarms.Uninitialized_union llv))
diff --git a/src/plugins/sparecode/globs.ml b/src/plugins/sparecode/globs.ml
index 595c5a51b729c045584974d53f1c93b4dcd16f7e..60b2535c517afc6887b362d762c5df1d9ad0dab6 100644
--- a/src/plugins/sparecode/globs.ml
+++ b/src/plugins/sparecode/globs.ml
@@ -70,7 +70,7 @@ class collect_visitor = object (self)
Hashtbl.add used_compinfo ci.cname ();
List.iter
(fun f -> ignore (visitCilType (self:>Cil.cilVisitor) f.ftype))
- (Extlib.opt_conv [] ci.cfields);
+ (Option.value ~default:[] ci.cfields);
DoChildren
end
| _ -> DoChildren
diff --git a/src/plugins/value/domains/cvalue/builtins_memory.ml b/src/plugins/value/domains/cvalue/builtins_memory.ml
index fd86744961bb4938299113c0392722e82d5417b2..22c01f6f083c0675b99abd6a74e30aa0aa7b572b 100644
--- a/src/plugins/value/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/value/domains/cvalue/builtins_memory.ml
@@ -475,10 +475,10 @@ let memset_typ_offsm_int full_typ i =
let offset_fi = Int.of_int (fst (Cil.fieldBitsOffset fi)) in
aux fi.ftype (Int.add offset offset_fi) offsm
in
- List.fold_left aux_field offsm (Extlib.opt_conv [] l)
+ List.fold_left aux_field offsm (Option.value ~default:[] l)
| TComp ({ cstruct = false ; cfields = l}, _, _) -> (* union *)
(* Use only the first field. This is somewhat arbitrary *)
- aux (List.hd (Extlib.the l)).ftype offset offsm
+ aux (List.hd (Option.get l)).ftype offset offsm
| TArray (typelt, nb, _, _) -> begin
let nb = Cil.lenOfArray64 nb in (* always succeeds, we computed the
size of the entire type earlier *)
diff --git a/src/plugins/value/domains/cvalue/cvalue_init.ml b/src/plugins/value/domains/cvalue/cvalue_init.ml
index 2266554ce9472355f88ba022459f0363942523f4..063a3ce6fe184d81897d5e9c5a70179699cd4c7c 100644
--- a/src/plugins/value/domains/cvalue/cvalue_init.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_init.ml
@@ -313,7 +313,8 @@ let initialize_var_using_type varinfo state =
in
begin
try
- List.fold_left treat_field state (Extlib.opt_conv [] compinfo.cfields)
+ List.fold_left treat_field state
+ (Option.value ~default:[] compinfo.cfields)
with Cil.SizeOfError (s, t) ->
warn_unknown_size varinfo (s, t);
bind_entire_loc Cvalue.V.top_int;
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index 1543c507fa238cdcd447d177e7a129393019e0fb..481131e2920ffc91547167ebabe1604ca60f866a 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -193,7 +193,7 @@ module V = struct
if o = NoOffset then
let o' = match Cil.unrollType typ_base with
| TArray _ -> Index (Cil.(zero Cil_builtins.builtinLoc), NoOffset)
- | TComp (ci, _, _) -> Field (List.hd (Extlib.the ci.cfields), NoOffset)
+ | TComp (ci, _, _) -> Field (List.hd (Option.get ci.cfields), NoOffset)
| _ -> raise Bit_utils.NoMatchingOffset
in o', ok
else o, ok
diff --git a/src/plugins/wp/CodeSemantics.ml b/src/plugins/wp/CodeSemantics.ml
index 560e934200a025309fc347483582dcb87e6c97e8..36c2c41941d5480a32e165033d1ded317bfc9c84 100644
--- a/src/plugins/wp/CodeSemantics.ml
+++ b/src/plugins/wp/CodeSemantics.ml
@@ -96,7 +96,7 @@ struct
| C_comp c ->
p_all
(fun f -> is_zero sigma (Ctypes.object_of f.ftype) (M.field l f))
- (Extlib.the c.cfields)
+ (Option.get c.cfields)
| C_array a ->
(*TODO[LC] make zero-initializers model-dependent.
For instance, a[N][M] becomes a[N*M] in MemTyped,
@@ -484,8 +484,9 @@ struct
let ct = constfold_ctyp ct in
let acc = (* updated acc with default init of structure *)
match ct with
- | TComp (cp,_,_) when cp.cstruct && (* not for union... *)
- (List.length initl) < (List.length (Extlib.the cp.cfields)) ->
+ | TComp (cp,_,_)
+ when cp.cstruct && (* not for union... *)
+ (List.length initl) < (List.length (Option.get cp.cfields)) ->
(* default init for unintialized field of a struct *)
List.fold_left
(fun acc f ->
@@ -501,7 +502,7 @@ struct
(Cil.addOffsetLval (Field(f, NoOffset)) lv)
f.ftype None in
init :: acc)
- acc (List.rev (Extlib.the cp.cfields))
+ acc (List.rev (Option.get cp.cfields))
| _ -> acc
in
diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index 03a39afbea4010899be8c7d32a35e43c6d5c8ef1..70c87ca9aa4e385694a0628d3da224435f9b5f3b 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -77,7 +77,7 @@ let rec init_value value obj =
let make_term f =
Cfield (f, KInit), init_value value (object_of f.ftype)
in
- Lang.F.e_record (List.map make_term (Extlib.the ci.cfields))
+ Lang.F.e_record (List.map make_term (Option.get ci.cfields))
| C_array _ as arr ->
Lang.F.e_const Lang.t_int
(init_value value (object_of_array_elem arr))
@@ -99,7 +99,8 @@ and is_constrained_obj = function
| C_comp c -> is_constrained_comp c
and is_constrained_comp c =
- List.exists (fun f -> is_constrained f.ftype) (Extlib.opt_conv [] c.cfields)
+ List.exists
+ (fun f -> is_constrained f.ftype) (Option.value ~default:[] c.cfields)
module type CASES =
sig
@@ -160,7 +161,7 @@ struct
let def = p_all
(fun f ->
is_typ f.ftype (e_getfield (e_var s) (Lang.Cfield (f, KValue))))
- (Extlib.the c.cfields)
+ (Option.get c.cfields)
in {
d_lfun = lfun ; d_types = 0 ; d_params = [s] ;
d_cluster = Definitions.compinfo c ;
@@ -351,7 +352,7 @@ module EQCOMP = WpContext.Generator(Cil_datatype.Compinfo)
let fd = Cfield (f, KValue) in
!equal_rec (Ctypes.object_of f.ftype)
(e_getfield ra fd) (e_getfield rb fd))
- (Extlib.the c.cfields)
+ (Option.get c.cfields)
in
(* Registration *)
Definitions.define_symbol {
diff --git a/src/plugins/wp/Definitions.ml b/src/plugins/wp/Definitions.ml
index ea539670355606cb2ecd5bf04686248eeea9991f..848a2763cd6fad973961cb0d0dea1902647dc36c 100644
--- a/src/plugins/wp/Definitions.ml
+++ b/src/plugins/wp/Definitions.ml
@@ -341,7 +341,7 @@ class virtual visitor main =
let t = Lang.tau_of_ctype f.ftype in
self#vtau t ; Cfield (f, KValue) , t
)
- (Extlib.opt_conv [] r.cfields)
+ (Option.value ~default:[] r.cfields)
in self#on_comp r fts ;
end
end
@@ -358,7 +358,7 @@ class virtual visitor main =
let t = Lang.init_of_ctype f.ftype in
self#vtau t ; Cfield (f, KInit) , t
)
- (Extlib.opt_conv [] r.cfields)
+ (Option.value ~default:[] r.cfields)
in self#on_icomp r fts ;
end
end
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 07ca63a4b29c85249428bbdf23f573d0a2eaa739..61a8123ba9d1609fb81a18b3de54a51154c9d124 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -351,7 +351,7 @@ let comp_init c = Comp (c, KInit)
let fields_of_adt = function
| Mrecord(_,r) -> r.fields
| Comp (c, k) ->
- List.map (fun f -> Cfield (f, k)) (Extlib.opt_conv [] c.cfields)
+ List.map (fun f -> Cfield (f, k)) (Option.value ~default:[] c.cfields)
| _ -> []
let fields_of_tau = function
@@ -362,7 +362,7 @@ let fields_of_tau = function
let fields_of_field = function
| Mfield(_,r,_,_) -> r.fields
| Cfield(f, k) ->
- List.map (fun f -> Cfield (f, k)) (Extlib.opt_conv [] f.fcomp.cfields)
+ List.map (fun f -> Cfield (f, k)) (Option.value ~default:[] f.fcomp.cfields)
let tau_of_field = function
| Mfield(_,_,_,t) -> t
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index a6df8a74022d8f6082226d115f3e830b197700cd..dc6972e98f266d05f4a70770725d1dc5e856807a 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -907,7 +907,7 @@ struct
(fun offsets (obj,ofs) ->
(obj , TField(fd,ofs)) :: offsets
) offsets (compound_offsets (Ctypes.object_of fd.ftype))
- ) [] (Extlib.the comp.cfields)
+ ) [] (Option.get comp.cfields)
| obj -> [obj , TNoOffset]
let assignable_lval env ~unfold lv =
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index 0008f2b6dad00fe0255368b6799ed001542a69d4..bb8f6d0e09a110dad4958635da514c1aa3814553 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -199,7 +199,7 @@ struct
(fun f ->
Cfield (f, KValue) ,
!loadrec sigma (object_of f.ftype) (M.field loc f)
- ) (Extlib.the c.cfields) in
+ ) (Option.get c.cfields) in
let dfun = Definitions.Function( result , Def , e_record def ) in
Definitions.define_symbol {
d_lfun = lfun ; d_types = 0 ;
@@ -366,7 +366,7 @@ struct
let params = x :: xms in
let def = p_all
(fun f -> !isinitrec sigma (object_of f.ftype) (M.field loc f))
- (Extlib.the c.cfields)
+ (Option.get c.cfields)
in
Definitions.define_symbol {
d_lfun = lfun ; d_types = 0 ;
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 0a7ea59741b7d92be4b8a21a6269eba54c3a7846..08949ff05717487acd1296a3e370890a0ad6dfb9 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -204,7 +204,7 @@ and footprint_comp c =
List.fold_left
(fun ft f ->
Heap.Set.union ft (footprint (object_of f.ftype))
- ) Heap.Set.empty (Extlib.opt_conv [] c.cfields)
+ ) Heap.Set.empty (Option.value ~default:[] c.cfields)
let init_footprint _ _ = Heap.Set.singleton T_init
let value_footprint obj _l = footprint obj
@@ -227,7 +227,7 @@ and length_of_comp c =
(* union field are considered as struct field *)
List.fold_left
(fun s f -> s + length_of_field f)
- 0 (Extlib.opt_conv [] c.cfields)
+ 0 (Option.value ~default:[] c.cfields)
let position_of_field f =
let rec fnext k f = function
@@ -235,7 +235,7 @@ let position_of_field f =
| g::gs ->
if Fieldinfo.equal f g then k
else fnext (k + length_of_field g) f gs
- in fnext 0 f (Extlib.the f.fcomp.cfields)
+ in fnext 0 f (Option.get f.fcomp.cfields)
(* -------------------------------------------------------------------------- *)
(* --- Utilities on loc-as-term --- *)
@@ -719,7 +719,7 @@ struct
let clayout (c: Cil_types.compinfo) : layout =
let flayout w f = rlayout w (Ctypes.object_of f.ftype) in
- List.fold_left flayout [] (List.rev (Extlib.the c.cfields))
+ List.fold_left flayout [] (List.rev (Option.get c.cfields))
type comparison = Srem of layout | Drem of layout | Equal | Mismatch
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 076fd8e2ac3e393ef3b38be56828b6e818fe8582..c60e2a82eee11322c42324eaf1b876b643da9230 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -903,7 +903,7 @@ struct
| OBJ , _ , [Shift(te,k)] -> Some(te,k,obj)
| OBJ , C_comp c , (Field fd :: ofs) ->
begin
- match List.rev (Extlib.the c.cfields) with
+ match List.rev (Option.get c.cfields) with
| fd0::_ when Fieldinfo.equal fd fd0 ->
last_field_shift acs (Ctypes.object_of fd.ftype) ofs
| _ -> None
@@ -1055,7 +1055,7 @@ struct
let ofs = ofs @ [Field f] in
initialized_loc sigma obj x ofs
in
- Lang.F.p_conj (List.map mk_pred (Extlib.the ci.cfields))
+ Lang.F.p_conj (List.map mk_pred (Option.get ci.cfields))
and initialized_range sigma obj x ofs low up =
match obj with
@@ -1140,7 +1140,7 @@ struct
F.p_all
(fun fd ->
forall_pointers phi (e_getfield v (Cfield (fd, KValue))) fd.ftype)
- (Extlib.the cfields)
+ (Option.get cfields)
| TArray(elt,_,_,_) ->
let k = Lang.freshvar Qed.Logic.Int in
F.p_forall [k] (forall_pointers phi (e_get v (e_var k)) elt)
@@ -1250,7 +1250,7 @@ struct
let bg = e_getfield b cg in
let eqg = p_forall ys (p_equal ag bg) in
eqg :: hs
- ) hs (Extlib.the f.fcomp.cfields)
+ ) hs (Option.get f.fcomp.cfields)
| Shift(_,e) :: ofs ->
let y = Lang.freshvar ~basename:"k" Qed.Logic.Int in
@@ -1327,7 +1327,7 @@ struct
let ofs = ofs @ [Field f] in
monotonic_initialized seq obj x ofs
in
- Lang.F.p_conj (List.map mk_pred (Extlib.the ci.cfields))
+ Lang.F.p_conj (List.map mk_pred (Option.get ci.cfields))
let memvar_assigned seq obj loc v =
match loc with
diff --git a/src/plugins/wp/RegionAnnot.ml b/src/plugins/wp/RegionAnnot.ml
index 85aa4c281f65656b4c428f8b0f849ac884c2ea4b..be730458b9400c78cadd4909d418eca344333099 100644
--- a/src/plugins/wp/RegionAnnot.ml
+++ b/src/plugins/wp/RegionAnnot.ml
@@ -270,7 +270,7 @@ let parse_varinfo env ~loc x =
error env ~loc "Unknown variable (or region) '%s'" x
let parse_fieldinfo env ~loc comp f =
- try List.find (fun fd -> fd.fname = f) (Extlib.opt_conv [] comp.cfields)
+ try List.find (fun fd -> fd.fname = f) (Option.value ~default:[] comp.cfields)
with Not_found ->
error env ~loc "No field '%s' in compound type '%s'" f comp.cname
@@ -382,17 +382,26 @@ let rec parse_lpath env e =
let comp =
if Compinfo.equal fa.fcomp fb.fcomp then fa.fcomp
else error env ~loc "Range of fields from incompatible types" in
- let fields = field_range ~inside:false fa fb (Extlib.opt_conv [] comp.cfields) in
+ let fields =
+ field_range ~inside:false fa fb
+ (Option.value ~default:[] comp.cfields)
+ in
let ltype = typeof_fields fields in
{ loc ; lnode = L_field(p,fields) ; ltype }
| PLrange( Some a , None ) ->
let p,fd = parse_fpath env a in
- let fields = field_range ~inside:false fd fd (Extlib.opt_conv [] fd.fcomp.cfields) in
+ let fields =
+ field_range ~inside:false fd fd
+ (Option.value ~default:[] fd.fcomp.cfields)
+ in
let ltype = typeof_fields fields in
{ loc ; lnode = L_field(p,fields) ; ltype }
| PLrange( None , Some a ) ->
let p,fd = parse_fpath env a in
- let fields = field_range ~inside:true fd fd (Extlib.opt_conv [] fd.fcomp.cfields) in
+ let fields =
+ field_range ~inside:true fd fd
+ (Option.value ~default:[] fd.fcomp.cfields)
+ in
let ltype = typeof_fields fields in
{ loc ; lnode = L_field(p,fields) ; ltype }
| _ ->
diff --git a/tests/misc/exception.ml b/tests/misc/exception.ml
index 34b7ec283c7b0d2841fadfda5945a33cf34bc4f9..83d0a204e5ece3883c436f054be6f6f4793e8871 100644
--- a/tests/misc/exception.ml
+++ b/tests/misc/exception.ml
@@ -35,7 +35,7 @@ let add_my_exn my_exn f =
let init =
CompoundInit(
exn_type,
- [Field(List.hd (Extlib.the my_exn.cfields), NoOffset), SingleInit (Cil.zero ~loc)])
+ [Field(List.hd (Option.get my_exn.cfields), NoOffset), SingleInit (Cil.zero ~loc)])
in
add_throw_test f exn_type c init
@@ -61,8 +61,8 @@ let add_int_ptr_exn glob f =
let add_catch my_exn my_exn2 f =
let exn_type = TComp(my_exn, { scache = Not_Computed }, []) in
let exn_type2 = TComp(my_exn2, {scache = Not_Computed }, []) in
- let exn_field = Field (List.hd (Extlib.the my_exn.cfields), NoOffset) in
- let exn2_field = Field (List.hd (Extlib.the my_exn2.cfields), NoOffset) in
+ let exn_field = Field (List.hd (Option.get my_exn.cfields), NoOffset) in
+ let exn2_field = Field (List.hd (Option.get my_exn2.cfields), NoOffset) in
let loc = Cil_datatype.Location.unknown in
let real_locals = f.sbody.blocals in
let v1 = Cil.makeLocalVar f "exn" exn_type in
diff --git a/tests/syntax/ghost_cv_var_decl.ml b/tests/syntax/ghost_cv_var_decl.ml
index 96b29cd949e17fb157c2ae4a29fb6d84d37a71df..7d60ff48a6af560db9cd0ab88973b7b2ebfc090a 100644
--- a/tests/syntax/ghost_cv_var_decl.ml
+++ b/tests/syntax/ghost_cv_var_decl.ml
@@ -47,7 +47,7 @@ and comp_ghost_status fmt lval =
match Cil.typeOfLval lval with
| TComp({ cfields }, _, _) ->
Format.fprintf fmt "{ " ;
- List.iter (field_ghost_status fmt lval) (Extlib.opt_conv [] cfields) ;
+ List.iter (field_ghost_status fmt lval) (Option.value ~default:[] cfields) ;
Format.fprintf fmt " }"
| _ -> assert false
and field_ghost_status fmt lval f =