diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml index d221fd517741f9377c8f48a1bf949cf0227cea91..2ceca06655fada23fd1b4a5925b939e328c98113 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 8fce93bf595b2df31ae2c29b5a01c7f842aad6c7..2b2f948d436a879d103e927d32a49c54cbb5919c 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 *)