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 is_singleton_int : t -> bool
val extract_ival : t -> Frama_c_kernel.Ival.t
assume Ival _
as argument
val ikind_of_ival : Frama_c_kernel.Ival.t -> Frama_c_kernel.Cil_types.ikind
val interv_of_typ : Frama_c_kernel.Cil_types.typ -> t
val extended_interv_of_typ : Frama_c_kernel.Cil_types.typ -> t
val plus_one : Analyses_types.ival -> Analyses_types.ival
val get_from_profile :
profile:Analyses_datatype.Profile.t ->
Frama_c_kernel.Cil_types.term ->
t
val get :
logic_env:Analyses_datatype.Logic_env.t ->
Frama_c_kernel.Cil_types.term ->
t
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 get_widened_profile :
Analyses_datatype.Profile.t ->
Frama_c_kernel.Cil_types.logic_info ->
Analyses_datatype.Profile.t