From 30e29676854b7d35beb597644d4c474b7a46f4b5 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Tue, 26 Feb 2019 13:23:48 +0100
Subject: [PATCH] [wp] explicits offset of an union field
---
src/plugins/wp/ctypes.ml | 9 ++++++---
1 file changed, 6 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index 04cd9701c91..bde88014eff 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -464,9 +464,12 @@ let sizeof_object = function
WpLog.fatal ~current:true "Sizeof unknown-size array"
let field_offset fd =
- let ctype = TComp(fd.fcomp,Cil.empty_size_cache(),[]) in
- let offset = Field(fd,NoOffset) in
- fst (Cil.bitsOffset ctype offset) / 8
+ if fd.fcomp.cstruct then (* C struct *)
+ let ctype = TComp(fd.fcomp,Cil.empty_size_cache(),[]) in
+ let offset = Field(fd,NoOffset) in
+ fst (Cil.bitsOffset ctype offset) / 8
+ else (* CIL invariant: all C union fields start at offset 0 *)
+ 0
(* Conforms to C-ISO 6.3.1.8 *)
(* If same sign => greater rank. *)
--
GitLab