From be2460c363858f40a24e3e2f9aa18522187fbf87 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 9 Oct 2024 14:13:48 +0200
Subject: [PATCH] [region] fix union fields
---
src/plugins/region/memory.ml | 8 +++++---
1 file changed, 5 insertions(+), 3 deletions(-)
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index 1ad5b12e13b..cedff2c22ac 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)
--
GitLab