Newer
Older
(**************************************************************************)
(* *)
(* Copyright (C) 2007-2017 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
(** 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 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\];
Note: this is a partial wrapper on top of [Ival.t], to which most
functions are delegated. *)
(* ************************************************************************** *)
(** {3 Useful operations on intervals} *)
(* ************************************************************************** *)
val interv_of_typ: Cil_types.typ -> Ival.t
(** @return the smallest interval which contains the given C type.
@raise Not_an_integer if the given type is not an integral type. *)
(* ************************************************************************** *)
(** {3 Environment for interval computations} *)
(* ************************************************************************** *)
(** Environment which maps logic variables to intervals. This environment must
be extended from outside. *)
module Env: sig
val clear: unit -> unit
val add: Cil_types.logic_var -> Ival.t -> unit
(* ************************************************************************** *)
(* ************************************************************************** *)
val infer: Cil_types.term -> Ival.t
(** [infer t] infers the smallest possible integer interval which the values
@raise Not_an_integer if the type of the term is not a subtype of
[Linteger]. *)
(*
Local Variables:
compile-command: "make"
End:
*)