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:

o contains a single scalar binding, of the expected scalar type t (float or integer)
o contains multiple bindings, pointers, etc.
t is not a scalar type.

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