Module Interval

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.



Useful operations on intervals


type ival = 
| Ival of Ival.t
| Float of Cil_types.fkind * float option
| Rational
| Real
| Nan
include Datatype.S_with_collections
val is_included : t -> t -> bool
val join : t -> t -> t
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
Raises Cil.Not_representable if the given interval does not fit into any C integral type.
Returns the smallest ikind that contains the given interval.
val interv_of_typ : Cil_types.typ -> t
Raises Returns the smallest interval which contains the given C type.

Environment for interval computations


module Env: sig .. end
Environment which maps logic variables to intervals.

Inference system


val infer : Cil_types.term -> t
infer t infers the smallest possible integer interval which the values of the term can fit in.
Raises