package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Inference system
Interval processing

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-28.0-Nickel.tar.gz

sha256=29612882330ecb6eddd0b4ca3afc0492b70d0feb3379a1b8e893194c6e173983

doc/frama-c-e-acsl.core/E_ACSL/Interval/index.html

Module `E_ACSL.Interval`

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.

type t = Analyses_types.ival

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.

val get : 
  logic_env:Analyses_datatype.Logic_env.t ->
  Frama_c_kernel.Cil_types.term ->
  t

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

val joins : 
  logic_env:Analyses_datatype.Logic_env.t ->
  Frama_c_kernel.Cil_types.term list ->
  t

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

val get_ival : 
  logic_env:Analyses_datatype.Logic_env.t ->
  Frama_c_kernel.Cil_types.term ->
  Frama_c_kernel.Ival.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