module Interval:sig
..end
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
ival =
| |
Ival of |
| |
Float of |
| |
Rational |
| |
Real |
| |
Nan |
include Datatype.S_with_collections
val is_included : t -> t -> bool
val join : t -> t -> t
val meet : t -> t -> t
val widen : t -> t
val is_singleton_int : t -> bool
val top_ival : t
val ival : Integer.t -> Integer.t -> t
val extract_ival : t -> Ival.t
assume Ival _
as argument
val ikind_of_ival : Ival.t -> Cil_types.ikind
Cil.Not_representable
if the given interval does not fit into any C
integral type.val interv_of_typ : Cil_types.typ -> t
Is_a_real
if the given type is a float type.Not_a_number
if the given type does not represent any number.val extended_interv_of_typ : Cil_types.typ -> t
Is_a_real
if the given type is a float type.Not_a_number
if the given type does not represent any number.n..m+1
when interv_of_typ returns n..m
.
It is in particular useful for computing bounds of quantified variables.module Env:sig
..end
Environment which maps logic variables to intervals.
val infer : Cil_types.term -> t
infer t
infers the smallest possible integer interval which the values
of the term can fit in.
Is_a_real
if the term is either a float or a real.Not_a_number
if the term does not represent any number.