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 implement Figure 3 of J. Signoles' JFLA'15 paper "Rester statique pour devenir plus rapide, plus précis et plus mince".
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.
exception Not_an_integer
val ikind_of_interv : 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 -> Ival.t
Not_an_integer
if the given type is not an integral type.module Env:sig
..end
Environment which maps logic variables to intervals.
val infer : Cil_types.term -> Ival.t
infer t
infers the smallest possible integer interval which the values
of the term can fit in.
Not_an_integer
if the type of the term is not a subtype of
Linteger
.