Frama-C:
Plug-ins:
Libraries:

Frama-C API - Eval_typ

Functions related to type conversions

Size of the type of a lval, taking into account that the lval might have been a bitfield.

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.

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 integer_range = {
  1. i_bits : int;
  2. i_signed : bool;
}

Abstraction of an integer type, more convenient than an ikind because it can also be used for bitfields.

Range for an integer type with some attributes. The attribute Ast_attributes.bitfield_attribute_name influences the width of the type.

val pointer_range : unit -> integer_range

Range for a pointer type.

val range_inclusion : integer_range -> integer_range -> bool

Checks inclusion of two integer ranges.

val range_lower_bound : integer_range -> Frama_c_kernel.Z.t
val range_upper_bound : integer_range -> Frama_c_kernel.Z.t
type scalar_typ =
  1. | TSInt of integer_range
  2. | TSPtr of integer_range
  3. | TSFloat of Frama_c_kernel.Cil_types.fkind

Abstraction of scalar types -- in particular, all those that can be involved in a cast. Enum and integers are coalesced.

val classify_as_scalar : Frama_c_kernel.Cil_types.typ -> scalar_typ option
val integer_range : ptr:bool -> Frama_c_kernel.Cil_types.typ -> integer_range option