Module Eval_typ

module Eval_typ: sig .. end
Functions related to type conversions


Functions related to type conversions
val is_bitfield : Cil_types.typ -> bool
Bitfields
val sizeof_lval_typ : Cil_types.typ -> Int_Base.t
Size of the type of a lval, taking into account that the lval might have been a bitfield.
val offsetmap_matches_type : Cil_types.typ -> Cvalue.V_Offsetmap.t -> bool
offsetmap_matches_type t o returns true if either:
val need_cast : Cil_types.typ -> Cil_types.typ -> bool
return true if the two types are statically distinct, and a cast from one to the other may have an effect on an abstract value.
val compatible_functions : Cil_types.typ ->
?args:Cil_types.exp list ->
Kernel_function.t list -> Kernel_function.t list * bool
val expr_contains_volatile : Cil_types.exp -> bool
val lval_contains_volatile : Cil_types.lval -> bool
Those two expressions indicate that one l-value contained inside the arguments (and the l-value itself for lval_contains_volatile) has volatile qualifier. Relational analyses should not learn anything on such values.
type integer_range = {
   i_bits : int;
   i_signed : bool;
}
Abstraction of an integer type, more convenient than an ikind because it can also be used for bitfields.
module DatatypeIntegerRange: Datatype.S  with type t = integer_range
val ik_range : Cil_types.ikind -> integer_range
val ik_attrs_range : Cil_types.ikind -> Cil_types.attributes -> integer_range
Range for an integer type with some attributes. The attribute Cil.bitfield_attribute_name influences the width of the type.
val range_inclusion : integer_range -> integer_range -> bool
Checks inclusion of two integer ranges.
val range_lower_bound : integer_range -> Integer.t
val range_upper_bound : integer_range -> Integer.t
type scalar_typ = 
| TSInt of integer_range
| TSPtr of integer_range
| TSFloat of Cil_types.fkind
Abstraction of scalar types -- in particular, all those that can be involved in a cast. Enum and integers are coalesced.
val classify_as_scalar : Cil_types.typ -> scalar_typ option