diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml index 1ad5b12e13bcc7950c181f43c9c38290c4f9010f..cedff2c22ac9fd5f0d7f4e58fe43178eb38fc795 100644 --- a/src/plugins/region/memory.ml +++ b/src/plugins/region/memory.ml @@ -447,9 +447,11 @@ let rec move (m: map) (r: node) (p: int) (s: int) = move m rg.data (p - rg.offset) s let field (m: map) (r: node) (fd: fieldinfo) : node = - let s = Cil.bitsSizeOf fd.ftype in - let (p,_) = Cil.fieldBitsOffset fd in - move m r p s + if fd.fcomp.cstruct then + let s = Cil.bitsSizeOf fd.ftype in + let (p,_) = Cil.fieldBitsOffset fd in + move m r p s + else r let index (m : map) (r: node) (ty:typ) : node = move m r 0 (Cil.bitsSizeOf ty)