Module Eval_typ

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