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 of |
| |
Float of |
| |
Rational |
| |
Real |
| |
Nan |
typet =ival
val is_included : t -> t -> bool
val join : t -> t -> t
val meet : t -> t -> t
val widen : t -> tval is_singleton_int : t -> bool
val extract_ival : t -> Ival.tassume Ival _ as argument
val ikind_of_ival : Ival.t -> Cil_types.ikindCil.Not_representable if the given interval does not fit into any C
integral type.val interv_of_typ : Cil_types.typ -> tIs_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 -> tIs_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 -> tinfer 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.