diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index dfc1b52ca6d916ee183aa30ebfa8880a2687a914..0569e4814b1d0efc4a7114951029407bc4e2b70a 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -192,38 +192,7 @@ let rec infer t =
(* TODO: should not be necessary to distinguish the recursive case.
Stack overflow if not distingued *)
if Misc.is_recursive li then
- (* 1) Build a system of interval equations that constrain the
- solution: do so by returning a variable when encoutering a call
- of a recursive function instead of performing the usual interval
- inference.
-
- BEWARE: we might be tempted to memoize the solution for a given
- function signature HOWEVER: it cannot be done in a straightforward
- manner due to the cases of functions that use C (global) variables
- in their definition (as the values of those variables can change
- between two function calls).
-
- TODO: I do not understand the remark above. The interval of a C
- global variable is computed from its type. *)
- let iexp, ieqs = Interval_system.build ~infer t in
- (* 2) Solve it:
- The problem is probably undecidable in the general case.
- Thus we just look for reasonably precise approximations
- without being too computationally expensive:
- simply iterate over a finite set of pre-defined intervals.
- See [Interval_system_solver.solve] for details. *)
- let chain_of_ivalmax =
- [| Integer.one; Integer.billion_one; Integer.max_int64 |]
- (* This set can be changed based on experimental evidences,
- but it works fine for now. *)
- in
- match iexp with
- | Interval_system.Ivar ivar ->
- Interval_system.solve ieqs ivar chain_of_ivalmax
- | Interval_system.Iconst _
- | Interval_system.Ibinop _
- | Interval_system.Iunsupported ->
- assert false
+ Interval_system.build_and_solve ~infer t
else begin (* non-recursive case *)
(* add the arguments to the context *)
List.iter2
diff --git a/src/plugins/e-acsl/interval_system.ml b/src/plugins/e-acsl/interval_system.ml
index ca1b35a69e283e918c78709bcb7ec3dc0e5b5a72..8fb99106e321221a46ca36171b6ac4980aae7f05 100644
--- a/src/plugins/e-acsl/interval_system.ml
+++ b/src/plugins/e-acsl/interval_system.ml
@@ -59,8 +59,6 @@ module Ivar =
let hash iv = Datatype.String.hash iv.iv_name + 7 * LT_List.hash iv.iv_types
end)
-type t = ival_exp Ivar.Map.t
-
(**************************************************************************)
(***************************** Solver *************************************)
(**************************************************************************)
@@ -184,8 +182,7 @@ let build ~infer t =
| _ ->
Iunsupported, ieqs, ivars
in
- let iexp, ieqs, _ = aux Ivar.Map.empty [] t in
- iexp, ieqs
+ aux Ivar.Map.empty [] t
(* Normalize the expression.
@@ -331,3 +328,31 @@ let solve ieqs ivar chain_of_ivalmax =
iterate_till_post_fixpoint ieqs bottom chain_of_ivalmax
in
get_ival_of_iconst ivar post_fixpoint
+
+let build_and_solve ~infer t =
+ (* 1) Build a system of interval equations that constrain the solution: do so
+ by returning a variable when encoutering a call of a recursive function
+ instead of performing the usual interval inference.
+
+ BEWARE: we might be tempted to memoize the solution for a given function
+ signature HOWEVER: it cannot be done in a straightforward manner due to the
+ cases of functions that use C (global) variables in their definition (as
+ the values of those variables can change between two function calls).
+
+ TODO: I do not understand the remark above. The interval of a C global
+ variable is computed from its type. *)
+ let iexp, ieqs, _ = build ~infer t in
+ (* 2) Solve it:
+ The problem is probably undecidable in the general case.
+ Thus we just look for reasonably precise approximations
+ without being too computationally expensive:
+ simply iterate over a finite set of pre-defined intervals.
+ See [Interval_system_solver.solve] for details. *)
+ let chain_of_ivalmax =
+ [| Integer.one; Integer.billion_one; Integer.max_int64 |]
+ (* This set can be changed based on experimental evidences,
+ but it works fine for now. *)
+ in
+ match iexp with
+ | Ivar ivar -> solve ieqs ivar chain_of_ivalmax
+ | Iconst _ | Ibinop _ | Iunsupported -> assert false
diff --git a/src/plugins/e-acsl/interval_system.mli b/src/plugins/e-acsl/interval_system.mli
index 8487d396fc74746fea225cd5fbfdc1ca52a0e61c..af842bd2ae69ddee0aee17cb4d4ffa6d78011a2c 100644
--- a/src/plugins/e-acsl/interval_system.mli
+++ b/src/plugins/e-acsl/interval_system.mli
@@ -22,64 +22,17 @@
open Cil_types
-(** Fixpoint equation solver for infering intervals of
- recursively defined logic functions *)
+(** Fixpoint equation solver for infering intervals of recursively defined logic
+ functions. *)
-(**************************************************************************)
-(******************************* Types ************************************)
-(**************************************************************************)
-
-type ival_binop = Ival_add | Ival_min | Ival_mul | Ival_div | Ival_union
-
-(* variables of the system represents functions of a given names and types for
- its parameters.
- No need to store the type of the return value since it is computable from the
- type of its parameters. *)
-type ivar = { iv_name: string; iv_types: logic_type list }
-
-type ival_exp =
- | Iconst of Ival.t
- | Ivar of ivar
- | Ibinop of ival_binop * ival_exp * ival_exp
- | Iunsupported
-
-type t
-(** type of systems of equations over [ival_exp] expressions in which the
- variables to be found are the [Ivar] constructs. [Equations.t] can be viewed
- as a fixpoint equation in the sense that the left-hand side of the equation
- MUST be an [Ivar]: solving the system [(S): x1=f1(x1, ..., xn) /\ ... /\
- xn=fn(x1, ..., xn)] is equivalent to solving the fixpoint equation [(E):
- X=F(X)] where X=(x1, ..., xn) and F=(f1, ..., fn). *)
-
-(**************************************************************************)
-(*************************** Constructors *********************************)
-(**************************************************************************)
-
-val build: infer:(term -> Ival.t) -> term -> ival_exp * t
-
-(**************************************************************************)
-(***************************** Solver *************************************)
-(**************************************************************************)
-
-val solve: t -> ivar -> Integer.t array -> Ival.t
-(** [solve ieqs ivar chain] finds an interval for the variable [ivar]
- that satisfies the fixpoint equation [ieqs]. The solver is parameterized
- by the increasingly sorted array [chain] of positive integers.
- For chain=[n1; n2; ...; nk] where n1 < ... < nk, [solve] will
- consider the following set S of intervals as potential solution:
- S={[-n1, n1], [-n2, n2]... [-nk; nk]}. Then [solve] will iteratively
- affect intervals from S to the different variables of [ieqs],
- starting from the smallest interval [-n1, n1] to the biggest one [-nk,
- nk], until finding the smallest combination that satisfies [ieqs].
- If no combination is found then [solve] returns Z. *)
-
-(**************************************************************************)
-(****************************** Utils *************************************)
-(**************************************************************************)
+val build_and_solve: infer:(term -> Ival.t) -> term -> Ival.t
+(** @return the interval of the given term denoting a recursive function. *)
-(* the following functions should be defined in [Interval] but are here to break
- mutual module dependencies *)
+(*/*)
+(** The following functions should be defined in [Interval] but are here to
+ break mutual module dependencies *)
exception Not_an_integer
val interv_of_typ: typ -> Ival.t
val ikind_of_interv: Ival.t -> Cil_types.ikind
+(*/*)