diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 70ab53fe7e64e87ae9e68af4df2a8308145dcbdc..1dd8631d176925dbf526f2aa60251243f86b340c 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -688,10 +688,10 @@ let isTransparentUnion (t: typ) : fieldinfo option =
(* Turn transparent unions into the type of their first field *)
if typeHasAttribute "transparent_union" t then begin
match comp.cfields with
- | [] ->
+ | Some [] | None ->
abort_context
"Empty transparent union: %s" (compFullName comp)
- | f :: _ -> Some f
+ | Some (f :: _) -> Some f
end else
None
| _ -> None
@@ -3342,7 +3342,7 @@ let rec setOneInit this o preinit =
| f' :: _ when f'.fname = f.fname -> idx
| _ :: restf -> loop (idx + 1) restf
in
- loop 0 f.fcomp.cfields, off
+ loop 0 (Extlib.opt_conv [] f.fcomp.cfields), off
| _ -> abort_context "setOneInit: non-constant index"
in
let pMaxIdx, pArray =
@@ -3519,7 +3519,7 @@ 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 comp.cfields in
+ let init, reads = collect 0 reads (Extlib.opt_conv [] comp.cfields) in
CompoundInit (thistype, init), thistype, reads
| TComp (comp, _, _), CompoundPre (pMaxIdx, pArray) when not comp.cstruct ->
@@ -3543,7 +3543,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 comp.cfields in
+ let init, reads = findField 0 (Extlib.opt_conv [] comp.cfields) in
CompoundInit (thistype, [ init ]), thistype, reads
| _ -> Kernel.fatal ~current:true "collectInitializer"
@@ -3684,7 +3684,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 comp.cfields acc
+ add_fields offset in_union (Extlib.opt_conv [] comp.cfields) acc
and add_fields (offset : offset) (in_union : bool) (l : fieldinfo list) acc =
match l with
| [] -> acc
@@ -3744,7 +3744,7 @@ 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 ci.cfields in Field(fid,off)
+ (try let off = search (Extlib.the 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 +3755,7 @@ let find_field_offset cond (fidlist: fieldinfo list) : offset =
let findField n comp =
try
- find_field_offset (fun x -> x.fname = n) comp.cfields
+ find_field_offset (fun x -> x.fname = n) (Extlib.the comp.cfields)
with Not_found ->
abort_context "Cannot find field %s in type %s" n (Cil.compFullName comp)
@@ -5500,7 +5500,9 @@ and makeCompType ghost (isstruct: bool)
(if comp.cstruct then "struct" else "union")
comp.cname;
end else
- List.iter (fun f -> is_circular f.ftype) comp'.cfields;
+ List.iter
+ (fun f -> is_circular f.ftype)
+ (Extlib.opt_conv [] comp'.cfields);
| _ -> ()
in
is_circular ftype;
@@ -5543,30 +5545,30 @@ and makeCompType ghost (isstruct: bool)
if f.fname <> "" then Hashtbl.add fld_table f.fname f
in
List.iter check flds;
- if comp.cfields <> [] then begin
+ if comp.cfields <> Some [] && comp.cfields <> None then begin
(* This appears to be a multiply defined structure. This can happen from
* a construct like "typedef struct foo { ... } A, B;". This is dangerous
* because at the time B is processed some forward references in { ... }
* appear as backward references, which could lead to circularity in
* the type structure. We do a thorough check and then we reuse the type
* for A *)
- if List.length comp.cfields <> List.length flds
+ if List.length (Extlib.opt_conv [] comp.cfields) <> List.length flds
|| (List.exists2 (fun f1 f2 -> not (Cil_datatype.Typ.equal f1.ftype f2.ftype))
- comp.cfields flds)
+ (Extlib.opt_conv [] comp.cfields) flds)
then
Kernel.error ~once:true ~current:true
"%s seems to be multiply defined" (compFullName comp)
end else
begin
- comp.cfields <- flds;
+ comp.cfields <- Some flds;
let fields_with_pragma_attrs =
List.map (fun fld ->
(* note: in the call below, we CANNOT use fld.fcomp.cattr because it has not
been filled in yet, so we need to pass the list of attributes [a] to it *)
{fld with fattr = (process_pragmas_pack_align_field_attributes fld fld.fattr a)}
- ) comp.cfields
+ ) flds
in
- comp.cfields <- fields_with_pragma_attrs
+ comp.cfields <- Some fields_with_pragma_attrs
end;
(* ignore (E.log "makeComp: %s: %a\n" comp.cname d_attrlist a); *)
@@ -8323,7 +8325,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
[(A.NEXT_INIT, A.SINGLE_INIT oneinit)]
else
(* If this is a GNU extension with field-to-union cast find the field *)
- let fi = findField ci.cfields in
+ let fi = findField (Extlib.the ci.cfields) in
(* Change the designator and redo *)
doInit
local_env asconst add_implicit_ensures preinit so acc
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index ef0d0d96c0390db868e258835bb64e7d59cdf16a..2dc0f65e9996dea5e056cd427f04f108fb16ae12 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 oldci.cfields in
- let len = List.length ci.cfields in
+ let old_len = List.length (Extlib.opt_conv [] oldci.cfields) in
+ let len = List.length (Extlib.opt_conv [] 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
@@ -1249,18 +1249,23 @@ and matchCompInfo (oldfidx: int) (oldci: compinfo)
[%a] vs [%a]"
pp_attrs attrs pp_attrs oldattrs))
in
- List.iter2
- (fun oldf f ->
- checkFieldsEqualModuloPackedAlign ~mustCheckOffsets f oldf;
- (* Make sure the types are compatible *)
- (* Note: 6.2.7 §1 states that the names of the fields should be the
- same. We do not force this for now, but could do it. *)
- let newtype =
- combineTypes CombineOther oldfidx oldf.ftype fidx f.ftype
- in
- (* Change the type in the representative *)
- oldf.ftype <- newtype)
- oldci.cfields ci.cfields
+ match oldci.cfields, ci.cfields with
+ | None, None -> ()
+ | Some old_flds, Some flds ->
+ List.iter2
+ (fun oldf f ->
+ checkFieldsEqualModuloPackedAlign ~mustCheckOffsets f oldf;
+ (* Make sure the types are compatible *)
+ (* Note: 6.2.7 §1 states that the names of the fields should be the
+ same. We do not force this for now, but could do it. *)
+ let newtype =
+ combineTypes CombineOther oldfidx oldf.ftype fidx f.ftype
+ in
+ (* Change the type in the representative *)
+ oldf.ftype <- newtype)
+ old_flds flds
+ | _ ->
+ Kernel.fatal "unmatching fields lists"
with Failure reason ->
(* Our assumption was wrong. Forget the isomorphism *)
undo ();
@@ -2178,12 +2183,12 @@ class renameVisitorClass =
| f' :: _ when f' == f -> i
| _ :: rest -> indexOf (i + 1) rest
in
- let index = indexOf 0 f.fcomp.cfields in
- if List.length ci'.cfields <= index then
+ let index = indexOf 0 (Extlib.the f.fcomp.cfields) in
+ if List.length (Extlib.the ci'.cfields) <= index then
Kernel.fatal "Too few fields in replacement %s for %s"
(compFullName ci')
(compFullName f.fcomp);
- let f' = List.nth ci'.cfields index in
+ let f' = List.nth (Extlib.the ci'.cfields) index in
ChangeDoChildrenPost (Field (f', o), fun x -> x)
end
end
@@ -2208,12 +2213,12 @@ class renameVisitorClass =
| f' :: _ when f' == f -> i
| _ :: rest -> indexOf (i + 1) rest
in
- let index = indexOf 0 f.fcomp.cfields in
- if List.length ci'.cfields <= index then
+ let index = indexOf 0 (Extlib.the f.fcomp.cfields) in
+ if List.length (Extlib.the ci'.cfields) <= index then
Kernel.fatal "Too few fields in replacement %s for %s"
(compFullName ci')
(compFullName f.fcomp);
- let f' = List.nth ci'.cfields index in
+ let f' = List.nth (Extlib.the ci'.cfields) index in
ChangeDoChildrenPost (TField (f', o), fun x -> x)
end
end
diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index 4a6a6f796373b8d2bcd6893dd2d91e0b52969cfe..c14292e68d6440f45b897bd63b7ebeed4973c58d 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 c.cfields;
+ List.iter recurse (Extlib.opt_conv [] c.cfields);
self#visitAttrs attrs;
self#visitAttrs c.cattr
end;
diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index 226eefc98e5cefef8ab31e32f53547054abacb74..24f2c220f957eda93ddf064291b3cdb0006a8792 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -41,7 +41,7 @@ type validity =
let pretty_validity fmt v =
match v with
| Empty -> Format.fprintf fmt "Empty"
- | Unknown (b,k,e) ->
+ | Unknown (b,k,e) ->
Format.fprintf fmt "Unknown %a/%a/%a"
Int.pretty b (Pretty_utils.pp_opt Int.pretty) k Int.pretty e
| Known (b,e) -> Format.fprintf fmt "Known %a-%a" Int.pretty b Int.pretty e
@@ -128,10 +128,10 @@ let null = Null
let is_null x = match x with Null -> true | _ -> false
-let pretty fmt t =
+let pretty fmt t =
match t with
| String (_, CSString s) -> Format.fprintf fmt "%S" s
- | String (_, CSWstring s) ->
+ | String (_, CSWstring s) ->
Format.fprintf fmt "L\"%s\"" (Escape.escape_wstring s)
| Var (t,_) | Allocated (t,_,_) -> Printer.pp_varinfo fmt t
| CLogic_Var (lvi, _, _) -> Printer.pp_logic_var fmt lvi
@@ -154,8 +154,8 @@ let typeof v =
| Null -> None
| Var (v,_) | Allocated(v,_,_) -> Some (unrollType v.vtype)
-let cstring_bitlength s =
- let u, l =
+let cstring_bitlength s =
+ let u, l =
match s with
| CSString s ->
bitsSizeOf charType, (String.length s)
@@ -200,7 +200,7 @@ let () =
(fun min max ->
(* let mul_CHAR_BIT = Int64.mul (Int64.of_int (bitsSizeOf charType)) in *)
(* the above is what we would like to write but it is too early *)
- let mul_CHAR_BIT = Int.mul Int.eight in
+ let mul_CHAR_BIT = Int.mul Int.eight in
MinValidAbsoluteAddress.set
(mul_CHAR_BIT (Int.of_string min));
MaxValidAbsoluteAddress.set
@@ -257,8 +257,8 @@ let rec final_empty_struct = function
| TComp (compinfo, _, _) ->
begin
match compinfo.cfields with
- | [] -> true
- | l ->
+ | Some [] | None -> true
+ | Some l ->
let last_field = List.(hd (rev l)) in
try Cil.bitsSizeOf last_field.ftype = 0
with Cil.SizeOfError _ -> false
diff --git a/src/kernel_services/analysis/bit_utils.ml b/src/kernel_services/analysis/bit_utils.ml
index 0ed0755ee7f9f646292cc2f0ea738fcbf8f238d4..00dab3522f4ca3b7ec19dc14a54e2467f8bf038c 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)
[]
- compinfo.cfields
+ (Extlib.opt_conv [] 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)
- compinfo.cfields
+ (Extlib.opt_conv [] compinfo.cfields)
else full_fields_to_print, Integer.zero
in
let overflowing =
@@ -462,7 +462,7 @@ type offset_match =
let rec equal_type_no_attribute t1 t2 =
match Cil.unrollType t1, Cil.unrollType t2 with
| TVoid _, TVoid _ -> true
- | TInt (i1, _), TInt (i2, _) -> i1 = i2
+ | TInt (i1, _), TInt (i2, _) -> i1 = i2
| TFloat (f1, _), TFloat (f2, _) -> f1 = f2
| TPtr (t1, _), TPtr (t2, _) -> equal_type_no_attribute t1 t2
| TArray (t1', s1, _, _), TArray (t2', s2, _, _) ->
@@ -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 ci.cfields
+ find_field (Extlib.opt_conv [] ci.cfields)
| _ -> raise NoMatchingOffset
diff --git a/src/kernel_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml
index e6badcad629642c2838b939b21aab3b326d45b45..677f87ff0ebedb2bec588d09e6846781294f17bc 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) union.cfields in
+ let fi = List.find (fun fi -> fi.fname = s) (Extlib.the 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 exn_struct).cfields
+ List.find (fun fi -> fi.fname = name) (Extlib.(the (the 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_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 43e748017dd33a3a93855dee5a8170e58bbf9686..22b936df2af007d27831ed8b7ee91892087755b2 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -365,7 +365,7 @@ and compinfo = {
files might have different keys. Use {!Cil_const.copyCompInfo} to copy
structures so that a new key is assigned. *)
- mutable cfields: fieldinfo list;
+ mutable cfields: fieldinfo list option;
(** Information about the fields. Notice that each fieldinfo has a pointer
back to the host compinfo. This means that you should not share
fieldinfo's between two compinfo's *)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 37364ee028462571d6efdbf3c42cdd033663f577..97baf6af68309a830ae5b596ad15400196df425f 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)
- comp.cfields
+ (Extlib.opt_conv [] comp.cfields)
self#attributes rest_attr
| GCompTagDecl (comp, l) -> (* This is a declaration of a tag *)
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 9ce30a3dac134d87e8e65424eae08e7e4d8f2276..ca470bb9dae30f2615af47d62c163166c1025673 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -207,7 +207,7 @@ and pp_compinfo fmt compinfo =
pp_string compinfo.corig_name
pp_string compinfo.cname
pp_int compinfo.ckey
- (pp_list pp_fieldinfo) compinfo.cfields
+ (pp_option (pp_list pp_fieldinfo)) compinfo.cfields
pp_attributes compinfo.cattr
pp_bool compinfo.cdefined
pp_bool compinfo.creferenced
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index fd327796b0b2d13459f7fabe0f203da3d65ef50a..873a6416b00a568c4a90fcaa5edea81da4f02697 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -441,7 +441,9 @@ let typeHasAttributeMemoryBlock a (ty:typ): bool =
| TNamed (r, a') -> f a' ; visit r.ttype
| TArray(t, _, _, a') -> f a'; visit t
| TComp (comp, _, a') -> f a';
- List.iter (fun fi -> f fi.fattr; visit fi.ftype) comp.cfields
+ List.iter
+ (fun fi -> f fi.fattr; visit fi.ftype)
+ (Extlib.opt_conv [] comp.cfields)
| TVoid a'
| TInt (_, a')
| TFloat (_, a')
@@ -2839,7 +2841,7 @@ let visitCilFieldInfo vis f =
doVisitCil vis (Visitor_behavior.Memo.fieldinfo vis#behavior) vis#vfieldinfo childrenFieldInfo f
let childrenCompInfo vis comp =
- comp.cfields <- mapNoCopy (visitCilFieldInfo vis) comp.cfields;
+ comp.cfields <- Extlib.opt_map (mapNoCopy (visitCilFieldInfo vis)) comp.cfields;
comp.cattr <- visitCilAttributes vis comp.cattr;
comp
@@ -4023,7 +4025,7 @@ let rec bytesAlignOf t =
| f :: rest -> f :: dropZeros (f.fbitfield <> None) rest
| [] -> []
in
- let fields = dropZeros false c.cfields in
+ let fields = dropZeros false (Extlib.opt_conv [] c.cfields) in
List.fold_left
(fun sofar f ->
(* Bitfields with zero width do not contribute to the alignment in
@@ -4314,7 +4316,7 @@ and bitsSizeOf t =
| TPtr _ -> 8 * theMachine.theMachine.sizeof_ptr
| TBuiltin_va_list _ -> 8 * theMachine.theMachine.sizeof_ptr
| TNamed (t, _) -> bitsSizeOf t.ttype
- | TComp (comp, scache, _) when comp.cfields == [] ->
+ | TComp (comp, scache, _) when comp.cfields = Some [] || comp.cfields = None ->
find_size_in_cache
scache
(fun () -> begin
@@ -4341,9 +4343,10 @@ and bitsSizeOf t =
let lastoff =
fold_struct_fields
(fun ~last acc fi -> offsetOfFieldAcc ~last ~fi ~sofar:acc)
- startAcc comp.cfields
+ startAcc (Extlib.opt_conv [] comp.cfields)
in
- if msvcMode () && lastoff.oaFirstFree = 0 && comp.cfields <> []
+ if msvcMode () && lastoff.oaFirstFree = 0 &&
+ comp.cfields = Some [] && comp.cfields <> None
then
(* On MSVC if we have just a zero-width bitfields then the length
* is 32 and is not padded *)
@@ -4366,7 +4369,7 @@ and bitsSizeOf t =
List.fold_left (fun acc fi ->
let lastoff = offsetOfFieldAcc ?last:None ~fi ~sofar:startAcc in
if lastoff.oaFirstFree > acc then
- lastoff.oaFirstFree else acc) 0 comp.cfields in
+ lastoff.oaFirstFree else acc) 0 (Extlib.opt_conv [] comp.cfields) in
(* Add trailing by simulating adding an extra field *)
addTrailing max (8 * bytesAlignOf t))
@@ -4436,7 +4439,7 @@ and fieldBitsOffset (f : fieldinfo) : int * int =
oaLastFieldStart = 0;
oaLastFieldWidth = 0;
oaPrevBitPack = None }
- f.fcomp.cfields
+ (Extlib.opt_conv [] f.fcomp.cfields)
);
end;
Extlib.the f.foffset_in_bits, Extlib.the f.fsize_in_bits
@@ -5734,7 +5737,7 @@ let isIntegerConstant e =
e
let getCompField cinfo fieldName =
- List.find (fun fi -> fi.fname = fieldName) cinfo.cfields
+ List.find (fun fi -> fi.fname = fieldName) (Extlib.opt_conv [] cinfo.cfields)
let mkCastT ?(force=false) ~(e: exp) ~(oldt: typ) ~(newt: typ) =
let loc = e.eloc in
@@ -5908,7 +5911,7 @@ let existsType (f: typ -> existsAction) (t: typ) : bool =
false
else begin
Hashtbl.add memo c.ckey ();
- List.exists (fun f -> loop f.ftype) c.cfields
+ List.exists (fun f -> loop f.ftype) (Extlib.opt_conv [] c.cfields)
end
in
loop t
@@ -5960,16 +5963,18 @@ let rec makeZeroInit ~loc (t: typ) : init =
(Field(f, NoOffset), makeZeroInit ~loc f.ftype) :: acc
else
acc)
- comp.cfields []
+ (Extlib.opt_conv [] comp.cfields) []
in
CompoundInit (t', inits)
| TComp (comp, _, _) when not comp.cstruct ->
(match comp.cfields with
- | [] -> CompoundInit(t, []) (* tolerate empty initialization. *)
- | f :: _rest ->
+ | Some [] -> CompoundInit(t, []) (* tolerate empty initialization. *)
+ | Some (f :: _rest) ->
(* ISO C99 [6.7.8.10] says that the first field of the union
is the one we should initialize. *)
- CompoundInit(t, [(Field(f, NoOffset), makeZeroInit ~loc f.ftype)]))
+ CompoundInit(t, [(Field(f, NoOffset), makeZeroInit ~loc f.ftype)])
+ | None ->
+ Kernel.fatal "Initialization of incomplete struct")
| TArray(bt, Some len, _, _) as t' ->
let n =
match constFoldToInt len with
@@ -6076,7 +6081,10 @@ let has_flexible_array_member t =
in
match unrollType t with
| TComp (c,_,_) ->
- c.cfields <> [] && is_flexible_array (Extlib.last c.cfields).ftype
+ begin match c.cfields with
+ | Some ((_ :: _) as l) -> is_flexible_array (Extlib.last l).ftype
+ | _ -> false
+ end
| _ -> false
(* last_field is [true] if the given type is the type of the last field of
@@ -6115,7 +6123,9 @@ and complete_type_fields ?allowZeroSizeArrays is_struct fields =
| f :: tl ->
is_complete_agg_member ?allowZeroSizeArrays f.ftype && aux false tl
in
- aux true fields
+ match fields with
+ | None -> false
+ | Some fields -> aux true fields
and is_complete_agg_member ?allowZeroSizeArrays ?last_field t =
isCompleteType ?allowZeroSizeArrays ?last_field t &&
diff --git a/src/kernel_services/ast_queries/cil_const.ml b/src/kernel_services/ast_queries/cil_const.ml
index bd0e72125cdc20b29c46f1215f94da2973e18a77..d7f183431cda082f65b6ac59904563cbe0b3fa3a 100644
--- a/src/kernel_services/ast_queries/cil_const.ml
+++ b/src/kernel_services/ast_queries/cil_const.ml
@@ -110,7 +110,7 @@ let mkCompInfo
corig_name = norig;
cname = n;
ckey = nextCompinfoKey ();
- cfields = []; (* fields will be added afterwards. *)
+ cfields = None; (* fields will be added afterwards. *)
cattr = a;
creferenced = false;
(* Make this compinfo undefined by default *)
@@ -131,7 +131,7 @@ let mkCompInfo
foffset_in_bits = None;
fpadding_in_bits = None;
}) (mkfspec comp) in
- comp.cfields <- flds;
+ comp.cfields <- if flds <> [] then Some flds else None;
if flds <> [] then comp.cdefined <- true;
comp
@@ -140,12 +140,13 @@ let copyCompInfo ?(fresh=true) ci cname =
let ckey = if fresh then nextCompinfoKey () else ci.ckey in
let ci' = { ci with cname; ckey } in
(* Copy the fields and set the new pointers to parents *)
- ci'.cfields <- List.map (fun f -> {f with fcomp = ci'}) ci'.cfields;
+ ci'.cfields <-
+ Extlib.opt_map (List.map (fun f -> {f with fcomp = ci'})) ci'.cfields;
ci'
let make_logic_var_kind x kind typ =
- {lv_name = x; lv_id = new_raw_id(); lv_type = typ; lv_kind = kind;
+ {lv_name = x; lv_id = new_raw_id(); lv_type = typ; lv_kind = kind;
lv_origin = None; lv_attr = [] }
let make_logic_var_global x t = make_logic_var_kind x LVGlobal t
@@ -154,7 +155,7 @@ let make_logic_var_quant x t = make_logic_var_kind x LVQuant t
let make_logic_var_local x t = make_logic_var_kind x LVLocal t
let make_logic_var =
- Kernel.deprecated "Cil_const.make_logic_var"
+ Kernel.deprecated "Cil_const.make_logic_var"
~now:"Use one of Cil_const.make_logic_var_* to indicate \
the origin of the variable"
make_logic_var_quant
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index d1c06925427b28ce3aadaa56485ab24aa1895d3e..5716e4384f54b22ea7c06da9c14478c85cf8f458 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -776,7 +776,7 @@ module Compinfo = struct
corig_name = "";
cname = "";
ckey = -1;
- cfields = [];
+ cfields = None;
cattr = [];
cdefined = false;
creferenced = false } ]
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index 18ad6e32241cc8410cdefaaa9c94e4724dcff09b..198f3a6156f4447a9b8512e94d74b4fa3da9b144 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -897,7 +897,9 @@ module Base_checker = struct
Compinfo.Hashtbl.add known_compinfos c c;
Kernel.debug
~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) c.cfields;
+ List.iter
+ (fun x -> Fieldinfo.Hashtbl.add known_fields x x)
+ (Extlib.opt_conv [] 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 db72d3ac6311cc746a454c6d0dd5598e4c2fb39b..01b63d0f99208a8533b7657117aa6219a866177a 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -798,7 +798,7 @@ struct
with Not_found ->
(match Cil.unrollType ty with
| TComp(comp,_,_) ->
- List.exists (fun x -> x.fname = f) comp.cfields
+ List.exists (fun x -> x.fname = f) (Extlib.opt_conv [] 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 a1798fec152da146f9131751eb1babc993423cdc..0629c08802ec3e85a0e65eb33d314fe569c0c75e 100644
--- a/src/kernel_services/visitors/visitor_behavior.ml
+++ b/src/kernel_services/visitors/visitor_behavior.ml
@@ -506,28 +506,39 @@ let copy_visit_gen fresh prj =
in
let temp_set_compinfo c new_c =
Cil_datatype.Compinfo.Hashtbl.add compinfos c new_c;
- List.iter2
- (fun f new_f -> Cil_datatype.Fieldinfo.Hashtbl.add fieldinfos f new_f)
- c.cfields new_c.cfields
+ match c.cfields, new_c.cfields with
+ | None, None -> ()
+ | Some c_flds, Some new_c_flds ->
+ List.iter2
+ (fun f new_f -> Cil_datatype.Fieldinfo.Hashtbl.add fieldinfos f new_f)
+ c_flds new_c_flds
+ | _ ->
+ Kernel.fatal "set_compinfo: structures or unions do not match"
in
let temp_set_orig_compinfo new_c c =
Cil_datatype.Compinfo.Hashtbl.add orig_compinfos new_c c;
- List.iter2
- (fun new_f f ->
- Cil_datatype.Fieldinfo.Hashtbl.add orig_fieldinfos new_f f)
- new_c.cfields c.cfields
+ match new_c.cfields, c.cfields with
+ | None, None -> ()
+ | Some new_c_flds, Some c_flds ->
+ List.iter2
+ (fun new_f f ->
+ Cil_datatype.Fieldinfo.Hashtbl.add orig_fieldinfos new_f f)
+ new_c_flds c_flds
+ | _ ->
+ Kernel.fatal "set_orig_compinfo: structures or unions do not match"
in
let temp_unset_compinfo c =
Cil_datatype.Compinfo.Hashtbl.remove compinfos c;
List.iter
- (fun f -> Cil_datatype.Fieldinfo.Hashtbl.remove fieldinfos f) c.cfields
+ (fun f -> Cil_datatype.Fieldinfo.Hashtbl.remove fieldinfos f)
+ (Extlib.opt_conv [] 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)
- new_c.cfields
+ (Extlib.opt_conv [] 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 0b45abd1249bf2903f1642eca21e6afb0945d75d..7e0ff63e47b7164ca243af6b800359f9f93771d3 100644
--- a/src/plugins/aorai/utils_parser.ml
+++ b/src/plugins/aorai/utils_parser.ml
@@ -75,8 +75,8 @@ let get_new_offset my_host my_offset name=
mc
end
in
-
- let field_info = get_field_info_from_name my_comp.Cil_types.cfields name in
+ let cfiels = Extlib.opt_conv [] 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)
| _ -> Aorai_option.fatal "NOT YET IMPLEMENTED : mem is not supported"
diff --git a/src/plugins/instantiate/basic_blocks.ml b/src/plugins/instantiate/basic_blocks.ml
index 744917afbad2aef97acbe6cf1e75c29ba33873a0..d652f0b11d7f876b5fb1fda817450133c15d48ea 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 ci.cfields)
+ pands (eqs_fields (Extlib.the 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 ci.cfields).ftype in
+ let flex_type = Ctype (Extlib.(last (the 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 0faa0e41124ff41340e4db42bac30e685cf54c43..afd085e51aa6fb9400c3a25e97e7d08850520075 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 ci.cfields).ftype with
+ let elem = match (last (opt_conv [] 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/instantiate/string/memset.ml b/src/plugins/instantiate/string/memset.ml
index 1538ba32be03820bce1499f1dc1d25cdc35be6ff..1ed583fcfb21f8aa01e37a912883cdc7faf2ef92 100644
--- a/src/plugins/instantiate/string/memset.ml
+++ b/src/plugins/instantiate/string/memset.ml
@@ -189,7 +189,7 @@ let rec contains_union_type t =
match Cil.unrollType t with
| TComp({ cstruct = false }, _, _) ->
true
- | TComp({ cfields = fields }, _, _) ->
+ | TComp({ cfields = Some fields }, _, _) ->
List.exists contains_union_type (List.map (fun f -> f.ftype) fields)
| TArray(t, _, _, _) ->
contains_union_type t
diff --git a/src/plugins/rte/rte.ml b/src/plugins/rte/rte.ml
index bc526753f3612bf6fefef2d0bc0c6c752a1437eb..71ea75016fd0d57a198ae1dce2f9283342e69516 100644
--- a/src/plugins/rte/rte.ml
+++ b/src/plugins/rte/rte.ml
@@ -113,13 +113,13 @@ let lval_initialized_assertion ~remove_trivial:_ ~on_alarm lv =
match typ with
| TComp({cstruct = false; cfields} ,_,_) ->
(match cfields with
- | [] -> () (* empty union, supported by gcc with size 0.
+ | Some [] | None -> () (* empty union, supported by gcc with size 0.
Trivially initialized. *)
| _ ->
let llv =
List.map
(fun fi -> Cil.addOffsetLval (Field (fi, NoOffset)) lv)
- cfields
+ (Extlib.opt_conv [] 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 f35f478c8800a7a4f78e1bad7c717ff0cc55632e..595c5a51b729c045584974d53f1c93b4dcd16f7e 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))
- ci.cfields;
+ (Extlib.opt_conv [] 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 9f0e325e07c67523804413820be3da68a0b32379..fd86744961bb4938299113c0392722e82d5417b2 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 l
+ List.fold_left aux_field offsm (Extlib.opt_conv [] l)
| TComp ({ cstruct = false ; cfields = l}, _, _) -> (* union *)
(* Use only the first field. This is somewhat arbitrary *)
- aux (List.hd l).ftype offset offsm
+ aux (List.hd (Extlib.the 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 92786e24562cfbc1d6a0a2d5870e95b98bc88ec7..28b09e3fb964d92c074059990a91fbc9c8afee53 100644
--- a/src/plugins/value/domains/cvalue/cvalue_init.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_init.ml
@@ -98,7 +98,7 @@ let create_hidden_base ~libc ~valid ~hidden_var_name ~name_desc pointed_typ =
let reject_empty_struct b offset typ =
match Cil.unrollType typ with
| TComp (ci, _, _) ->
- if ci.cfields = [] && ci.cdefined &&
+ if ci.cfields = Some [] && ci.cdefined &&
not (Cil.gccMode () || Cil.msvcMode ()) then
Value_parameters.abort ~current:true
"@[empty %ss@ are unsupported@ (type '%a',@ location %a%a)@ \
@@ -314,7 +314,7 @@ let initialize_var_using_type varinfo state =
in
begin
try
- List.fold_left treat_field state compinfo.cfields
+ List.fold_left treat_field state (Extlib.opt_conv [] 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 de29ab14d029903c2f43518d39f3820082cc6313..1543c507fa238cdcd447d177e7a129393019e0fb 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 ci.cfields, NoOffset)
+ | TComp (ci, _, _) -> Field (List.hd (Extlib.the 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 c4b348892c1c893fafd4c29e2d634e9beb436ce4..560e934200a025309fc347483582dcb87e6c97e8 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))
- c.cfields
+ (Extlib.the c.cfields)
| C_array a ->
(*TODO[LC] make zero-initializers model-dependent.
For instance, a[N][M] becomes a[N*M] in MemTyped,
@@ -485,7 +485,7 @@ struct
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 cp.cfields) ->
+ (List.length initl) < (List.length (Extlib.the cp.cfields)) ->
(* default init for unintialized field of a struct *)
List.fold_left
(fun acc f ->
@@ -501,7 +501,7 @@ struct
(Cil.addOffsetLval (Field(f, NoOffset)) lv)
f.ftype None in
init :: acc)
- acc (List.rev cp.cfields)
+ acc (List.rev (Extlib.the cp.cfields))
| _ -> acc
in
diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index fe1589813a2dd79adf03424c4bc78ba974e942ef..03a39afbea4010899be8c7d32a35e43c6d5c8ef1 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 ci.cfields)
+ Lang.F.e_record (List.map make_term (Extlib.the ci.cfields))
| C_array _ as arr ->
Lang.F.e_const Lang.t_int
(init_value value (object_of_array_elem arr))
@@ -99,7 +99,7 @@ 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) c.cfields
+ List.exists (fun f -> is_constrained f.ftype) (Extlib.opt_conv [] c.cfields)
module type CASES =
sig
@@ -160,7 +160,7 @@ struct
let def = p_all
(fun f ->
is_typ f.ftype (e_getfield (e_var s) (Lang.Cfield (f, KValue))))
- c.cfields
+ (Extlib.the c.cfields)
in {
d_lfun = lfun ; d_types = 0 ; d_params = [s] ;
d_cluster = Definitions.compinfo c ;
@@ -351,7 +351,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))
- c.cfields
+ (Extlib.the c.cfields)
in
(* Registration *)
Definitions.define_symbol {
diff --git a/src/plugins/wp/Definitions.ml b/src/plugins/wp/Definitions.ml
index e265f9dbf24458ebc0182f2867b1d87cb5570022..ea539670355606cb2ecd5bf04686248eeea9991f 100644
--- a/src/plugins/wp/Definitions.ml
+++ b/src/plugins/wp/Definitions.ml
@@ -340,7 +340,8 @@ class virtual visitor main =
(fun f ->
let t = Lang.tau_of_ctype f.ftype in
self#vtau t ; Cfield (f, KValue) , t
- ) r.cfields
+ )
+ (Extlib.opt_conv [] r.cfields)
in self#on_comp r fts ;
end
end
@@ -356,7 +357,8 @@ class virtual visitor main =
(fun f ->
let t = Lang.init_of_ctype f.ftype in
self#vtau t ; Cfield (f, KInit) , t
- ) r.cfields
+ )
+ (Extlib.opt_conv [] 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 bb621655ffed1d216a4862d171fea548cfcfeb29..07ca63a4b29c85249428bbdf23f573d0a2eaa739 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -350,7 +350,8 @@ 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)) c.cfields
+ | Comp (c, k) ->
+ List.map (fun f -> Cfield (f, k)) (Extlib.opt_conv [] c.cfields)
| _ -> []
let fields_of_tau = function
@@ -360,7 +361,8 @@ let fields_of_tau = function
let fields_of_field = function
| Mfield(_,r,_,_) -> r.fields
- | Cfield(f, k) -> List.map (fun f -> Cfield (f, k)) f.fcomp.cfields
+ | Cfield(f, k) ->
+ List.map (fun f -> Cfield (f, k)) (Extlib.opt_conv [] 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 c235b68f103b51f4ad9a1db546ec7fb3051a3e9b..a6df8a74022d8f6082226d115f3e830b197700cd 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))
- ) [] comp.cfields
+ ) [] (Extlib.the 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 62ef4a7efcc469e2beb9356d1f5d8de875aaec3e..0008f2b6dad00fe0255368b6799ed001542a69d4 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)
- ) c.cfields in
+ ) (Extlib.the 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))
- c.cfields
+ (Extlib.the 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 041f48443637c4af908806f3244d8bb92ad3ea38..0a7ea59741b7d92be4b8a21a6269eba54c3a7846 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 c.cfields
+ ) Heap.Set.empty (Extlib.opt_conv [] 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 c.cfields
+ 0 (Extlib.opt_conv [] 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 f.fcomp.cfields
+ in fnext 0 f (Extlib.the f.fcomp.cfields)
(* -------------------------------------------------------------------------- *)
(* --- Utilities on loc-as-term --- *)
@@ -649,7 +649,7 @@ struct
| C_int i -> A (I i)
| C_float f -> A (F f)
| C_pointer t -> A (P t)
- | C_comp ( { cfields = [f] } as c ) ->
+ | C_comp ( { cfields = Some [f] } as c ) ->
begin (* union having only one field is equivalent to a struct *)
match Ctypes.object_of f.ftype with
| C_array _ -> (if c.cstruct then S c else U c)
@@ -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 c.cfields)
+ List.fold_left flayout [] (List.rev (Extlib.the 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 6706a5a6f194fc3767189e66f288eb3ea5eb8222..076fd8e2ac3e393ef3b38be56828b6e818fe8582 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 c.cfields with
+ match List.rev (Extlib.the 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 ci.cfields)
+ Lang.F.p_conj (List.map mk_pred (Extlib.the 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)
- cfields
+ (Extlib.the 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 f.fcomp.cfields
+ ) hs (Extlib.the 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 ci.cfields)
+ Lang.F.p_conj (List.map mk_pred (Extlib.the 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 fa27dd5e6da55d31ed1be0bb92353b302a2da548..85aa4c281f65656b4c428f8b0f849ac884c2ea4b 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) comp.cfields
+ try List.find (fun fd -> fd.fname = f) (Extlib.opt_conv [] comp.cfields)
with Not_found ->
error env ~loc "No field '%s' in compound type '%s'" f comp.cname
@@ -382,17 +382,17 @@ 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 comp.cfields in
+ let fields = field_range ~inside:false fa fb (Extlib.opt_conv [] 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 fd.fcomp.cfields in
+ let fields = field_range ~inside:false fd fd (Extlib.opt_conv [] 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 fd.fcomp.cfields in
+ let fields = field_range ~inside:true fd fd (Extlib.opt_conv [] 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 0af32684819c1f6b9c5a6b990f88916e06d3ae4d..34b7ec283c7b0d2841fadfda5945a33cf34bc4f9 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 my_exn.cfields, NoOffset), SingleInit (Cil.zero ~loc)])
+ [Field(List.hd (Extlib.the 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 my_exn.cfields, NoOffset) in
- let exn2_field = Field (List.hd my_exn2.cfields, NoOffset) 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 loc = Cil_datatype.Location.unknown in
let real_locals = f.sbody.blocals in
let v1 = Cil.makeLocalVar f "exn" exn_type in
@@ -86,7 +86,7 @@ let add_catch my_exn my_exn2 f =
(TryCatch(
f.sbody,
[ Catch_exn (v1,[(v3,id_block); (v4, convert_exn_block)]),
- Cil.mkBlock
+ Cil.mkBlock
[ Cil.mkStmt
(Return
(Some (Cil.new_exp ~loc (Lval (Var v1, exn_field))),
@@ -178,4 +178,4 @@ let add_exn_cat = File.register_code_transformation_category "add_exn"
let () = File.add_code_transformation_before_cleanup add_exn_cat add_exn
-
+
diff --git a/tests/syntax/ghost_cv_var_decl.ml b/tests/syntax/ghost_cv_var_decl.ml
index b2baec811fdea011ed4111a1d856996604c6d870..96b29cd949e17fb157c2ae4a29fb6d84d37a71df 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) cfields ;
+ List.iter (field_ghost_status fmt lval) (Extlib.opt_conv [] cfields) ;
Format.fprintf fmt " }"
| _ -> assert false
and field_ghost_status fmt lval f =