diff --git a/src/plugins/region/code.ml b/src/plugins/region/code.ml index 084809d43bd2e06bce04f8841270269b391f166a..1f0b29667abacdf9d1a7a829505506fdb570722c 100644 --- a/src/plugins/region/code.ml +++ b/src/plugins/region/code.ml @@ -28,7 +28,7 @@ open Memory (* --- L-Values & Expressions --- *) (* -------------------------------------------------------------------------- *) -type value = { from : node option ; ptr : node option } +type scalar = { from : node option ; ptr : node option } let integral = { from = None ; ptr = None } let pointer m v = match v.ptr with @@ -57,7 +57,7 @@ and add_loffset (m:map) (s:stmt) (r:node) (ty:typ)= function and add_value m s e = ignore (add_exp m s e) -and add_exp (m: map) (s:stmt) (e:exp) : value = +and add_exp (m: map) (s:stmt) (e:exp) : scalar = match e.enode with | AddrOf lv | StartOf lv -> @@ -120,6 +120,13 @@ let add_instr (m:map) (s:stmt) (instr:instr) = match instr with | Skip _ | Code_annot _ -> () + | Set(lv, { enode = Lval exp }, _) -> + let l = add_lval m s lv in + let r = add_lval m s exp in + Memory.read m l (Lval(s,exp)) ; + Memory.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 diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml index d1dd5198156ed560a08d6e5000dfeee44d623134..e10914c98ebc6e5503c32ea4d5adc40d65b3a869 100644 --- a/src/plugins/region/memory.ml +++ b/src/plugins/region/memory.ml @@ -444,6 +444,10 @@ let merge (m: map) (a: node) (b: node) : unit = failwith_locked m "Region.Memory.merge" ; merge_all m [a;b] +let merge_copy (m: map) ~(l: node) ~(r: node) : unit = + let { clayout } = get m r in + merge_all m [ l; Ufind.make m.store { empty with clayout } ] + (* -------------------------------------------------------------------------- *) (* --- Offset --- *) (* -------------------------------------------------------------------------- *) diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli index e15853e9530b642cef5d9dbb5ad2e6ace8314dcb..788ed51359df0959c63ffe2da17495f357ae9c63 100644 --- a/src/plugins/region/memory.mli +++ b/src/plugins/region/memory.mli @@ -87,6 +87,7 @@ val shift : map -> node -> Access.acs -> unit val merge : map -> node -> node -> unit val merge_all : map -> node list -> unit +val merge_copy : map -> l:node -> r:node -> unit (** @raise Not_found *) val lval : map -> lval -> node