From fdcf6a8cac3c96736d30a574a86c33757ab6eadb Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 1 Mar 2019 16:39:16 +0100
Subject: [PATCH] a bit of comments
---
src/plugins/e-acsl/interval.ml | 14 ++++++++++----
src/plugins/e-acsl/interval_system.ml | 6 +++++-
2 files changed, 15 insertions(+), 5 deletions(-)
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index 08f59cbf348..7dcf07af3b4 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -79,8 +79,14 @@ let interv_of_unknown_block =
(Ival.inject_range (Some Integer.zero) (Some (Bit_utils.max_byte_address ())))
(* imperative environments *)
-
-module Env = struct
+module Env: sig
+ val clear: unit -> unit
+ val add: Cil_types.logic_var -> Ival.t -> unit
+ val find: Cil_types.logic_var -> Ival.t
+ val remove: Cil_types.logic_var -> unit
+ val replace: Cil_types.logic_var -> Ival.t -> unit
+ val find_all: Cil_types.logic_var -> Ival.t list
+end = struct
open Cil_datatype
let tbl: Ival.t Logic_var.Hashtbl.t = Logic_var.Hashtbl.create 7
let clear () = Logic_var.Hashtbl.clear tbl
@@ -360,6 +366,7 @@ and build_ieqs t ieqs ivars =
let args_lty = List.map2
(fun lv arg ->
try
+ (* speed-up convergence *)
let i = interv_of_typ_containing_interv (infer arg) in
Env.add lv i;
Ctype (TInt(ikind_of_interv i, []))
@@ -371,8 +378,7 @@ and build_ieqs t ieqs ivars =
in
(* x *)
let ivar =
- { Interval_system.iv_name = li.l_var_info.lv_name;
- iv_types = args_lty }
+ { Interval_system.iv_name = li.l_var_info.lv_name; iv_types = args_lty }
in
(* Adding x = g(x) if it is not yet in the system of equations.
Without this check, the algorithm would not terminate. *)
diff --git a/src/plugins/e-acsl/interval_system.ml b/src/plugins/e-acsl/interval_system.ml
index 9ad95cf582b..32292572679 100644
--- a/src/plugins/e-acsl/interval_system.ml
+++ b/src/plugins/e-acsl/interval_system.ml
@@ -28,7 +28,11 @@ open Cil_types
type ival_binop = Ival_add | Ival_min | Ival_mul | Ival_div | Ival_union
-type ivar = { iv_name: string; iv_types: logic_type list }
+type ivar =
+ (* it would be possible to get more precise results by storing an ival for
+ each argument instead of a logic type, but the system would converge too
+ slowly to a solution. *)
+ { iv_name: string; iv_types: logic_type list }
type ival_exp =
| Iconst of Ival.t
--
GitLab