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



Useful operations on intervals


exception Not_an_integer
val interv_of_typ : Cil_types.typ -> Ival.t
Raises Not_an_integer if the given type is not an integral type.
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 -> Ival.t
infer t infers the smallest possible integer interval which the values of the term can fit in.
Raises Not_an_integer if the type of the term is not a subtype of Linteger.