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
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
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 * 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 = 
| TSInt of integer_range
| TSPtr of integer_range
| TSFloat of Cil_types.fkind
| TSNotScalar
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