diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 5b5ee4a03c0a0fc79671c094b9f2b0df526bdf1e..05f104b08484bb6ac8710710f55e482d15519b9a 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -2568,30 +2568,6 @@ let cabsAddAttributes al0 (al: attributes) : attributes =
al
al0
-type combineWhat =
- CombineFundef of bool
- (* The new definition is for a function definition. The old
- * is for a prototype. arg is [true] for an old-style declaration *)
- | CombineFunarg of bool
- (* Comparing a function argument type with an old prototype argument.
- arg is [true] for an old-style declaration, which
- triggers some ad hoc treatment in GCC mode. *)
- | CombineFunret (* Comparing the return of a function with that from an old
- * prototype *)
- | CombineOther
-
-(* [combineAttributes what olda a] combines the attributes in [olda] and [a]
- according to [what]:
- - if [what == CombineFunarg], then override old attributes;
- this is used to ensure that attributes from formal argument types in a
- function definition are not mixed with attributes from arguments in other
- (compatible, but with different qualifiers) declarations;
- - else, perform the union of old and new attributes. *)
-let combineAttributes what olda a =
- match what with
- | CombineFunarg _ -> a (* override old attributes with new ones *)
- | _ -> cabsAddAttributes olda a (* union of attributes *)
-
(* BY: nothing cabs here, plus seems to duplicate most of Cil.typeAddAttributes *)
(* see [combineAttributes] above for details about the [what] argument *)
let rec cabsTypeCombineAttributes what a0 t =
@@ -2679,266 +2655,11 @@ and cabsArrayPushAttributes what al = function
let cabsTypeAddAttributes =
cabsTypeCombineAttributes CombineOther
-exception Cannot_combine of string
(* Do types *)
-(* Combine the types. Raises the Cannot_combine exception with an error message.
- [what] is used to recursively deal with function return types and function
- arguments in special ways.
- Note: we cannot force the qualifiers of oldt and t to be the same here,
- because in some cases (e.g. string literals and char pointers) it is
- allowed to have differences, while in others we want to be more strict. *)
-let rec combineTypes ?(strictReturnTypes=false) (what: combineWhat) (oldt: typ) (t: typ) : typ =
- match oldt, t with
- | TVoid olda, TVoid a -> TVoid (combineAttributes what olda a)
- (* allows ignoring a returned value *)
- | _ , TVoid _ when what = CombineFunret && not strictReturnTypes -> t
- | TInt (oldik, olda), TInt (ik, a) ->
- let combineIK oldk k =
- if oldk = k then oldk else
- (match what with
- | CombineFunarg b when
- Cil.gccMode () && oldk = IInt
- && bytesSizeOf t <= (bytesSizeOfInt IInt) && b ->
- (* GCC allows a function definition to have a more precise integer
- * type than a prototype that says "int" *)
- k
- | _ ->
- raise (Cannot_combine
- (Format.asprintf
- "different integer types:@ '%a' and '%a'"
- Cil_printer.pp_ikind oldk Cil_printer.pp_ikind k)))
- in
- TInt (combineIK oldik ik, combineAttributes what olda a)
- | TFloat (oldfk, olda), TFloat (fk, a) ->
- let combineFK oldk k =
- if oldk = k then oldk else
- ( match what with
- | CombineFunarg b when
- Cil.gccMode () && oldk = FDouble && k = FFloat && b ->
- (* GCC allows a function definition to have a more precise float
- * type than a prototype that says "double" *)
- k
- | _ ->
- raise (Cannot_combine "different floating point types"))
- in
- TFloat (combineFK oldfk fk, combineAttributes what olda a)
- | TEnum (_, olda), TEnum (ei, a) ->
- TEnum (ei, combineAttributes what olda a)
-
- (* Strange one. But seems to be handled by GCC *)
- | TEnum (oldei, olda) , TInt(IInt, a) -> TEnum(oldei,
- combineAttributes what olda a)
- (* Strange one. But seems to be handled by GCC *)
- | TInt(IInt, olda), TEnum (ei, a) -> TEnum(ei, combineAttributes what olda a)
-
-
- | TComp (oldci, olda) , TComp (ci, a) ->
- if oldci.cstruct <> ci.cstruct then
- raise (Cannot_combine "different struct/union types");
- let comb_a = combineAttributes what olda a in
- if oldci.cname = ci.cname then
- TComp (oldci, comb_a)
- else
- raise (Cannot_combine (Format.sprintf "%ss with different tags"
- (if oldci.cstruct then "struct" else "union")))
-
- | TArray (oldbt, oldsz, olda), TArray (bt, sz, a) ->
- let newbt = combineTypes ~strictReturnTypes CombineOther oldbt bt in
- let newsz =
- match oldsz, sz with
- | None, Some _ -> sz
- | Some _, None -> oldsz
- | None, None -> sz
- | Some oldsz', Some sz' ->
- (* They are not structurally equal. But perhaps they are equal if we
- evaluate them. Check first machine independent comparison. *)
- let checkEqualSize (machdep: bool) =
- let size_t = Cil.theMachine.Cil.typeOfSizeOf in
- let size_t_oldsz' = Cil.mkCast ~force:false ~newt:size_t oldsz' in
- let size_t_sz' = Cil.mkCast ~force:false ~newt:size_t sz' in
- ExpStructEq.equal
- (constFold machdep size_t_oldsz')
- (constFold machdep size_t_sz')
- in
- if checkEqualSize false then
- oldsz
- else if checkEqualSize true then begin
- Kernel.warning ~current:true
- "Array type comparison succeeds only based on machine-dependent \
- constant evaluation: %a and %a\n"
- Cil_printer.pp_exp oldsz' Cil_printer.pp_exp sz';
- oldsz
- end else
- raise (Cannot_combine "different array lengths")
-
- in
- TArray (newbt, newsz, combineAttributes what olda a)
-
- | TPtr (oldbt, olda), TPtr (bt, a) ->
- TPtr (combineTypes ~strictReturnTypes CombineOther oldbt bt, combineAttributes what olda a)
-
- | TFun (oldrt, oldargs, oldva, olda), TFun (rt, args, va, a) ->
- let newrt = combineTypes ~strictReturnTypes CombineFunret oldrt rt in
- if oldva != va then
- raise (Cannot_combine "different vararg specifiers");
- (* If one does not have arguments, believe the one with the
- * arguments *)
- let newargs, olda' =
- if oldargs = None then args, olda else
- if args = None then oldargs, olda else
- let (oldargslist, oldghostargslist) = argsToPairOfLists oldargs in
- let (argslist, ghostargslist) = argsToPairOfLists args in
- if List.length oldargslist <> List.length argslist then
- raise (Cannot_combine "different number of arguments")
- else if List.length oldghostargslist <> List.length ghostargslist then
- raise (Cannot_combine "different number of ghost arguments")
- else begin
- let oldargslist = oldargslist @ oldghostargslist in
- let argslist = argslist @ ghostargslist in
- (* Construct a mapping between old and new argument names. *)
- let map = H.create 5 in
- List.iter2
- (fun (on, _, _) (an, _, _) -> H.replace map on an)
- oldargslist argslist;
- (* Go over the arguments and update the old ones with the
- * adjusted types *)
- (* Format.printf "new type is %a@." Cil_datatype.Typ.pretty t; *)
- let what =
- match what with
- | CombineFundef b -> CombineFunarg b
- | _ -> CombineOther
- in
- Some
- (List.map2
- (fun (on, ot, oa) (an, at, aa) ->
- (* Update the names. Always prefer the new name. This is
- * very important if the prototype uses different names than
- * the function definition. *)
- let n = if an <> "" then an else on in
- let t = combineTypes ~strictReturnTypes what ot at in
- let a = addAttributes oa aa in
- (n, t, a))
- oldargslist argslist),
- olda
- end
- in
- (* Drop missingproto as soon as one of the type is a properly declared one*)
- let olda =
- if not (Cil.hasAttribute "missingproto" a) then
- Cil.dropAttribute "missingproto" olda'
- else olda'
- in
- let a =
- if not (Cil.hasAttribute "missingproto" olda') then
- Cil.dropAttribute "missingproto" a
- else a
- in
- TFun (newrt, newargs, oldva, combineAttributes what olda a)
-
- | TNamed (oldt, olda), TNamed (t, a) when oldt.tname = t.tname ->
- TNamed (oldt, combineAttributes what olda a)
-
- | TBuiltin_va_list olda, TBuiltin_va_list a ->
- TBuiltin_va_list (combineAttributes what olda a)
-
- (* Unroll first the new type *)
- | _, TNamed (t, a) ->
- let res = combineTypes what oldt t.ttype in
- cabsTypeCombineAttributes what a res
-
- (* And unroll the old type as well if necessary *)
- | TNamed (oldt, a), _ ->
- let res = combineTypes what oldt.ttype t in
- cabsTypeCombineAttributes what a res
-
- | _ -> raise (Cannot_combine
- (Format.asprintf "different type constructors:@ %a and %a"
- Cil_datatype.Typ.pretty oldt Cil_datatype.Typ.pretty t))
let get_qualifiers t = Cil.filter_qualifier_attributes (Cil.typeAttrs t)
-(* how type qualifiers must be checked *)
-type qualifier_check_context =
- | Identical (* identical qualifiers. *)
- | IdenticalToplevel (* ignore at toplevel, use Identical when going under a
- pointer. *)
- | Covariant (* first type can have const-qualifications
- the second doesn't have. *)
- | CovariantToplevel
- (* accepts everything for current type, use Covariant when going under a
- pointer. *)
- | Contravariant (* second type can have const-qualifications
- the first doesn't have. *)
- | ContravariantToplevel
- (* accepts everything for current type, use Contravariant when going under
- a pointer. *)
-
-let qualifier_context_fun_arg = function
- | Identical | IdenticalToplevel -> IdenticalToplevel
- | Covariant | CovariantToplevel -> ContravariantToplevel
- | Contravariant | ContravariantToplevel -> CovariantToplevel
-
-let qualifier_context_fun_ret = function
- | Identical | IdenticalToplevel -> IdenticalToplevel
- | Covariant | CovariantToplevel -> CovariantToplevel
- | Contravariant | ContravariantToplevel -> ContravariantToplevel
-
-let qualifier_context_ptr = function
- | Identical | IdenticalToplevel -> Identical
- | Covariant | CovariantToplevel -> Covariant
- | Contravariant | ContravariantToplevel -> Contravariant
-
-let included_qualifiers ?(context=Identical) a1 a2 =
- let a1 = Cil.filter_qualifier_attributes a1 in
- let a2 = Cil.filter_qualifier_attributes a2 in
- let a1 = Cil.dropAttribute "restrict" a1 in
- let a2 = Cil.dropAttribute "restrict" a2 in
- let a1_no_cv = Cil.dropAttributes ["const"; "volatile"] a1 in
- let a2_no_cv = Cil.dropAttributes ["const"; "volatile"] a2 in
- let is_equal = Cil_datatype.Attributes.equal a1 a2 in
- if is_equal then true
- else begin
- match context with
- | Identical -> false
- | Covariant -> Cil_datatype.Attributes.equal a1_no_cv a2
- | Contravariant -> Cil_datatype.Attributes.equal a1 a2_no_cv
- | CovariantToplevel | ContravariantToplevel | IdenticalToplevel -> true
- end
-
-(* precondition: t1 and t2 must be "compatible" as per combineTypes, i.e.
- you must have called [combineTypes t1 t2] before calling this function. *)
-let rec have_compatible_qualifiers_deep ?(context=Identical) t1 t2 =
- match unrollType t1, unrollType t2 with
- | TFun (tres1, Some args1, _, _), TFun (tres2, Some args2, _, _) ->
- have_compatible_qualifiers_deep
- ~context:(qualifier_context_fun_ret context) tres1 tres2 &&
- let context = qualifier_context_fun_arg context in
- List.for_all2 (fun (_, t1', a1) (_, t2', a2) ->
- have_compatible_qualifiers_deep ~context t1' t2' &&
- included_qualifiers ~context a1 a2)
- args1 args2
- | TPtr (t1', a1), TPtr (t2', a2)
- | TArray (t1', _, a1), TArray (t2', _, a2) ->
- (included_qualifiers ~context a1 a2) &&
- let context = qualifier_context_ptr context in
- have_compatible_qualifiers_deep ~context t1' t2'
- | _, _ -> included_qualifiers ~context (Cil.typeAttrs t1) (Cil.typeAttrs t2)
-
-let compatibleTypes ?strictReturnTypes ?context t1 t2 =
- let r = combineTypes ?strictReturnTypes CombineOther t1 t2 in
- (* C99, 6.7.3 §9: "... to be compatible, both shall have the identically
- qualified version of a compatible type;" *)
- if not (have_compatible_qualifiers_deep ?context t1 t2) then
- raise (Cannot_combine "different qualifiers");
- (* Note: different non-qualifier attributes will be silently dropped. *)
- r
-
-let areCompatibleTypes ?strictReturnTypes ?context t1 t2 =
- try
- ignore (compatibleTypes ?strictReturnTypes ?context t1 t2); true
- with Cannot_combine _ -> false
-
(* Specify whether the cast is from the source code *)
let rec castTo ?context ?(fromsource=false)
(ot : typ) (nt : typ) (e : exp) : (typ * exp ) =
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 0ef1c773dbe80583e455cda43402ac07cdd8f31d..a84cc8f68cbeddc85b3ed1691419d5784a8ba422 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -561,10 +561,6 @@ module ModelMerging =
Format.fprintf fmt "model@ %a@ { %s }" Cil_printer.pp_typ t s
end)
-let same_int64 e1 e2 =
- match constFoldToInt e1, constFoldToInt e2 with
- | Some i, Some i' -> Integer.equal i i'
- | _ -> false
let compare_int e1 e2 =
match (constFold true e1), (constFold true e2) with
@@ -959,217 +955,89 @@ let intEnumInfoNode =
EnumMerging.getNode eEq eSyn 0 intEnumInfo intEnumInfo
(Some (Cil_datatype.Location.unknown, 0))
-(* Combine the types. Raises the Failure exception with an error message.
- * isdef says whether the new type is for a definition *)
-type combineWhat =
- CombineFundef (* The new definition is for a function definition. The old
- * is for a prototype *)
- | CombineFunarg (* Comparing a function argument type with an old prototype
- * arg *)
- | CombineFunret (* Comparing the return of a function with that from an old
- * prototype *)
- | CombineOther
-
-let rec combineTypes (what: combineWhat)
- (oldfidx: int) (oldt: typ)
- (fidx: int) (t: typ) : typ =
- match oldt, t with
- | TVoid olda, TVoid a -> TVoid (addAttributes olda a)
- | TInt (oldik, olda), TInt (ik, a) ->
- let combineIK oldk k =
- if oldk == k
- then oldk
- else
- if bytesSizeOfInt oldk=bytesSizeOfInt k && isSigned oldk=isSigned k
- then
- (* the types contain the same sort of values but are not equal.
- For example on x86_16 machdep unsigned short and unsigned int. *)
- if rank oldk<rank k then k else oldk
- else
- (* GCC allows a function definition to have a more precise integer
- * type than a prototype that says "int" *)
- if Cil.gccMode () && oldk = IInt && bitsSizeOf t <= 32
- && (what = CombineFunarg || what = CombineFunret)
- then
- k
- else (
- let msg =
- Format.asprintf
- "different integer types %a and %a"
- Cil_printer.pp_typ oldt Cil_printer.pp_typ t
- in
- raise (Failure msg))
- in
- TInt (combineIK oldik ik, addAttributes olda a)
-
- | TFloat (oldfk, olda), TFloat (fk, a) ->
- let combineFK oldk k =
- if oldk == k then oldk else
- (* GCC allows a function definition to have a more precise integer
- * type than a prototype that says "double" *)
- if Cil.gccMode () && oldk = FDouble && k = FFloat &&
- (what = CombineFunarg || what = CombineFunret)
- then
- k
- else
- raise (Failure "different floating point types")
- in
- TFloat (combineFK oldfk fk, addAttributes olda a)
-
- | TEnum (oldei, olda), TEnum (ei, a) ->
- (* Matching enumerations always succeeds. But sometimes it maps both
- * enumerations to integers *)
- matchEnumInfo oldfidx oldei fidx ei;
- TEnum (oldei, addAttributes olda a)
-
-
- (* Strange one. But seems to be handled by GCC *)
- | TEnum (oldei, olda) , TInt(IInt, a) -> TEnum(oldei,
- addAttributes olda a)
-
- (* Strange one. But seems to be handled by GCC. Warning. Here we are
- * leaking types from new to old *)
- | TInt(IInt, olda), TEnum (ei, a) -> TEnum(ei, addAttributes olda a)
-
- | TComp (oldci, olda) , TComp (ci, a) ->
- matchCompInfo oldfidx oldci fidx ci;
- (* If we get here we were successful *)
- TComp (oldci, addAttributes olda a)
-
- | TArray (oldbt, oldsz, olda), TArray (bt, sz, a) ->
- let combbt = combineTypes CombineOther oldfidx oldbt fidx bt in
- let combinesz =
- match oldsz, sz with
- None, Some _ -> sz
- | Some _, None -> oldsz
- | None, None -> oldsz
- | Some oldsz', Some sz' ->
- if same_int64 oldsz' sz' then oldsz else
- raise (Failure "different array sizes")
- in
- TArray (combbt, combinesz, addAttributes olda a)
-
- | TPtr (oldbt, olda), TPtr (bt, a) ->
- TPtr (combineTypes CombineOther oldfidx oldbt fidx bt,
- addAttributes olda a)
-
- | TFun (oldrt, oldargs, oldva, olda), TFun (rt, args, va, a) ->
- let newrt =
- combineTypes
- (if what = CombineFundef then CombineFunret else CombineOther)
- oldfidx oldrt fidx rt
- in
- if oldva != va then
- raise (Failure "different vararg specifiers");
- (* If one does not have arguments, believe the one with the
- * arguments *)
- let newargs =
- if oldargs = None then args else
- if args = None then oldargs else
- let oldargslist = argsToList oldargs in
- let argslist = argsToList args in
- if List.length oldargslist <> List.length argslist then
- raise (Failure "different number of arguments")
- else begin
- (* Go over the arguments and update the old ones with the
- * adjusted types *)
- Some
- (List.map2
- (fun (on, ot, oa) (an, at, aa) ->
- let n = if an <> "" then an else on in
- let t =
- combineTypes
- (if what = CombineFundef then CombineFunarg
- else CombineOther)
- oldfidx ot fidx at
- in
- let a = addAttributes oa aa in
- (n, t, a))
- oldargslist argslist)
- end
- in
- let olda =
- if Cil.hasAttribute "missingproto" a then olda
- else Cil.dropAttribute "missingproto" olda
- in
- let a =
- if Cil.hasAttribute "missingproto" olda then a
- else Cil.dropAttribute "missingproto" a
- in
- TFun (newrt, newargs, oldva, addAttributes olda a)
-
- | TBuiltin_va_list olda, TBuiltin_va_list a ->
- TBuiltin_va_list (addAttributes olda a)
-
- | TNamed (oldt, olda), TNamed (t, a) ->
- matchTypeInfo oldfidx oldt fidx t;
- (* If we get here we were able to match *)
- TNamed(oldt, addAttributes olda a)
-
- (* Unroll first the new type *)
- | _, TNamed (t, a) ->
- let res = combineTypes what oldfidx oldt fidx t.ttype in
- typeAddAttributes a res
-
- (* And unroll the old type as well if necessary *)
- | TNamed (oldt, a), _ ->
- let res = combineTypes what oldfidx oldt.ttype fidx t in
- typeAddAttributes a res
-
- | _ -> (
- (* raise (Failure "different type constructors") *)
- let msg:string =
- Format.asprintf
- "different type constructors: %a vs. %a"
- Cil_printer.pp_typ oldt Cil_printer.pp_typ t
- in
- raise (Failure msg))
(* When comparing composite types for equality, we tolerate
some differences related to packed/aligned attributes:
if the offsets of each field are the same regardless of these
attributes, we allow them to merge (arbitrarily choosing whether
to keep or to drop such attributes). *)
-and equalModuloPackedAlign attrs1 attrs2 =
+let equalModuloPackedAlign attrs1 attrs2 =
let drop = Cil.dropAttributes ["packed"; "aligned"] in
equal_attributes_for_merge (drop attrs1) (drop attrs2)
+
+
(* Checks if fields [f1] and [f2] (contained in the composite types
[typ_ci1] and [typ_ci2] respectively) are equal except for
alignment-related attributes.
Raises [Failure] if the fields are not equivalent.
If [mustCheckOffsets] is true, then there is already a difference in the
composite type, so each field must be checked. *)
-and checkFieldsEqualModuloPackedAlign ~mustCheckOffsets f1 f2 =
+let checkFieldsEqualModuloPackedAlign ~mustCheckOffsets f1 f2 =
if f1.fbitfield <> f2.fbitfield then
raise (Failure "different bitfield info");
if mustCheckOffsets || not (equal_attributes_for_merge f1.fattr f2.fattr) then
(* different attributes: check if the difference is only due
to aligned/packed attributes, and if the offsets are the same,
in which case the difference may be safely ignored *)
- begin
- try
- let offs1, width1 = Cil.fieldBitsOffset f1
- and offs2, width2 = Cil.fieldBitsOffset f2
- in
- if not (equalModuloPackedAlign f1.fattr f2.fattr)
- || offs1 <> offs2 || width1 <> width2 then
- if mustCheckOffsets then
- let err = "incompatible attributes in composite types "
- ^ "and/or field " ^ f1.fname in
- raise (Failure err)
- else
- let err = "incompatible attributes for field " ^ f1.fname in
- raise (Failure err)
- with Not_found ->
- Kernel.fatal
- "field offset not found in table: %a or %a"
- Printer.pp_field f1 Printer.pp_field f2
- end
+ try
+ let offs1, width1 = Cil.fieldBitsOffset f1
+ and offs2, width2 = Cil.fieldBitsOffset f2
+ in
+ if not (equalModuloPackedAlign f1.fattr f2.fattr)
+ || offs1 <> offs2 || width1 <> width2 then
+ if mustCheckOffsets then
+ let err = "incompatible attributes in composite types and/or field "
+ ^ f1.fname in
+ raise (Failure err)
+ else
+ let err = "incompatible attributes for field " ^ f1.fname in
+ raise (Failure err)
+ with Not_found ->
+ Kernel.fatal
+ "field offset not found in table: %a or %a"
+ Printer.pp_field f1 Printer.pp_field f2
-(* Match two compinfos and throw a Failure if they do not match *)
-and matchCompInfo (oldfidx: int) (oldci: compinfo)
- (fidx: int) (ci: compinfo) : unit =
+
+(* Match two enuminfos and throw a Failure if they do not match *)
+let matchEnumInfo (oldfidx: int) (oldei: enuminfo)
+ (fidx: int) (ei: enuminfo) : unit =
+ (* Find the node for this enum, no path compression. *)
+ let oldeinode = EnumMerging.getNode eEq eSyn oldfidx oldei oldei None in
+ let einode = EnumMerging.getNode eEq eSyn fidx ei ei None in
+ if oldeinode == einode then (* We already know they are the same *)
+ ()
+ else
+ (* Replace with the representative data *)
+ let oldei = oldeinode.ndata in
+ let ei = einode.ndata in
+ (* Try to match them. But if you cannot just make them both integers *)
+ try
+ have_same_enum_items oldei ei;
+ (* Set the representative *)
+ let newrep, _ = EnumMerging.union oldeinode einode in
+ (* We get here if the enumerations match *)
+ newrep.ndata.eattr <- addAttributes oldei.eattr ei.eattr
+ with (Cannot_combine msg | Failure msg) ->
+ let pp_items = Pretty_utils.pp_list ~pre:"{" ~suf:"}" ~sep:",@ "
+ (fun fmt item ->
+ Format.fprintf fmt "%s=%a" item.eiorig_name
+ Cil_printer.pp_exp item.eival)
+ in
+ if oldeinode != intEnumInfoNode && einode != intEnumInfoNode then
+ Kernel.warning
+ "@[merging definitions of enum %s using int type@ (%s);@ items %a and@ %a@]"
+ oldei.ename msg
+ pp_items oldei.eitems pp_items ei.eitems;
+ (* Get here if you cannot merge two enumeration nodes *)
+ if oldeinode != intEnumInfoNode then
+ ignore(EnumMerging.union oldeinode intEnumInfoNode);
+ if einode != intEnumInfoNode then
+ ignore(EnumMerging.union einode intEnumInfoNode)
+
+
+let matchCompInfoGen (combineF : combineFunction) (oldfidx: int) (oldci: compinfo)
+ (fidx: int) (ci: compinfo) : unit =
let cstruct = oldci.cstruct in
if cstruct <> ci.cstruct then
raise (Failure "different struct/union types");
@@ -1182,7 +1050,7 @@ and matchCompInfo (oldfidx: int) (oldci: compinfo)
let cinode = PlainMerging.getNode sEq sSyn fidx ci.cname ci None in
if oldcinode == cinode then (* We already know they are the same *)
()
- else begin
+ else
(* Replace with the representative data *)
let oldci = oldcinode.ndata in
let oldfidx = oldcinode.nfidx in
@@ -1245,12 +1113,12 @@ and matchCompInfo (oldfidx: int) (oldci: compinfo)
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
+ combineF.typ_combine combineF true
+ CombineOther oldfidx oldf.ftype fidx f.ftype in
(* Change the type in the representative *)
oldf.ftype <- newtype)
oldfields fields
- with Failure reason ->
+ with (Cannot_combine reason | Failure reason) ->
(* Our assumption was wrong. Forget the isomorphism *)
undo ();
let fields_old =
@@ -1295,53 +1163,10 @@ and matchCompInfo (oldfidx: int) (oldci: compinfo)
(* We get here when we succeeded checking that they are equal, or one of
* them was empty *)
newrep.ndata.cattr <- addAttributes oldci.cattr ci.cattr
- end
-
-(* Match two enuminfos and throw a Failure if they do not match *)
-and matchEnumInfo (oldfidx: int) (oldei: enuminfo)
- (fidx: int) (ei: enuminfo) : unit =
- (* Find the node for this enum, no path compression. *)
- let oldeinode = EnumMerging.getNode eEq eSyn oldfidx oldei oldei None
- in
- let einode = EnumMerging.getNode eEq eSyn fidx ei ei None in
- if oldeinode == einode then (* We already know they are the same *)
- ()
- else begin
- (* Replace with the representative data *)
- let oldei = oldeinode.ndata in
- let ei = einode.ndata in
- (* Try to match them. But if you cannot just make them both integers *)
- try
- have_same_enum_items oldei ei;
- (* Set the representative *)
- let newrep, _ = EnumMerging.union oldeinode einode in
- (* We get here if the enumerations match *)
- newrep.ndata.eattr <- addAttributes oldei.eattr ei.eattr;
- ()
- with Failure msg -> begin
- let pp_items = Pretty_utils.pp_list ~pre:"{" ~suf:"}" ~sep:",@ "
- (fun fmt item ->
- Format.fprintf fmt "%s=%a" item.eiorig_name
- Cil_printer.pp_exp item.eival)
- in
- if oldeinode != intEnumInfoNode && einode != intEnumInfoNode then
- Kernel.warning
- "@[merging definitions of enum %s using int type@ (%s);@ items %a and@ %a@]"
- oldei.ename msg
- pp_items oldei.eitems pp_items ei.eitems;
- (* Get here if you cannot merge two enumeration nodes *)
- if oldeinode != intEnumInfoNode then begin
- let _ = EnumMerging.union oldeinode intEnumInfoNode in ()
- end;
- if einode != intEnumInfoNode then begin
- let _ = EnumMerging.union einode intEnumInfoNode in ()
- end;
- end
- end
(* Match two typeinfos and throw a Failure if they do not match *)
-and matchTypeInfo (oldfidx: int) (oldti: typeinfo)
+let matchTypeInfoGen (combineF : combineFunction) (oldfidx: int) (oldti: typeinfo)
(fidx: int) (ti: typeinfo) : unit =
if oldti.tname = "" || ti.tname = "" then
Kernel.fatal "matchTypeInfo for anonymous type";
@@ -1350,7 +1175,7 @@ and matchTypeInfo (oldfidx: int) (oldti: typeinfo)
let tnode = PlainMerging.getNode tEq tSyn fidx ti.tname ti None in
if oldtnode == tnode then (* We already know they are the same *)
()
- else begin
+ else
(* Replace with the representative data *)
let oldti = oldtnode.ndata in
let oldfidx = oldtnode.nfidx in
@@ -1358,27 +1183,46 @@ and matchTypeInfo (oldfidx: int) (oldti: typeinfo)
let fidx = tnode.nfidx in
(* Check that they are the same *)
(try
- ignore (combineTypes CombineOther oldfidx oldti.ttype fidx ti.ttype);
- with Failure reason -> begin
- let msg =
- let oldname = oldti.tname in
- let name = ti.tname in
- if oldname = name
- then
- Format.sprintf
- "Definitions of type %s are not isomorphic. \
- Reason follows:@\n@?%s"
- oldname reason
- else
- Format.sprintf
- "Types %s and %s are not isomorphic. Reason follows:@\n@?%s"
- oldname name reason
- in
- raise (Failure msg)
- end);
- let _ = union oldtnode tnode in
- ()
- end
+ ignore (combineF.typ_combine combineF true
+ CombineOther oldfidx oldti.ttype fidx ti.ttype);
+ with (Cannot_combine reason | Failure reason) ->
+ let msg =
+ let oldname = oldti.tname in
+ let name = ti.tname in
+ if oldname = name
+ then
+ Format.sprintf
+ "Definitions of type %s are not isomorphic. \
+ Reason follows:@\n@?%s"
+ oldname reason
+ else
+ Format.sprintf
+ "Types %s and %s are not isomorphic. Reason follows:@\n@?%s"
+ oldname name reason
+ in
+ raise (Failure msg));
+ ignore(union oldtnode tnode)
+
+let combines = {
+ typ_combine = (fun a b -> combineTypesGen a ~strictInteger:false ~strictReturnTypes:b);
+ enum_combine = (fun _ oldfidx oldei fidx ei ->
+ matchEnumInfo oldfidx oldei fidx ei;
+ oldei);
+ comp_combine = (fun c oldfidx oldei fidx ei ->
+ matchCompInfoGen c oldfidx oldei fidx ei;
+ oldei);
+ name_combine = (fun c _ oldfidx oldei fidx ei ->
+ matchTypeInfoGen c oldfidx oldei fidx ei;
+ oldei);
+}
+
+let matchCompInfo = matchCompInfoGen combines
+
+let matchTypeInfo = matchTypeInfoGen combines
+
+let combineTypes = combines.typ_combine combines true
+
+(* Match two compinfos and throw a Failure if they do not match *)
let update_compinfo ci =
let node =
@@ -1701,7 +1545,7 @@ let oneFilePass1 (f:file) : unit =
combineTypes CombineOther
oldvinode.nfidx oldvi.vtype
!currentFidx vi.vtype, fst (union oldvinode vinode);
- with (Failure reason) -> begin
+ with (Cannot_combine reason | Failure reason) -> begin
(* If one of the variable is currently unused, we can ignore it.
If both are unused and only one is defined, we keep this one.
Otherwise, we keep the old variable by default. *)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index c3520bf16882dba358b2f0d1d0a857b41c3fa445..115b8742da569c5081af185a9d285086312f3802 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -400,7 +400,7 @@ let splitArrayAttributes =
List.partition
(fun a -> List.mem (attributeName a) qualifier_attributes)
-let rec typeAddAttributes a0 t =
+let rec typeAddAttributes ?(combine=addAttributes) a0 t =
begin
match a0 with
| [] ->
@@ -408,7 +408,7 @@ let rec typeAddAttributes a0 t =
t
| _ ->
(* anything else: add a0 to existing attributes *)
- let add (a: attributes) = addAttributes a0 a in
+ let add (a: attributes) = combine a0 a in
match t with
TVoid a -> TVoid (add a)
| TInt (ik, a) -> TInt (ik, add a)
@@ -5860,6 +5860,369 @@ let getCompField cinfo fieldName =
(fun fi -> fi.fname = fieldName)
(Option.value ~default:[] cinfo.cfields)
+let sameSizeInt (ik1 : ikind) (ik2 : ikind) =
+ match ik1, ik2 with
+ | (IChar | ISChar | IUChar), (IChar | ISChar | IUChar) -> true
+ | (IShort | IUShort), (IShort | IUShort) -> true
+ | (IInt | IUInt), (IInt | IUInt) -> true
+ | (ILong | IULong), (ILong | IULong) -> true
+ | (ILongLong | IULongLong), (ILongLong | IULongLong) -> true
+ | _ -> false
+
+
+let sameSign ?(machdep=false) (ik1 : ikind) (ik2 : ikind) =
+ if machdep then isSigned ik1 = isSigned ik2
+ else
+ match ik1, ik2 with
+ | IChar, (ISChar | IUChar)
+ | ISChar, (IChar | IUChar)
+ | IUChar, (IChar | ISChar) -> false
+ | _ -> isSigned ik1 = isSigned ik2
+
+let same_int64 ?(machdep=true) e1 e2 =
+ match constFoldToInt ~machdep e1, constFoldToInt ~machdep e2 with
+ | Some i, Some i' -> Integer.equal i i'
+ | _ -> false
+
+exception Cannot_combine of string
+
+type combineWhat =
+ CombineFundef of bool
+ (* The new definition is for a function definition. The old
+ * is for a prototype. arg is [true] for an old-style declaration *)
+ | CombineFunarg of bool
+ (* Comparing a function argument type with an old prototype argument.
+ arg is [true] for an old-style declaration, which
+ triggers some ad hoc treatment in GCC mode. *)
+ | CombineFunret (* Comparing the return of a function with that from an old
+ * prototype *)
+ | CombineOther
+
+(* [combineAttributes what olda a] combines the attributes in [olda] and [a]
+ according to [what]:
+ - if [what == CombineFunarg], then override old attributes;
+ this is used to ensure that attributes from formal argument types in a
+ function definition are not mixed with attributes from arguments in other
+ (compatible, but with different qualifiers) declarations;
+ - else, perform the union of old and new attributes. *)
+let combineAttributes what olda a =
+ match what with
+ | CombineFunarg _ -> a (* override old attributes with new ones *)
+ | _ -> addAttributes olda a (* union of attributes *)
+
+type combineFunction =
+ {
+ typ_combine : combineFunction ->
+ bool -> combineWhat -> int -> typ -> int -> typ -> typ;
+
+ enum_combine : combineFunction ->
+ int -> enuminfo -> int -> enuminfo -> enuminfo;
+
+ comp_combine : combineFunction ->
+ int -> compinfo -> int -> compinfo -> compinfo;
+
+ name_combine : combineFunction -> combineWhat ->
+ int -> typeinfo -> int -> typeinfo -> typeinfo;
+ }
+
+(* Combine the types. Raises the Cannot_combine exception with an error message.
+ [what] is used to recursively deal with function return types and function
+ arguments in special ways.
+ Note: we cannot force the qualifiers of oldt and t to be the same here,
+ because in some cases (e.g. string literals and char pointers) it is
+ allowed to have differences, while in others we want to be more strict. *)
+let combineTypesGen (combineF : combineFunction)
+ ?(strictInteger=true) ?(strictReturnTypes=false)
+ (what : combineWhat) (oldfidx : int) (oldt : typ) (fidx : int) (t : typ) : typ =
+ match oldt, t with
+ | TVoid olda, TVoid a -> TVoid (combineAttributes what olda a)
+
+ | _, TVoid _ when what = CombineFunret && not strictReturnTypes -> t
+
+ | TInt (oldik, olda), TInt (ik, a) ->
+ let result k oldk = if rank oldk<rank k then k else oldk in
+ let check_gcc_mode oldk k =
+ if gccMode () && oldk == IInt &&
+ bytesSizeOf t <= bytesSizeOfInt IInt &&
+ (what = CombineFunarg true || what = CombineFunret)
+ then k
+ else
+ let msg =
+ Format.asprintf
+ "different integer types:@ '%a' and '%a'"
+ Cil_datatype.Typ.pretty oldt Cil_datatype.Typ.pretty t in
+ raise (Cannot_combine msg)
+ in
+ let combineIK oldk k =
+ if oldk == k then oldk else
+ if not strictInteger
+ then
+ if sameSizeInt oldk k && sameSign ~machdep:false oldk k
+ then
+ (* The types contain the same sort of values but are not equal.
+ For example on x86_16 machdep unsigned short and unsigned int. *)
+ result k oldk
+ else
+ if bytesSizeOfInt oldk == bytesSizeOfInt k && isSigned oldk == isSigned k
+ then
+ begin
+ Kernel.warning ~current:true
+ "Integer compatibily is machine-dependant : %a and %a\n"
+ Cil_datatype.Typ.pretty oldt Cil_datatype.Typ.pretty t;
+ result k oldk
+ end
+ else
+ check_gcc_mode oldk k
+ else
+ check_gcc_mode oldk k
+ in
+ TInt (combineIK oldik ik, combineAttributes what olda a)
+
+ | TFloat (oldfk, olda), TFloat (fk, a) ->
+ let combineFK oldk k =
+ if oldk == k then oldk else
+ if gccMode () && oldk == FDouble && k == FFloat
+ && (what = CombineFunarg true || what = CombineFunret)
+ then k
+ else
+ raise (Cannot_combine "different floating point types")
+ in
+ TFloat (combineFK oldfk fk, combineAttributes what olda a)
+
+ | TEnum (oldei, olda), TEnum (ei, a) ->
+ (* Matching enumerations always succeeds. But sometimes it maps both
+ * enumerations to integers *)
+ TEnum (combineF.enum_combine combineF oldfidx oldei fidx ei,
+ combineAttributes what olda a)
+
+ (* Strange one. But seems to be handled by GCC *)
+ | TEnum (oldei, olda) , TInt(IInt, a) ->
+ TEnum(oldei, combineAttributes what olda a)
+
+ (* Strange one. But seems to be handled by GCC. Warning. Here we are
+ * leaking types from new to old *)
+ | TInt(IInt, olda), TEnum (ei, a) ->
+ TEnum(ei, combineAttributes what olda a)
+
+ | TComp (oldci, olda) , TComp (ci, a) ->
+ TComp(combineF.comp_combine combineF oldfidx oldci fidx ci,
+ combineAttributes what olda a)
+
+ | TArray (oldbt, oldsz, olda), TArray (bt, sz, a) ->
+ let newbt = combineF.typ_combine combineF strictReturnTypes
+ CombineOther oldfidx oldbt fidx bt in
+ let newsz =
+ match oldsz, sz with
+ | None, Some _ -> sz
+ | Some _, None -> oldsz
+ | None, None -> sz
+ | Some oldsz', Some sz' ->
+ (* They are not structurally equal. But perhaps they are equal if we
+ evaluate them. Check first machine independent comparison. *)
+ if same_int64 ~machdep:false oldsz' sz' then
+ oldsz
+ else if same_int64 ~machdep:true oldsz' sz' then begin
+ Kernel.warning ~current:true
+ "Array type comparison succeeds only based on machine-dependent \
+ constant evaluation: %a and %a\n"
+ Cil_datatype.Typ.pretty oldt Cil_datatype.Typ.pretty t;
+ oldsz
+ end else
+ raise (Cannot_combine "different array lengths")
+ in
+ TArray (newbt, newsz, combineAttributes what olda a)
+
+ | TPtr (oldbt, olda), TPtr (bt, a) ->
+ TPtr (combineF.typ_combine combineF strictReturnTypes
+ CombineOther oldfidx oldbt fidx bt,
+ combineAttributes what olda a)
+
+ | TFun (oldrt, oldargs, oldva, olda), TFun (rt, args, va, a) ->
+ let newrt = combineF.typ_combine combineF strictReturnTypes
+ CombineFunret oldfidx oldrt fidx rt in
+ if oldva != va then
+ raise (Cannot_combine "different vararg specifiers");
+ (* If one does not have arguments, believe the one with the
+ * arguments *)
+ let newargs, olda' =
+ if oldargs = None then args, olda else
+ if args = None then oldargs, olda else
+ let (oldargslist, oldghostargslist) = argsToPairOfLists oldargs in
+ let (argslist, ghostargslist) = argsToPairOfLists args in
+ if List.length oldargslist <> List.length argslist then
+ raise (Cannot_combine "different number of arguments")
+ else if List.length oldghostargslist <> List.length ghostargslist then
+ raise (Cannot_combine "different number of ghost arguments")
+ else begin
+ let oldargslist = oldargslist @ oldghostargslist in
+ let argslist = argslist @ ghostargslist in
+ (* Go over the arguments and update the old ones with the
+ * adjusted types *)
+ (* Format.printf "new type is %a@." Cil_datatype.Typ.pretty t; *)
+ let what =
+ match what with
+ | CombineFundef b -> CombineFunarg b
+ | _ -> CombineOther
+ in
+ Some
+ (List.map2
+ (fun (on, ot, oa) (an, at, aa) ->
+ (* Update the names. Always prefer the new name. This is
+ * very important if the prototype uses different names than
+ * the function definition. *)
+ let n = if an <> "" then an else on in
+ let t = combineF.typ_combine combineF strictReturnTypes
+ what oldfidx ot fidx at in
+ let a = addAttributes oa aa in
+ (n, t, a))
+ oldargslist argslist),
+ olda
+ end
+ in
+ (* Drop missingproto as soon as one of the type is a properly declared one*)
+ let olda =
+ if not (hasAttribute "missingproto" a) then
+ dropAttribute "missingproto" olda'
+ else olda'
+ in
+ let a =
+ if not (hasAttribute "missingproto" olda') then
+ dropAttribute "missingproto" a
+ else a
+ in
+ TFun (newrt, newargs, oldva, combineAttributes what olda a)
+
+ | TBuiltin_va_list olda, TBuiltin_va_list a ->
+ TBuiltin_va_list (combineAttributes what olda a)
+
+ | TNamed (oldt, olda), TNamed (t, a) ->
+ TNamed (combineF.name_combine combineF what oldfidx oldt fidx t,
+ combineAttributes what olda a)
+
+ | _, TNamed (t, a) ->
+ let res = combineF.typ_combine combineF strictReturnTypes what oldfidx oldt fidx t.ttype in
+ typeAddAttributes ~combine:(combineAttributes what) a res
+
+ | TNamed (oldt, olda), _ ->
+ let res = combineF.typ_combine combineF strictReturnTypes what oldfidx oldt.ttype fidx t in
+ typeAddAttributes ~combine:(combineAttributes what) olda res
+
+ | _ -> raise (Cannot_combine
+ (Format.asprintf "different type constructors:@ %a and %a"
+ Cil_datatype.Typ.pretty oldt Cil_datatype.Typ.pretty t))
+
+
+let default_combines = {
+ typ_combine = (fun c b -> combineTypesGen c ~strictInteger:true ~strictReturnTypes:b);
+ enum_combine = (fun _ _ _ _ ei -> ei);
+ comp_combine = (fun _ _ oldci _ ci ->
+ if oldci.cstruct <> ci.cstruct then
+ raise (Cannot_combine "different struct/union types");
+ if oldci.cname = ci.cname then
+ oldci
+ else
+ raise (Cannot_combine (Format.sprintf "%ss with different tags"
+ (if oldci.cstruct then "struct" else "union"))));
+ name_combine = (fun c what oldfidx oldt fidx t ->
+ if oldt.tname = t.tname then oldt
+ else
+ begin
+ ignore (c.typ_combine c false what oldfidx oldt.ttype fidx t.ttype);
+ oldt
+ end
+ );
+}
+
+
+let combineTypes ?(strictReturnTypes=false) (what: combineWhat) (oldt: typ) (t: typ) : typ =
+ let useless = 0 in
+ combineTypesGen default_combines ~strictReturnTypes what useless oldt useless t
+
+(***************** Compatibility ******)
+
+
+(* how type qualifiers must be checked *)
+type qualifier_check_context =
+ | Identical (* identical qualifiers. *)
+ | IdenticalToplevel (* ignore at toplevel, use Identical when going under a
+ pointer. *)
+ | Covariant (* first type can have const-qualifications
+ the second doesn't have. *)
+ | CovariantToplevel
+ (* accepts everything for current type, use Covariant when going under a
+ pointer. *)
+ | Contravariant (* second type can have const-qualifications
+ the first doesn't have. *)
+ | ContravariantToplevel
+ (* accepts everything for current type, use Contravariant when going under
+ a pointer. *)
+
+let qualifier_context_fun_arg = function
+ | Identical | IdenticalToplevel -> IdenticalToplevel
+ | Covariant | CovariantToplevel -> ContravariantToplevel
+ | Contravariant | ContravariantToplevel -> CovariantToplevel
+
+let qualifier_context_fun_ret = function
+ | Identical | IdenticalToplevel -> IdenticalToplevel
+ | Covariant | CovariantToplevel -> CovariantToplevel
+ | Contravariant | ContravariantToplevel -> ContravariantToplevel
+
+let qualifier_context_ptr = function
+ | Identical | IdenticalToplevel -> Identical
+ | Covariant | CovariantToplevel -> Covariant
+ | Contravariant | ContravariantToplevel -> Contravariant
+
+let included_qualifiers ?(context=Identical) a1 a2 =
+ let a1 = filter_qualifier_attributes a1 in
+ let a2 = filter_qualifier_attributes a2 in
+ let a1 = dropAttribute "restrict" a1 in
+ let a2 = dropAttribute "restrict" a2 in
+ let a1_no_cv = dropAttributes ["const"; "volatile"] a1 in
+ let a2_no_cv = dropAttributes ["const"; "volatile"] a2 in
+ let is_equal = Cil_datatype.Attributes.equal a1 a2 in
+ if is_equal then true
+ else begin
+ match context with
+ | Identical -> false
+ | Covariant -> Cil_datatype.Attributes.equal a1_no_cv a2
+ | Contravariant -> Cil_datatype.Attributes.equal a1 a2_no_cv
+ | CovariantToplevel | ContravariantToplevel | IdenticalToplevel -> true
+ end
+
+(* precondition: t1 and t2 must be "compatible" as per combineTypes, i.e.
+ you must have called [combineTypes t1 t2] before calling this function. *)
+let rec have_compatible_qualifiers_deep ?(context=Identical) t1 t2 =
+ match unrollType t1, unrollType t2 with
+ | TFun (tres1, Some args1, _, _), TFun (tres2, Some args2, _, _) ->
+ have_compatible_qualifiers_deep
+ ~context:(qualifier_context_fun_ret context) tres1 tres2 &&
+ let context = qualifier_context_fun_arg context in
+ List.for_all2 (fun (_, t1', a1) (_, t2', a2) ->
+ have_compatible_qualifiers_deep ~context t1' t2' &&
+ included_qualifiers ~context a1 a2)
+ args1 args2
+ | TPtr (t1', a1), TPtr (t2', a2)
+ | TArray (t1', _, a1), TArray (t2', _, a2) ->
+ (included_qualifiers ~context a1 a2) &&
+ let context = qualifier_context_ptr context in
+ have_compatible_qualifiers_deep ~context t1' t2'
+ | _, _ -> included_qualifiers ~context (typeAttrs t1) (typeAttrs t2)
+
+let compatibleTypes ?strictReturnTypes ?context t1 t2 =
+ let r = combineTypes ?strictReturnTypes CombineOther t1 t2 in
+ (* C99, 6.7.3 §9: "... to be compatible, both shall have the identically
+ qualified version of a compatible type;" *)
+ if not (have_compatible_qualifiers_deep ?context t1 t2) then
+ raise (Cannot_combine "different qualifiers");
+ (* Note: different non-qualifier attributes will be silently dropped. *)
+ r
+
+let areCompatibleTypes ?strictReturnTypes ?context t1 t2 =
+ try
+ ignore (compatibleTypes ?strictReturnTypes ?context t1 t2); true
+ with Cannot_combine _ -> false
+
+
let mkCastT ?(force=false) ~(oldt: typ) ~(newt: typ) e =
let loc = e.eloc in
(* Issue #!1546
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 92213780da74fc591c8a36209b7b0053ab2868b3..259b8ea9d7a7b15ed621ee0e82d9290979e3be70 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -862,6 +862,80 @@ val isIntegerConstant: ?is_varinfo_cst:(varinfo -> bool) -> exp -> bool
*)
val isConstantOffset: ?is_varinfo_cst:(varinfo -> bool) -> offset -> bool
+
+exception Cannot_combine of string
+
+
+type combineWhat =
+ CombineFundef of bool
+ (* The new definition is for a function definition. The old
+ * is for a prototype. arg is [true] for an old-style declaration *)
+ | CombineFunarg of bool
+ (* Comparing a function argument type with an old prototype argument.
+ arg is [true] for an old-style declaration, which
+ triggers some ad hoc treatment in GCC mode. *)
+ | CombineFunret (* Comparing the return of a function with that from an old
+ * prototype *)
+ | CombineOther
+
+(** [combineAttributes what olda a] combines the attributes in [olda] and [a]
+ according to [what]:
+ - if [what == CombineFunarg], then override old attributes;
+ this is used to ensure that attributes from formal argument types in a
+ function definition are not mixed with attributes from arguments in other
+ (compatible, but with different qualifiers) declarations;
+ - else, perform the union of old and new attributes. **)
+val combineAttributes : combineWhat -> attribute list -> attributes -> attributes
+
+
+(** [combineFunction] contains informations about how enum, struct/union and typedef
+ should be handled. *)
+type combineFunction =
+ {
+ typ_combine :
+ combineFunction -> bool -> combineWhat -> int -> typ -> int -> typ -> typ;
+ enum_combine :
+ combineFunction -> int -> enuminfo -> int -> enuminfo -> enuminfo;
+ comp_combine :
+ combineFunction -> int -> compinfo -> int -> compinfo -> compinfo;
+ name_combine :
+ combineFunction -> combineWhat -> int -> typeinfo -> int -> typeinfo -> typeinfo;
+ }
+
+(** [combineTypesGen] combine two types accordingly to the combineFunction argument.
+ If types cannot be combine, it throw an exception. *)
+val combineTypesGen : combineFunction -> ?strictInteger:bool ->
+ ?strictReturnTypes:bool -> combineWhat -> int -> typ -> int -> typ -> typ
+
+(** Specialized verison of [combineTypesGen], we suppore here that
+ if two global symbols are equal, then they are the same object. *)
+val combineTypes : ?strictReturnTypes:bool -> combineWhat -> typ -> typ -> typ
+
+(* how type qualifiers must be checked *)
+type qualifier_check_context =
+ | Identical (* identical qualifiers. *)
+ | IdenticalToplevel (* ignore at toplevel, use Identical when going under a
+ pointer. *)
+ | Covariant (* first type can have const-qualifications
+ the second doesn't have. *)
+ | CovariantToplevel
+ (* accepts everything for current type, use Covariant when going under a
+ pointer. *)
+ | Contravariant (* second type can have const-qualifications
+ the first doesn't have. *)
+ | ContravariantToplevel
+ (* accepts everything for current type, use Contravariant when going under
+ a pointer. *)
+
+(** [areCompatibleTypes] returns [true] if two types are compatible *)
+val areCompatibleTypes :
+ ?strictReturnTypes:bool -> ?context:qualifier_check_context -> typ -> typ -> bool
+
+(** same as [areCompatibleTypes] but returns the combined version *)
+val compatibleTypes :
+ ?strictReturnTypes:bool -> ?context:qualifier_check_context -> typ -> typ -> typ
+
+
(** True if the given expression is a (possibly cast'ed) integer or character
constant with value zero *)
val isZero: exp -> bool
@@ -930,6 +1004,13 @@ val constFoldBinOp: loc:location -> bool -> binop -> exp -> exp -> typ -> exp
*)
val compareConstant: constant -> constant -> bool
+
+(** [true] if two kinds have the same size independently of the machine.*)
+val sameSizeInt : ikind -> ikind -> bool
+
+(** [true] if the result of two expressions are two equal integers. *)
+val same_int64 : ?machdep:bool -> exp -> exp -> bool
+
(** Increment an expression. Can be arithmetic or pointer type *)
val increm: exp -> int -> exp
@@ -1338,7 +1419,8 @@ val typeAttr: typ -> attribute list
val setTypeAttrs: typ -> attributes -> typ
(** Add some attributes to a type *)
-val typeAddAttributes: attribute list -> typ -> typ
+val typeAddAttributes: ?combine: (attribute list -> attributes -> attributes) ->
+ attribute list -> typ -> typ
(** Remove all attributes with the given names from a type. Note that this
does not remove attributes from typedef and tag definitions, just from