diff --git a/src/plugins/region/code.ml b/src/plugins/region/code.ml index 858b1a02cda82c4aa449c73ace700e7289e2da88..fe37b8b73d2de4719785249d82a4f345bd195d72 100644 --- a/src/plugins/region/code.ml +++ b/src/plugins/region/code.ml @@ -66,14 +66,14 @@ and add_exp (m: map) (s:stmt) (e:exp) : scalar = | Lval lv -> let rv = add_lval m s lv in - Memory.read m rv (Lval(s,lv)) ; + Memory.add_read m rv (Lval(s,lv)) ; let ptr = Memory.add_value m rv @@ Cil.typeOfLval lv in { from = Some rv ; ptr } | BinOp((PlusPI|MinusPI),p,k,_) -> add_value m s k ; let v = add_exp m s p in - Option.iter (fun r -> Memory.shift m r (Exp(s,e))) v.from ; v + Option.iter (fun r -> Memory.add_shift m r (Exp(s,e))) v.from ; v | UnOp(_,e,_) -> add_value m s e ; integral @@ -102,7 +102,7 @@ let rec add_init (m:map) (s:stmt) (acs:Access.acs) (lv:lval) (iv:init) = | SingleInit e -> let r = add_lval m s lv in - Memory.write m r acs ; + Memory.add_write m r acs ; Option.iter (Memory.add_points_to m r) (add_exp m s e).ptr | CompoundInit(_,fvs) -> @@ -123,14 +123,14 @@ let add_instr (m:map) (s:stmt) (instr:instr) = | Set(lv, { enode = Lval exp }, _) -> let l = add_lval m s lv in let r = add_lval m s exp in - Memory.read m r (Lval(s,exp)) ; - Memory.write m l (Lval(s,lv)) ; + Memory.add_read m r (Lval(s,exp)) ; + Memory.add_write m l (Lval(s,lv)) ; Memory.merge_copy m ~l ~r | Set(lv,e,_) -> let r = add_lval m s lv in let v = add_exp m s e in - Memory.write m r (Lval(s,lv)) ; + Memory.add_write m r (Lval(s,lv)) ; Option.iter (Memory.add_points_to m r) v.ptr | Local_init(x,AssignInit iv,_) -> @@ -143,7 +143,7 @@ let add_instr (m:map) (s:stmt) (instr:instr) = Option.iter (fun lv -> let r = add_lval m s lv in - Memory.write m r (Lval(s,lv)) + Memory.add_write m r (Lval(s,lv)) ) lr ; Options.warning ~source:(fst @@ Stmt.loc s) "Incomplete call analysis" diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml index cedff2c22ac9fd5f0d7f4e58fe43178eb38fc795..c019b5f5251033f678d142f6f6fc7c15bd9fdc1a 100644 --- a/src/plugins/region/memory.ml +++ b/src/plugins/region/memory.ml @@ -367,20 +367,20 @@ let add_field (m:map) (r:node) (fd:fieldinfo) : node = let rf = new_chunk m () in let fields = Fields.singleton fd in let rc = new_range m ~fields ~size ~offset ~length rf in - ignore @@ merge m r rc ; rf + merge m r rc ; rf else r let add_index (m:map) (r:node) (ty:typ) (n:int) : node = let s = Cil.bitsSizeOf ty * n in let re = new_chunk m () in let rc = new_range m ~size:s ~offset:0 ~length:s re in - ignore @@ merge m r rc ; re + merge m r rc ; re let add_points_to (m: map) (a: node) (b : node) = begin failwith_locked m "Region.Memory.points_to" ; - ignore @@ merge m a @@ new_chunk m ~ptr:b () ; - ignore @@ merge m b @@ new_chunk m ~pointed:a () ; + merge m a @@ new_chunk m ~ptr:b () ; + merge m b @@ new_chunk m ~pointed:a () ; end let add_value (m:map) (rv:node) (ty:typ) : node option = @@ -388,7 +388,7 @@ let add_value (m:map) (rv:node) (ty:typ) : node option = begin failwith_locked m "Region.Memory.add_value" ; let rp = new_chunk m ~pointed:rv () in - ignore @@ merge m rv @@ new_chunk m ~ptr:rp () ; + merge m rv @@ new_chunk m ~ptr:rp () ; Some rp end else @@ -403,23 +403,23 @@ let sized (m:map) (a:node) (ty: typ) = let size = Ranges.gcd sr (Cil.bitsSizeOf ty) in if sr <> size then ignore (merge m a (new_chunk m ~size ())) -let read (m: map) (a: node) from = +let add_read (m: map) (a: node) acs = failwith_locked m "Region.Memory.read" ; let r = get m a in - Ufind.set m.store a { r with creads = Access.Set.add from r.creads } ; - sized m a (Access.typeof from) + Ufind.set m.store a { r with creads = Access.Set.add acs r.creads } ; + sized m a (Access.typeof acs) -let write (m: map) (a: node) from = +let add_write (m: map) (a: node) acs = failwith_locked m "Region.Memory.write" ; let r = get m a in - Ufind.set m.store a { r with cwrites = Access.Set.add from r.cwrites } ; - sized m a (Access.typeof from) + Ufind.set m.store a { r with cwrites = Access.Set.add acs r.cwrites } ; + sized m a (Access.typeof acs) -let shift (m: map) (a: node) from = +let add_shift (m: map) (a: node) acs = failwith_locked m "Region.Memory.shift" ; let r = get m a in - Ufind.set m.store a { r with cshifts = Access.Set.add from r.cshifts } ; - sized m a (Access.typeof from) + Ufind.set m.store a { r with cshifts = Access.Set.add acs r.cshifts } ; + sized m a (Access.typeof acs) (* -------------------------------------------------------------------------- *) (* --- Lookup ---- *) diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli index 35a2b9d2f8568513e67dc22b3f340f1f511b0372..938d5e88292685dc2c4483842e87c19341668651 100644 --- a/src/plugins/region/memory.mli +++ b/src/plugins/region/memory.mli @@ -88,9 +88,9 @@ val add_index : map -> node -> typ -> int -> node val add_points_to : map -> node -> node -> unit val add_value : map -> node -> typ -> node option -val read : map -> node -> Access.acs -> unit -val write : map -> node -> Access.acs -> unit -val shift : map -> node -> Access.acs -> unit +val add_read : map -> node -> Access.acs -> unit +val add_write : map -> node -> Access.acs -> unit +val add_shift : map -> node -> Access.acs -> unit val merge : map -> node -> node -> unit val merge_all : map -> node list -> unit