package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
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

assume Ival _ as argument

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