From 0c660440f0fe6508be9ceb37a57f9fdbec6d8494 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 23 Jul 2024 17:43:25 +0200
Subject: [PATCH] [region] cosmetics
---
src/plugins/region/memory.ml | 9 ++++-----
src/plugins/region/memory.mli | 2 +-
2 files changed, 5 insertions(+), 6 deletions(-)
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index d221fd51774..2ceca06655f 100644
--- a/src/plugins/region/memory.ml
+++ b/src/plugins/region/memory.ml
@@ -392,9 +392,9 @@ let merge_all (m:map) = function
do_merge m q a b ;
done
-let merge (m: map) (a: node) (b: node) : node =
+let merge (m: map) (a: node) (b: node) : unit =
failwith_locked m "Region.Memory.merge" ;
- merge_all m [a;b] ; Ufind.find m.store (min a b)
+ merge_all m [a;b]
(* -------------------------------------------------------------------------- *)
(* --- Offset --- *)
@@ -411,10 +411,9 @@ let add_field (m:map) (r:node) (fd:fieldinfo) : node =
else r
let add_index (m:map) (r:node) (ty:typ) (n:int) : node =
- let sizelt = Cil.bitsSizeOf ty in
- let length = sizelt * n in
+ let s = Cil.bitsSizeOf ty * n in
let re = new_chunk m () in
- let rc = new_range m ~size:length ~offset:0 ~length ~data:re in
+ let rc = new_range m ~size:s ~offset:0 ~length:s ~data:re in
ignore @@ merge m r rc ; re
let add_points_to (m: map) (a: node) (b : node) =
diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli
index 8fce93bf595..2b2f948d436 100644
--- a/src/plugins/region/memory.mli
+++ b/src/plugins/region/memory.mli
@@ -84,7 +84,7 @@ val read : map -> node -> Access.acs -> unit
val write : map -> node -> Access.acs -> unit
val shift : map -> node -> Access.acs -> unit
-val merge : map -> node -> node -> node
+val merge : map -> node -> node -> unit
val merge_all : map -> node list -> unit
(** @raise Not_found *)
--
GitLab