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 : |
|
i_signed : |
}
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 |
| |
TSPtr of |
| |
TSFloat of |
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