From a1bfb7821bbff7bad25954efb8c13f4f2d3d2932 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 11 Dec 2020 17:08:15 +0100
Subject: [PATCH] [kernel] Removes cdefined compinfo field
---
.Makefile.lint | 2 -
src/kernel_internals/typing/cabs2cil.ml | 10 +--
src/kernel_services/analysis/exn_flow.ml | 4 +-
src/kernel_services/ast_data/cil_types.mli | 14 ++--
.../ast_printing/cil_types_debug.ml | 2 -
src/kernel_services/ast_queries/cil.ml | 19 ++---
src/kernel_services/ast_queries/cil_const.ml | 71 +++++++++----------
src/kernel_services/ast_queries/cil_const.mli | 44 ++++++------
.../ast_queries/cil_datatype.ml | 1 -
src/plugins/rte/rte.ml | 2 +-
.../value/domains/cvalue/cvalue_init.ml | 3 +-
11 files changed, 86 insertions(+), 86 deletions(-)
diff --git a/.Makefile.lint b/.Makefile.lint
index 0f24c301fb5..32e325b878d 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -68,8 +68,6 @@ ML_LINT_KO+=src/kernel_services/ast_data/ast.mli
ML_LINT_KO+=src/kernel_services/ast_data/kernel_function.ml
ML_LINT_KO+=src/kernel_services/ast_data/kernel_function.mli
ML_LINT_KO+=src/kernel_services/ast_data/property_status.mli
-ML_LINT_KO+=src/kernel_services/ast_queries/cil_const.ml
-ML_LINT_KO+=src/kernel_services/ast_queries/cil_const.mli
ML_LINT_KO+=src/kernel_services/ast_queries/cil_datatype.mli
ML_LINT_KO+=src/kernel_services/ast_queries/cil_state_builder.mli
ML_LINT_KO+=src/kernel_services/ast_queries/logic_const.mli
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 1dd8631d176..458568e04f0 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1263,7 +1263,7 @@ 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 _ ->[]) (fc_stdlib_attribute [])
+ Cil_const.mkCompInfo iss n ~norig (fun _ -> None) (fc_stdlib_attribute [])
in
H.add compInfoNameEnv key res;
res, true
@@ -5544,6 +5544,10 @@ and makeCompType ghost (isstruct: bool)
(* Do not add unnamed bitfields: they can share the empty name. *)
if f.fname <> "" then Hashtbl.add fld_table f.fname f
in
+ if flds = [] && not (Cil.gccMode() || Cil.msvcMode()) then
+ Kernel.error ~current:true ~once:true
+ "Empty %s is allowed only in GCC or MSVC mode"
+ (if comp.cstruct then "struct" else "union");
List.iter check flds;
if comp.cfields <> Some [] && comp.cfields <> None then begin
(* This appears to be a multiply defined structure. This can happen from
@@ -5575,8 +5579,6 @@ and makeCompType ghost (isstruct: bool)
let a = Cil.addAttributes comp.cattr a in
comp.cattr <- process_pragmas_pack_align_comp_attributes comp a;
let res = TComp (comp,empty_size_cache (), []) in
- (* This compinfo is defined, even if there are no fields *)
- comp.cdefined <- true;
(* Create a typedef for this one *)
cabsPushGlobal (GCompTag (comp, CurrentLoc.get ()));
@@ -8219,7 +8221,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
(* Start over with the fields *)
doInit local_env asconst add_implicit_ensures preinit so acc allinitl
(* An incomplete structure with any initializer is an error. *)
- | TComp (comp, _, _), _ :: restil when not comp.cdefined ->
+ | TComp (comp, _, _), _ :: restil when comp.cfields = None ->
Kernel.error ~current:true ~once:true
"variable `%s' has initializer but incomplete type" so.host.vname;
doInit local_env asconst add_implicit_ensures preinit so acc restil
diff --git a/src/kernel_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml
index 677f87ff0eb..75a648f7aa3 100644
--- a/src/kernel_services/analysis/exn_flow.ml
+++ b/src/kernel_services/analysis/exn_flow.ml
@@ -346,7 +346,7 @@ let generate_exn_union e exns =
let loc = Cil_datatype.Location.unknown in
let create_union_fields _ =
let add_one_field t acc = (get_type_tag t, t, None, [], loc) :: acc in
- Cil_datatype.Typ.Set.fold add_one_field exns []
+ Some (Cil_datatype.Typ.Set.fold add_one_field exns [])
in
let union_name = "__fc_exn_union" in
let exn_kind_union =
@@ -360,7 +360,7 @@ let generate_exn_union e exns =
(exn_obj_name,
TComp(exn_kind_union, { scache = Not_Computed } , []), None, [], loc)
in
- [uncaught; kind; obj]
+ Some [uncaught; kind; obj]
in
let struct_name = "__fc_exn_struct" in
let exn_struct =
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 22b936df2af..f05d4b75c33 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -347,7 +347,10 @@ and attrparam =
(** The definition of a structure or union type. Use {!Cil.mkCompInfo} to make
one and use {!Cil.copyCompInfo} to copy one (this ensures that a new key is
assigned and that the fields have the right pointers to parents.).
- @plugin development guide *)
+ @plugin development guide
+
+ @since Frama-C+dev [cfields] is an option, [None] is used for incomplete
+ types (in replacement of removed field [cdefined]) *)
and compinfo = {
mutable cstruct: bool;
(** [true] if struct, [false] if union *)
@@ -368,18 +371,15 @@ and compinfo = {
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 *)
+ fieldinfo's between two compinfo's.
+
+ None value means that the type is incomplete. *)
mutable cattr: attributes;
(** The attributes that are defined at the same time as the composite
type. These attributes can be supplemented individually at each
reference to this [compinfo] using the [TComp] type constructor. *)
- mutable cdefined: bool;
- (** This boolean flag can be used to distinguish between structures
- that have not been defined and those that have been defined but have
- no fields (such things are allowed in gcc). *)
-
mutable creferenced: bool;
(** [true] if used. Initially set to [false]. *)
}
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index ca470bb9dae..7ab3d3f9d0f 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -200,7 +200,6 @@ and pp_compinfo fmt compinfo =
ckey=%a;\
cfields=%a;\
cattr=%a;\
- cdefined=%a;\
creferenced=%a;\
}"
pp_bool compinfo.cstruct
@@ -209,7 +208,6 @@ and pp_compinfo fmt compinfo =
pp_int compinfo.ckey
(pp_option (pp_list pp_fieldinfo)) compinfo.cfields
pp_attributes compinfo.cattr
- pp_bool compinfo.cdefined
pp_bool compinfo.creferenced
else
Format.fprintf fmt
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 873a6416b00..94b5089bfb7 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -4321,11 +4321,16 @@ and bitsSizeOf t =
scache
(fun () -> begin
(* sizeof() empty structs/arrays is only allowed on GCC/MSVC *)
- if not comp.cdefined && not (gccMode () || msvcMode ()) then begin
+ if comp.cfields = None then begin
raise
(SizeOfError
(Format.sprintf "abstract type '%s'" (compFullName comp), t))
- end else
+ end
+ else if comp.cfields = Some [] && not (gccMode () || msvcMode ()) then
+ raise
+ (SizeOfError
+ (Format.sprintf "empty struct '%s'" (compFullName comp), t))
+ else
0
end)
@@ -6105,9 +6110,9 @@ let rec isCompleteType ?allowZeroSizeArrays ?(last_field=false) t =
is_complete_agg_member ~allowZeroSizeArrays ~last_field t
| TArray(t, Some _, _, _) ->
is_complete_agg_member ~allowZeroSizeArrays ~last_field t
- | TComp (comp, _, _) -> (* Struct or union *)
- comp.cdefined &&
- complete_type_fields ~allowZeroSizeArrays comp.cstruct comp.cfields
+ | TComp ( { cfields = None } , _, _) -> false
+ | TComp ( { cstruct ; cfields = Some flds }, _, _) -> (* Struct or union *)
+ complete_type_fields ~allowZeroSizeArrays cstruct flds
| TEnum({eitems = []},_) -> false
| TEnum _ -> true
| TInt _ | TFloat _ | TPtr _ | TBuiltin_va_list _ -> true
@@ -6123,9 +6128,7 @@ and complete_type_fields ?allowZeroSizeArrays is_struct fields =
| f :: tl ->
is_complete_agg_member ?allowZeroSizeArrays f.ftype && aux false tl
in
- match fields with
- | None -> false
- | Some fields -> aux true 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 d7f183431cd..06e92efec1a 100644
--- a/src/kernel_services/ast_queries/cil_const.ml
+++ b/src/kernel_services/ast_queries/cil_const.ml
@@ -47,10 +47,10 @@ module CurrentLoc =
State_builder.Ref
(Cil_datatype.Location)
(struct
- let dependencies = []
- let name = "CurrentLoc"
- let default () = Cil_datatype.Location.unknown
- end)
+ let dependencies = []
+ let name = "CurrentLoc"
+ let default () = Cil_datatype.Location.unknown
+ end)
let voidType = TVoid([])
@@ -66,27 +66,27 @@ let copy_with_new_vid v =
let n = Vid.next () in
let new_v = { v with vid = n } in
(match v.vlogic_var_assoc with
- | None -> ()
- | Some lv ->
- let new_lv = { lv with lv_id = n } in
- new_v.vlogic_var_assoc <- Some new_lv;
- new_lv.lv_origin <- Some new_v);
+ | None -> ()
+ | Some lv ->
+ let new_lv = { lv with lv_id = n } in
+ new_v.vlogic_var_assoc <- Some new_lv;
+ new_lv.lv_origin <- Some new_v);
new_v
let change_varinfo_name vi name =
vi.vname <- name;
match vi.vlogic_var_assoc with
- | None -> ()
- | Some lv -> lv.lv_name <- name
+ | None -> ()
+ | Some lv -> lv.lv_name <- name
let new_raw_id = Vid.next
(* The next compindo identifier to use. Counts up. *)
- let nextCompinfoKey =
- let module M =
- State_builder.SharedCounter(struct let name = "compinfokey" end)
- in
- M.next
+let nextCompinfoKey =
+ let module M =
+ State_builder.SharedCounter(struct let name = "compinfokey" end)
+ in
+ M.next
(** Creates a (potentially recursive) composite type. Make sure you add a
* GTag for it to the file! **)
@@ -99,7 +99,7 @@ let mkCompInfo
* the fields. The function can ignore this argument if not
* constructing a recursive type. *)
(mkfspec: compinfo -> (string * typ * int option * attribute list *
- location) list)
+ location) list option)
(a: attribute list) : compinfo =
(* make a new name for anonymous structs *)
@@ -114,25 +114,24 @@ let mkCompInfo
cattr = a;
creferenced = false;
(* Make this compinfo undefined by default *)
- cdefined = false; }
+ }
in
let flds =
- List.mapi (fun forder (fn, ft, fb, fa, fl) ->
- { fcomp = comp;
- forder;
- ftype = ft;
- forig_name = fn;
- fname = fn;
- fbitfield = fb;
- fattr = fa;
- floc = fl;
- faddrof = false;
- fsize_in_bits = None;
- foffset_in_bits = None;
- fpadding_in_bits = None;
- }) (mkfspec comp) in
- comp.cfields <- if flds <> [] then Some flds else None;
- if flds <> [] then comp.cdefined <- true;
+ Extlib.opt_map (List.mapi (fun forder (fn, ft, fb, fa, fl) ->
+ { fcomp = comp;
+ forder;
+ ftype = ft;
+ forig_name = fn;
+ fname = fn;
+ fbitfield = fb;
+ fattr = fa;
+ floc = fl;
+ faddrof = false;
+ fsize_in_bits = None;
+ foffset_in_bits = None;
+ fpadding_in_bits = None;
+ })) (mkfspec comp) in
+ comp.cfields <- flds;
comp
(** Make a copy of a compinfo, changing the name and the key *)
@@ -162,8 +161,8 @@ let make_logic_var =
let make_logic_info k x =
{ l_var_info = make_logic_var_kind x k (Ctype voidType);
- (* we should put the right type when fields
- l_profile, l_type will be factorized *)
+ (* we should put the right type when fields
+ l_profile, l_type will be factorized *)
l_type = None;
l_tparams = [];
l_labels = [];
diff --git a/src/kernel_services/ast_queries/cil_const.mli b/src/kernel_services/ast_queries/cil_const.mli
index 58178291430..5523ae89d6f 100644
--- a/src/kernel_services/ast_queries/cil_const.mli
+++ b/src/kernel_services/ast_queries/cil_const.mli
@@ -70,28 +70,30 @@ val copy_with_new_vid: varinfo -> varinfo
val change_varinfo_name: varinfo -> string -> unit
val new_raw_id: unit -> int
- (** Generate a new ID. This will be different than any variable ID
- that is generated by {!Cil.makeLocalVar} and friends.
- Must not be used for setting vid: use {!set_vid} instead. *)
+(** Generate a new ID. This will be different than any variable ID
+ that is generated by {!Cil.makeLocalVar} and friends.
+ Must not be used for setting vid: use {!set_vid} instead. *)
(** Creates a (potentially recursive) composite type. The arguments are:
* (1) a boolean indicating whether it is a struct or a union, (2) the name
* (always non-empty), (3) a function that when given a representation of the
* structure type constructs the type of the fields recursive type (the first
* argument is only useful when some fields need to refer to the type of the
- * structure itself), and (4) a list of attributes to be associated with the
- * composite type. The resulting compinfo has the field "cdefined" only if
- * the list of fields is non-empty. *)
+ * structure itself), and (4) an optional list of attributes to be associated
+ * with the composite type, "None" means that the struct is incomplete.
+ *
+ * @since Frama-C+dev the 4th parameter is a function that returns an option.
+ **)
val mkCompInfo: bool -> (* whether it is a struct or a union *)
- string -> (* name of the composite type; cannot be empty *)
- ?norig:string -> (* original name of the composite type, empty when anonymous *)
- (compinfo ->
- (string * typ * int option * attributes * location) list) ->
- (* a function that when given a forward
- representation of the structure type constructs the type of
- the fields. The function can ignore this argument if not
- constructing a recursive type. *)
- attributes -> compinfo
+ string -> (* name of the composite type; cannot be empty *)
+ ?norig:string -> (* original name of the composite type, empty when anonymous *)
+ (compinfo ->
+ (string * typ * int option * attributes * location) list option) ->
+ (* a function that when given a forward
+ representation of the structure type constructs the type of
+ the fields. The function can ignore this argument if not
+ constructing a recursive type. *)
+ attributes -> compinfo
(** Makes a shallow copy of a {!Cil_types.compinfo} changing the name. It also
copies the fields, and makes sure that the copied field points back to the
@@ -107,25 +109,25 @@ val copyCompInfo: ?fresh:bool -> compinfo -> string -> compinfo
*)
val make_logic_var_kind : string -> logic_var_kind -> logic_type -> logic_var
-(** Create a fresh logical variable giving its name and type.
- @deprecated Fluorine-20130401 You should use a specific
+(** Create a fresh logical variable giving its name and type.
+ @deprecated Fluorine-20130401 You should use a specific
make_logic_var_[kind] function below, or {! Cil.cvar_to_lvar}
*)
val make_logic_var : string -> logic_type -> logic_var
-(** Create a new global logic variable
+(** Create a new global logic variable
@since Fluorine-20130401 *)
val make_logic_var_global: string -> logic_type -> logic_var
-(** Create a new formal logic variable
+(** Create a new formal logic variable
@since Fluorine-20130401 *)
val make_logic_var_formal: string -> logic_type -> logic_var
-(** Create a new quantified logic variable
+(** Create a new quantified logic variable
@since Fluorine-20130401 *)
val make_logic_var_quant: string -> logic_type -> logic_var
-(** Create a new local logic variable
+(** Create a new local logic variable
@since Fluorine-20130401 *)
val make_logic_var_local: string -> logic_type -> logic_var
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 5716e4384f5..b345e242afc 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -778,7 +778,6 @@ module Compinfo = struct
ckey = -1;
cfields = None;
cattr = [];
- cdefined = false;
creferenced = false } ]
let compare v1 v2 = Datatype.Int.compare v1.ckey v2.ckey
let hash v = Hashtbl.hash v.ckey
diff --git a/src/plugins/rte/rte.ml b/src/plugins/rte/rte.ml
index 71ea75016fd..51a97f8a7fb 100644
--- a/src/plugins/rte/rte.ml
+++ b/src/plugins/rte/rte.ml
@@ -114,7 +114,7 @@ let lval_initialized_assertion ~remove_trivial:_ ~on_alarm lv =
| TComp({cstruct = false; cfields} ,_,_) ->
(match cfields with
| Some [] | None -> () (* empty union, supported by gcc with size 0.
- Trivially initialized. *)
+ Trivially initialized. *)
| _ ->
let llv =
List.map
diff --git a/src/plugins/value/domains/cvalue/cvalue_init.ml b/src/plugins/value/domains/cvalue/cvalue_init.ml
index 28b09e3fb96..2266554ce94 100644
--- a/src/plugins/value/domains/cvalue/cvalue_init.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_init.ml
@@ -98,8 +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 = Some [] && ci.cdefined &&
- not (Cil.gccMode () || Cil.msvcMode ()) then
+ if ci.cfields = Some [] && not (Cil.gccMode () || Cil.msvcMode ()) then
Value_parameters.abort ~current:true
"@[empty %ss@ are unsupported@ (type '%a',@ location %a%a)@ \
in C99 (only allowed as GCC/MSVC extension).@ Aborting.@]"
--
GitLab