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:
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
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 =
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