From c789aed567dfab981ca521944e53542966a01723 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 15 Oct 2020 16:56:59 +0200
Subject: [PATCH] [offsetmap] Simplifies iter_offset.
---
src/kernel_services/abstract_interp/offsetmap.ml | 15 +++++----------
1 file changed, 5 insertions(+), 10 deletions(-)
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 35b98e220c6..624255d6fe3 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -527,16 +527,11 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
match t with
| Empty -> ()
| Node (max, _, _, _, _, r, m, v, _) ->
- begin
- let abs_max = max +~ o in
- f (o, abs_max) (v, m, r);
- let no, nt, nz =
- try move_right o t z
- with End_reached ->
- abs_max, Empty, z (* End the recursion at next iteration *)
- in
- aux_iter no nt nz
- end
+ let abs_max = max +~ o in
+ f (o, abs_max) (v, m, r);
+ match move_right o t z with
+ | no, nt, nz -> aux_iter no nt nz
+ | exception End_reached -> ()
in
aux_iter o n z
;;
--
GitLab