From 2ed8d4cbd6b19ef0058c6826e4d68ecae18efd53 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 29 Jul 2021 12:08:58 +0200
Subject: [PATCH] [Eva] Minor simplifications following the rewriting of Hptmap
shapes.
---
.../abstract_interp/lmap_bitwise.ml | 7 ++-----
src/plugins/value/domains/equality/equality.ml | 6 ++----
src/plugins/value/domains/gauges/gauges_domain.ml | 14 ++++----------
3 files changed, 8 insertions(+), 19 deletions(-)
diff --git a/src/kernel_services/abstract_interp/lmap_bitwise.ml b/src/kernel_services/abstract_interp/lmap_bitwise.ml
index dc01c40ef68..c908fe0f617 100644
--- a/src/kernel_services/abstract_interp/lmap_bitwise.ml
+++ b/src/kernel_services/abstract_interp/lmap_bitwise.ml
@@ -404,11 +404,8 @@ struct
let empty_left _ = empty (* zone over which to fold is empty *) in
let empty_right z = empty_map z in
let both b itvs map_b = conv b (both itvs map_b) in
- let fmap =
- Zone.fold2_join_heterogeneous
- ~cache ~empty_left ~empty_right ~both ~join ~empty
- in
- fun z m -> fmap z m
+ Zone.fold2_join_heterogeneous
+ ~cache ~empty_left ~empty_right ~both ~join ~empty
let shape x = x
diff --git a/src/plugins/value/domains/equality/equality.ml b/src/plugins/value/domains/equality/equality.ml
index e16da63d329..b7c63e5652b 100644
--- a/src/plugins/value/domains/equality/equality.ml
+++ b/src/plugins/value/domains/equality/equality.ml
@@ -415,9 +415,7 @@ module Set = struct
let both _ _ _ = Empty in
let join t1 t2 = Node (t1, t2) in
let empty = Empty in
- let f = fold2_join_heterogeneous
- ~cache ~empty_left ~empty_right ~both ~join ~empty
- in
- fun eqs1 eqs2 -> f eqs1 eqs2
+ fold2_join_heterogeneous
+ ~cache ~empty_left ~empty_right ~both ~join ~empty
end
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 3d5c2e30191..d6cf8037d45 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -388,11 +388,8 @@ module G = struct
| Some i -> MC.singleton b i
in
let join = MC.merge_disjoint in
- let f =
- MV.fold2_join_heterogeneous
- ~cache ~empty_left ~empty_right ~both ~join ~empty
- in
- fun mv1 mv2 -> f mv1 mv2
+ MV.fold2_join_heterogeneous
+ ~cache ~empty_left ~empty_right ~both ~join ~empty
(* compute pointwise [mv - mc] *)
let mv_minus_mc =
@@ -411,11 +408,8 @@ module G = struct
MV.singleton b v'
in
let join = MV.merge_disjoint in
- let f =
- MV.fold2_join_heterogeneous
- ~cache ~empty_left ~empty_right ~both ~join ~empty
- in
- fun mv mc -> f mv mc
+ MV.fold2_join_heterogeneous
+ ~cache ~empty_left ~empty_right ~both ~join ~empty
(* Implementation of the 'forget' operation. [nb] loop iterations have
elapsed, and during one iteration, variables are incremented by [coeffs].
--
GitLab