From c8f85d9f013fde0ee6497730f3161d35ff3358da Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 1 Mar 2019 17:27:38 +0100
Subject: [PATCH] comments
---
src/plugins/e-acsl/interval_system.ml | 7 +++----
1 file changed, 3 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/interval_system.ml b/src/plugins/e-acsl/interval_system.ml
index fe18fccc670..ca1b35a69e2 100644
--- a/src/plugins/e-acsl/interval_system.ml
+++ b/src/plugins/e-acsl/interval_system.ml
@@ -124,10 +124,10 @@ let build ~infer t =
let args_lty = List.map2
(fun lv arg ->
try
- (* speed-up convergence *)
+ (* speed-up convergence; because of this approximation, no need to
+ associate [i] to [lv] in [Interval.Env]: the very same interval
+ will be computed anyway. *)
let i = interv_of_typ_containing_interv (infer arg) in
- (* TODO: *)
-(* Env.add lv i;*)
Ctype (TInt(ikind_of_interv i, []))
with
| Cil.Not_representable -> Linteger
@@ -151,7 +151,6 @@ let build ~infer t =
let ieqs = Ivar.Map.add ivar iexp ieqs in
ieqs, ivars
in
-(* List.iter (fun lv -> Env.remove lv) li.l_profile;*)
Ivar ivar, ieqs, ivars
end else
(try Iconst(infer t), ieqs, ivars
--
GitLab