package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Interval inference for terms.

Compute the smallest interval that contains all the possible values of a given integer term. The interval of C variables is directly inferred from their C type. The interval of logic variables must be registered from outside before computing the interval of a term containing such variables (see module Interval.Env).

It implements Figure 3 of J. Signoles' JFLA'15 paper "Rester statique pour devenir plus rapide, plus précis et plus mince". Also implements a partial support for real numbers.

Example: consider a variable x of type int on a (strange) architecture in which values of type int belongs to the interval [-128;127] and a logic variable y which was registered in the environment with an interval [-32;31]. Then here are the intervals computed from the term 1+(x+1)/(y-64): 1. x in [128;127]; 2. x+1 in [129;128]; 3. y in [-32;31]; 4. y-64 in [-96;-33]; 5. (x+1)/(y-64) in [-3;3]; 6. 1+(x+1)/(y-64) in [-2;4]

Note: this is a partial wrapper on top of Ival.t, to which most functions are delegated.

Useful operations on intervals

val is_included : t -> t -> bool
val join : t -> t -> t
val meet : t -> t -> t
val widen : t -> t
  • returns

    the smallest interval containing a disjoint union of intervals

val is_singleton_int : t -> bool
val extract_ival : t -> Frama_c_kernel.Ival.t

assume Ival _ as argument

  • returns

    the smallest ikind that contains the given interval.

  • raises Cil.Not_representable

    if the given interval does not fit into any C integral type.

val interv_of_typ : Frama_c_kernel.Cil_types.typ -> t
  • returns

    the smallest interval which contains the given C type.

  • raises Is_a_real

    if the given type is a float type.

  • raises Not_a_number

    if the given type does not represent any number.

val extended_interv_of_typ : Frama_c_kernel.Cil_types.typ -> t
  • returns

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

  • raises Is_a_real

    if the given type is a float type.

  • raises Not_a_number

    if the given type does not represent any number.

  • returns

    the result of adding one to an interval. This is because when we have a condition x<t, we need to generate t+1

Inference system

val get_from_profile : profile:Analyses_datatype.Profile.t -> Frama_c_kernel.Cil_types.term -> t
  • returns

    the value computed by the interval inference phase

  • raises Is_a_real

    if the term is either a float or a real.

  • raises Not_a_number

    if the term does not represent any number.

  • returns

    the value computed by the interval inference phase, same as get_from_profile but with a full-fledged logic environment instead of a function profile

Interval processing

val infer_program : Frama_c_kernel.Cil_types.file -> unit

compute and store the type of all the terms that will be translated in a program

val preprocess_predicate : logic_env:Analyses_datatype.Logic_env.t -> Frama_c_kernel.Cil_types.predicate -> unit

compute and store the type of all the terms in a code annotation

val preprocess_code_annot : logic_env:Analyses_datatype.Logic_env.t -> Frama_c_kernel.Cil_types.code_annotation -> unit

compute and store the type of all the terms in a code annotation

val preprocess_term : logic_env:Analyses_datatype.Logic_env.t -> Frama_c_kernel.Cil_types.term -> unit
val clear : unit -> unit
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