Frama-C:
Plug-ins:
Libraries:

Frama-C API - Interval_utils

val is_included : Analyses_types.ival -> Analyses_types.ival -> bool
val is_singleton_int : Analyses_types.ival -> bool
val bottom : Analyses_types.ival
val top_ival : Analyses_types.ival
val singleton_of_int : int -> Analyses_types.ival
val interv_of_unknown_block : Analyses_types.ival lazy_t
  • returns

    the smallest interval containing a disjoint union of intervals

lift a unary operation on IVal.t to the type ival

Lift a binary operation on IVal.t to the type ival

val extract_ival : Analyses_types.ival -> Frama_c_kernel.Ival.t option
  • returns

    Some ival if argument is Ival ival

  • returns

    the smallest interval which contains the given C type.

val extended_interv_of_typ : Frama_c_kernel.Cil_types.typ -> Analyses_types.ival
  • returns

    the interval n..m+1 when interv_of_typ returns n..m. It is in particular useful for computing bounds of quantified variables.

  • returns

    the smallest interval which contains the given logic type.

exception Not_representable_ival

raised by ikind_of_ival.

  • since 28.0-Nickel
  • returns

    the smallest ikind that contains the given interval.