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.
type
fct_pointer_compatibility =
| |
Compatible |
| |
Incompatible |
| |
Incompatible_but_accepted |
val compatible_functions : typ_pointed:Cil_types.typ ->
typ_fun:Cil_types.typ -> fct_pointer_compatibility
Test that two functions types are compatible; used to verify that a call
through a function pointer is ok. In theory, we could only check that
both types are compatible as defined by C99, 6.2.7. However, some industrial
codes do not strictly follow the norm, and we must be more lenient.
Thus, we return Incompatible_but_accepted
if Value can ignore more or
less safely the incompatibleness in the types.
val resolve_functions : typ_pointer:Cil_types.typ ->
Cvalue.V.t -> Kernel_function.Hptset.t Eval.or_top * bool
given
(funs, warn) = resolve_functions typ v
,
funs
is the set of
functions pointed to by
v
that have a type compatible with
typ
.
Compatibility is interpreted in a relaxed way, using
Eval_typ.compatible_functions
.
warn
indicates that at least one value of
v
was not a function, or was a function with a type incompatible with
v
;
for
warn
, compatibility is interpreted in a strict way.
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 (or the l-value itself for lval_contains_volatile
) has
volatile qualifier. Relational analyses should not learn anything on
such values.
val kf_assigns_only_result_or_volatile : Cil_types.kernel_function -> bool
returns true
if the function assigns only \result
or variables
that have volatile
qualifier (that are usually not tracked by domains
anyway).
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 * bool
Check inclusion of two integer ranges. Returns two boolean ok_low, ok_up
,
for inclusion of the low and upper ranges respectively.
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