module Eval_typ: sig
.. end
Functions related to type conversions
Functions related to type conversions
val is_bitfield : Cil_types.typ -> bool
Bitfields
val bitfield_size : Cil_types.typ -> Integer.t option
val cast_lval_if_bitfield : Cil_types.typ -> Int_Base.t -> Cvalue.V.t -> Cvalue.V.t
if needed, cast the given abstract value to the given size. Useful
to handle bitfield. The type given as argument must be the type of
the l-value the abstract value is written into, which is of size size
.
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
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.