From 85f277b397a6123ef0039d76c0e9fd9a26899d33 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 3 May 2023 09:04:20 +0200
Subject: [PATCH] [wp] factorize & tune union warning
---
src/plugins/wp/Changelog | 1 +
src/plugins/wp/MemMemory.ml | 12 ++++++++++++
src/plugins/wp/MemMemory.mli | 4 ++++
src/plugins/wp/MemTyped.ml | 5 +----
src/plugins/wp/MemVar.ml | 5 +----
.../wp/tests/wp_acsl/oracle/init_value.0.res.oracle | 4 ++--
.../wp/tests/wp_acsl/oracle/init_value.1.res.oracle | 6 +++---
.../wp_acsl/oracle_qualif/init_value.0.res.oracle | 4 ++--
.../wp_acsl/oracle_qualif/init_value.1.res.oracle | 6 +++---
.../wp/tests/wp_typed/oracle/cast_fits.0.res.oracle | 6 +++---
.../wp/tests/wp_typed/oracle/cast_fits.1.res.oracle | 6 +++---
.../wp_typed/oracle_qualif/cast_fits.res.oracle | 6 +++---
12 files changed, 38 insertions(+), 27 deletions(-)
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 841808a4dbf..f329116e49e 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 75148e0b2ad..5db102a4dcf 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 a8ac29bfbbe..094cbb0bdc4 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 463cb389e77..c9748c9f908 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -426,10 +426,7 @@ module Shift = WpContext.Generator(Cobj)
end)
let field l f =
- if not f.fcomp.cstruct then
- Wp_parameters.warning ~once:true
- "Accessing union fields with WP might be unsound.@\n\
- Please refer to WP manual." ;
+ MemMemory.unsupported_union f ;
e_fun (ShiftField.get f) [l]
let shift l obj k = e_fun (Shift.get obj) [l;k]
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 707b5b7088a..66ff09df22a 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -721,10 +721,7 @@ struct
| Loc l -> Loc (M.field l f)
| Ref x -> noref ~op:"field access to" x
| Val(m,x,ofs) ->
- if not (f.fcomp.cstruct || is_heap_allocated m) then
- Wp_parameters.warning ~once:true
- "Accessing union fields with WP might be unsound.@\n\
- Please refer to WP manual." ;
+ if not @@ is_heap_allocated m then MemMemory.unsupported_union f ;
Val(m,x,ofs @ [Field f])
let rec ofs_shift obj k = function
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 ef2a512f0d5..cbdaaf5b2b7 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,10 +2,10 @@
[kernel] Parsing init_value.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] init_value.i:61: Warning:
+[wp:union] init_value.i:61: Warning:
Accessing union fields with WP might be unsound.
Please refer to WP manual.
-[wp] init_value.i:40: Warning:
+[wp:union] init_value.i:40: Warning:
Accessing union fields with WP might be unsound.
Please refer to WP manual.
------------------------------------------------------------
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 9174739316e..50f2495c6a0 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,13 +2,13 @@
[kernel] Parsing init_value.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] init_value.i:73: Warning:
+[wp:union] init_value.i:73: Warning:
Accessing union fields with WP might be unsound.
Please refer to WP manual.
-[wp] init_value.i:72: Warning:
+[wp:union] init_value.i:72: Warning:
Accessing union fields with WP might be unsound.
Please refer to WP manual.
-[wp] init_value.i:40: Warning:
+[wp:union] init_value.i:40: Warning:
Accessing union fields with WP might be unsound.
Please refer to WP manual.
------------------------------------------------------------
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 4ecf78df8fa..63575b9739f 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,10 +2,10 @@
[kernel] Parsing init_value.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] init_value.i:61: Warning:
+[wp:union] init_value.i:61: Warning:
Accessing union fields with WP might be unsound.
Please refer to WP manual.
-[wp] init_value.i:40: Warning:
+[wp:union] init_value.i:40: Warning:
Accessing union fields with WP might be unsound.
Please refer to WP manual.
[wp] 24 goals scheduled
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 43f5b2e62e3..11b2e62f896 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,13 +2,13 @@
[kernel] Parsing init_value.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] init_value.i:73: Warning:
+[wp:union] init_value.i:73: Warning:
Accessing union fields with WP might be unsound.
Please refer to WP manual.
-[wp] init_value.i:72: Warning:
+[wp:union] init_value.i:72: Warning:
Accessing union fields with WP might be unsound.
Please refer to WP manual.
-[wp] init_value.i:40: Warning:
+[wp:union] init_value.i:40: Warning:
Accessing union fields with WP might be unsound.
Please refer to WP manual.
[wp] 18 goals scheduled
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 4f250ecc507..11203eb0f17 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,16 +5,16 @@
[wp] cast_fits.i:13: Warning:
Cast with incompatible pointers types (source: __anonstruct_L2_2*)
(target: sint32*)
-[wp] cast_fits.i:45: Warning:
+[wp:union] cast_fits.i:45: Warning:
Accessing union fields with WP might be unsound.
Please refer to WP manual.
-[wp] cast_fits.i:52: Warning:
+[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] cast_fits.i:61: Warning:
+[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:
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 c4b755ecae2..1d8b88a4d13 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,16 +5,16 @@
[wp] cast_fits.i:13: Warning:
Cast with incompatible pointers types (source: __anonstruct_L2_2*)
(target: sint32*)
-[wp] cast_fits.i:45: Warning:
+[wp:union] cast_fits.i:45: Warning:
Accessing union fields with WP might be unsound.
Please refer to WP manual.
-[wp] cast_fits.i:52: Warning:
+[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] cast_fits.i:61: Warning:
+[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:
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 68d6dc0bf6d..87ff7ce151b 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,16 +5,16 @@
[wp] cast_fits.i:13: Warning:
Cast with incompatible pointers types (source: __anonstruct_L2_2*)
(target: sint32*)
-[wp] cast_fits.i:45: Warning:
+[wp:union] cast_fits.i:45: Warning:
Accessing union fields with WP might be unsound.
Please refer to WP manual.
-[wp] cast_fits.i:52: Warning:
+[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] cast_fits.i:61: Warning:
+[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:
--
GitLab