diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 841808a4dbf6912aed982070cfe321c466faac30..f329116e49efe18ed11934c82354e29d4b629b7b 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,6 +24,7 @@
 Plugin WP <next-release>
 ###############################################################################
 
+- WP          [2023-05-03] new warning against unions (see -wp-warn-key "union")
 - WP          [2023-04-03] Default timeout set to 2s
 - WP          [2023-03-29] fix option -wp-split to only split conditions
 - WP          [2023-03-29] new option -wp-split-switch to split switches
diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index 75148e0b2ad8c622ce136f1fcd05b141b18c31d9..5db102a4dcf67d0e16f65c803bf4bfe2dc6084ee 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -462,3 +462,15 @@ let separated ~shift ~addrof ~sizeof s1 s2 =
   r_disjoint (range s1) (range s2)
 
 (* -------------------------------------------------------------------------- *)
+(* --- Unsupported Unions                                                 --- *)
+(* -------------------------------------------------------------------------- *)
+
+let wkey = Wp_parameters.register_warn_category "union"
+
+let unsupported_union (fd : Cil_types.fieldinfo) =
+  if not fd.fcomp.cstruct then
+    Wp_parameters.warning ~once:true ~wkey
+      "Accessing union fields with WP might be unsound.@\n\
+       Please refer to WP manual."
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/MemMemory.mli b/src/plugins/wp/MemMemory.mli
index a8ac29bfbbe5aa9fd5a57b8fdc28e3afbd4398d4..094cbb0bdc479fa0e6ced313eafc9449dccf740d 100644
--- a/src/plugins/wp/MemMemory.mli
+++ b/src/plugins/wp/MemMemory.mli
@@ -134,4 +134,8 @@ val included :
   sizeof:(Ctypes.c_object -> term) ->
   'a Sigs.rloc -> 'a Sigs.rloc -> pred
 
+(** {2 Unsupported Union Fields} *)
+
+val unsupported_union : Cil_types.fieldinfo -> unit
+
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 9766ce052c7ec692002da0e7dcd66121f3442c60..c9748c9f908676f3425372043beb8e2961829f91 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -425,7 +425,10 @@ module Shift = WpContext.Generator(Cobj)
         dfun.d_lfun
     end)
 
-let field l f = e_fun (ShiftField.get f) [l]
+let field l f =
+  MemMemory.unsupported_union f ;
+  e_fun (ShiftField.get f) [l]
+
 let shift l obj k = e_fun (Shift.get obj) [l;k]
 
 module LITERAL =
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 168c67c9aa0278f6d6fd7378eec05b4ae8394184..66ff09df22afecd8d27860f4abca4794e6e56037 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -546,6 +546,9 @@ struct
     | CARR of MemoryContext.validity (* In-context array *)
     | HEAP (* In-heap variable *)
 
+  let is_heap_allocated = function
+    | CREF | CVAL -> false | HEAP | CTXT _ | CARR _ -> true
+
   type loc =
     | Ref of varinfo
     | Val of mem * varinfo * ofs list (* The varinfo has {i not} been contextualized yet *)
@@ -713,10 +716,13 @@ struct
   let pointer_loc p = Loc (M.pointer_loc p)
   let pointer_val l = M.pointer_val (mloc_of_loc l)
 
-  let field l f = match l with
+  let field l f =
+    match l with
     | Loc l -> Loc (M.field l f)
     | Ref x -> noref ~op:"field access to" x
-    | Val(m,x,ofs) -> Val(m,x,ofs @ [Field f])
+    | Val(m,x,ofs) ->
+      if not @@ is_heap_allocated m then MemMemory.unsupported_union f ;
+      Val(m,x,ofs @ [Field f])
 
   let rec ofs_shift obj k = function
     | [] -> [Shift(obj,k)]
@@ -901,9 +907,6 @@ struct
 
   exception ShiftMismatch
 
-  let is_heap_allocated = function
-    | CREF | CVAL -> false | HEAP | CTXT _ | CARR _ -> true
-
   let shift_mismatch l =
     Wp_parameters.fatal "Invalid shift : %a" pretty l
 
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle
index af9965baf747212ac2e4aea4e4ce0a55724cf81c..cbdaaf5b2b7be277b720039c917f78cfc8b2e51c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle
@@ -2,6 +2,12 @@
 [kernel] Parsing init_value.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
+[wp:union] init_value.i:61: Warning: 
+  Accessing union fields with WP might be unsound.
+  Please refer to WP manual.
+[wp:union] init_value.i:40: Warning: 
+  Accessing union fields with WP might be unsound.
+  Please refer to WP manual.
 ------------------------------------------------------------
   Function fa1
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle
index fefa721cebdc73474d7908079b75804fe176d96a..50f2495c6a01090bc6531f526007a7beb512f303 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle
@@ -2,6 +2,15 @@
 [kernel] Parsing init_value.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
+[wp:union] init_value.i:73: Warning: 
+  Accessing union fields with WP might be unsound.
+  Please refer to WP manual.
+[wp:union] init_value.i:72: Warning: 
+  Accessing union fields with WP might be unsound.
+  Please refer to WP manual.
+[wp:union] init_value.i:40: Warning: 
+  Accessing union fields with WP might be unsound.
+  Please refer to WP manual.
 ------------------------------------------------------------
   Function fa1
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle
index e7b468f7aee0e722570ffd9fe0f74c3a2a093fef..63575b9739f22b3ecee9973c5fa0acf9fcbcf694 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle
@@ -2,6 +2,12 @@
 [kernel] Parsing init_value.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
+[wp:union] init_value.i:61: Warning: 
+  Accessing union fields with WP might be unsound.
+  Please refer to WP manual.
+[wp:union] init_value.i:40: Warning: 
+  Accessing union fields with WP might be unsound.
+  Please refer to WP manual.
 [wp] 24 goals scheduled
 [wp] [Valid] typed_main_requires_qed_ok_Struct_Simple_a (Qed)
 [wp] [Valid] typed_main_requires_qed_ok_Struct_Simple_b (Qed)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle
index d10bff93b408b63526b401315b429d83248c495f..11b2e62f8964957835ca65dc89bf4cadd819b43c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle
@@ -2,6 +2,15 @@
 [kernel] Parsing init_value.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
+[wp:union] init_value.i:73: Warning: 
+  Accessing union fields with WP might be unsound.
+  Please refer to WP manual.
+[wp:union] init_value.i:72: Warning: 
+  Accessing union fields with WP might be unsound.
+  Please refer to WP manual.
+[wp:union] init_value.i:40: Warning: 
+  Accessing union fields with WP might be unsound.
+  Please refer to WP manual.
 [wp] 18 goals scheduled
 [wp] [Unsuccess] typed_main_ko_requires_qed_ko_Sc_eq_ko (Alt-Ergo) (Cached)
 [wp] [Unsuccess] typed_main_ko_requires_qed_ko_Sc_t (Alt-Ergo) (Cached)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle
index 91d993407e90198cfac7642dd37c622a3ba79925..11203eb0f175287b1e86ce888cc404cc9f9c9aa5 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle
@@ -5,9 +5,18 @@
 [wp] cast_fits.i:13: Warning: 
   Cast with incompatible pointers types (source: __anonstruct_L2_2*)
      (target: sint32*)
+[wp:union] cast_fits.i:45: Warning: 
+  Accessing union fields with WP might be unsound.
+  Please refer to WP manual.
+[wp:union] cast_fits.i:52: Warning: 
+  Accessing union fields with WP might be unsound.
+  Please refer to WP manual.
 [wp] cast_fits.i:54: Warning: 
   Cast with incompatible pointers types (source: __anonunion_L8_8*)
      (target: sint32*)
+[wp:union] cast_fits.i:61: Warning: 
+  Accessing union fields with WP might be unsound.
+  Please refer to WP manual.
 [wp] cast_fits.i:60: Warning: 
   Cast with incompatible pointers types (source: sint32*)
      (target: __anonunion_L8_8*)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle
index 76f3b9532f3c8ba5cf43aac5657b1af1bfd9d1c9..1d8b88a4d13589c516d004147b4678d62f2ea2ba 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle
@@ -5,9 +5,18 @@
 [wp] cast_fits.i:13: Warning: 
   Cast with incompatible pointers types (source: __anonstruct_L2_2*)
      (target: sint32*)
+[wp:union] cast_fits.i:45: Warning: 
+  Accessing union fields with WP might be unsound.
+  Please refer to WP manual.
+[wp:union] cast_fits.i:52: Warning: 
+  Accessing union fields with WP might be unsound.
+  Please refer to WP manual.
 [wp] cast_fits.i:54: Warning: 
   Cast with incompatible pointers types (source: __anonunion_L8_8*)
      (target: sint32*)
+[wp:union] cast_fits.i:61: Warning: 
+  Accessing union fields with WP might be unsound.
+  Please refer to WP manual.
 [wp] cast_fits.i:60: Warning: 
   Cast with incompatible pointers types (source: sint32*)
      (target: __anonunion_L8_8*)
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle
index 8f652bcc9d04f6adee76d97b60152802f2958b57..87ff7ce151b9fecfb0a2e46a31f66fea5b317107 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle
@@ -5,9 +5,18 @@
 [wp] cast_fits.i:13: Warning: 
   Cast with incompatible pointers types (source: __anonstruct_L2_2*)
      (target: sint32*)
+[wp:union] cast_fits.i:45: Warning: 
+  Accessing union fields with WP might be unsound.
+  Please refer to WP manual.
+[wp:union] cast_fits.i:52: Warning: 
+  Accessing union fields with WP might be unsound.
+  Please refer to WP manual.
 [wp] cast_fits.i:54: Warning: 
   Cast with incompatible pointers types (source: __anonunion_L8_8*)
      (target: sint32*)
+[wp:union] cast_fits.i:61: Warning: 
+  Accessing union fields with WP might be unsound.
+  Please refer to WP manual.
 [wp] cast_fits.i:60: Warning: 
   Cast with incompatible pointers types (source: sint32*)
      (target: __anonunion_L8_8*)