Module Eval_typ

module Eval_typ: sig .. end

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