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 ty_of_interv : ?ctx:Analyses_types.number_ty -> ?use_gmp_opt:bool -> t -> Analyses_types.number_ty
val is_included_in_typ : Analyses_types.ival -> Frama_c_kernel.Cil_types.typ -> bool

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

val joins_from_profile : profile:Analyses_datatype.Profile.t -> Frama_c_kernel.Cil_types.term list -> t

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