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 463cb389e77e925854526a2f43b6dcd4c35fb468..c9748c9f908676f3425372043beb8e2961829f91 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 707b5b7088ac52d0157f33c291a656ed6212756c..66ff09df22afecd8d27860f4abca4794e6e56037 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 ef2a512f0d5a46bb3ce50c22c93f912bb067c78f..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,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 9174739316e9fcb830f2875ed0b8ab5bc4e6b9ad..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,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 4ecf78df8fa98154cb25737ea20cfad40d834da7..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,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 43f5b2e62e3cac54184233a28a2b1b15ce8d21ed..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,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 4f250ecc507ac127b18ae76087793a792c1a96d0..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,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 c4b755ecae26e398b61ff605c63094d8301c7aab..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,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 68d6dc0bf6da836585671e453816cccc20ec6d9f..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,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: