diff --git a/src/plugins/region/store.ml b/src/plugins/region/store.ml index 4e964e42b373265fedea995c5665efd92e916e39..a1bd51e505e732b37f1eb85c864e5536ba6abcae 100644 --- a/src/plugins/region/store.ml +++ b/src/plugins/region/store.ml @@ -27,18 +27,20 @@ module Imap = Map.Make(Int) type 'a rref = int -type 'a store = 'a Imap.t ref +type 'a store = { + mutable rid : int ; + mutable map : 'a Imap.t ; +} -let new_store () = ref Imap.empty -let copy r = ref !r -let rid = ref 0 +let new_store () = { rid = 0 ; map = Imap.empty } +let copy r = { rid = r.rid ; map = r.map } let make s v = - let k = incr rid ; !rid in - s := Imap.add k v !s ; k + let k = succ s.rid in + s.rid <- k ; s.map <- Imap.add k v s.map ; k -let get s k = Imap.find k !s -let set s k v = s := Imap.add k v !s +let get s k = Imap.find k s.map +let set s k v = s.map <- Imap.add k v s.map let eq _s i j = (i == j) diff --git a/src/plugins/region/tests/region/oracle/blob_region.res.oracle b/src/plugins/region/tests/region/oracle/blob_region.res.oracle index f1a5f86d8ebe6fb1e6f43f8c0a47070bc62b8951..68162db150ddceb2c91ce8b734b5d06a8fdb6ed1 100644 --- a/src/plugins/region/tests/region/oracle/blob_region.res.oracle +++ b/src/plugins/region/tests/region/oracle/blob_region.res.oracle @@ -5,9 +5,9 @@ R0004: --- 0b ; R0001: -W- p (int *) 64b (*R0004) ; [region] Function struct_blob: - R0009: --- y 64b 0..32 [0]: R000a ; - R000a: --- 0b ; - R0007: -W- p (int *) 64b (*R000a) ; + R0003: --- y 64b 0..32 [0]: R0004 ; + R0004: --- 0b ; + R0001: -W- p (int *) 64b (*R0004) ; [region] Function var_blob: - R000f: --- x 0b ; - R000d: -W- p (int *) 64b (*R000f) ; + R0003: --- x 0b ; + R0001: -W- p (int *) 64b (*R0003) ; diff --git a/src/plugins/region/tests/region/oracle/swap.res.oracle b/src/plugins/region/tests/region/oracle/swap.res.oracle index 3117fb686d5ee476901cd95a19ab05fd51194ca0..49268e6ca2960f28c6581ce3f0ccf3cfee88fd9f 100644 --- a/src/plugins/region/tests/region/oracle/swap.res.oracle +++ b/src/plugins/region/tests/region/oracle/swap.res.oracle @@ -6,8 +6,8 @@ R0001: R-- b (int *) 64b (*R0007) ; R0008: RW- tmp (int) 32b ; [region] Function swap_separated: - R0013: R-- a (int *) 64b (*R0016) ; - R0016: RW- A: (int) 32b ; - R0017: R-- b (int *) 64b (*R001a) ; - R001a: RW- B: (int) 32b ; - R001b: RW- tmp (int) 32b ; + R0001: R-- a (int *) 64b (*R0004) ; + R0004: RW- A: (int) 32b ; + R0005: R-- b (int *) 64b (*R0008) ; + R0008: RW- B: (int) 32b ; + R0009: RW- tmp (int) 32b ;