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

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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct