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 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
val interv_of_typ : Cil_types.typ -> t
val extended_interv_of_typ : Cil_types.typ -> t

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.