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
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 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
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