diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml index 5515e44a3b884a7281f00342677c689c8333baa1..d5438b227de994181748fcdadfd7c43f3a49b05b 100644 --- a/src/plugins/value/engine/transfer_specification.ml +++ b/src/plugins/value/engine/transfer_specification.ml @@ -138,6 +138,7 @@ let reduce_to_valid_location out loc = begin if is_assigns out && not (Locations.is_bottom_loc loc) then Value_parameters.warning ~current:true ~once:true + ~wkey:Value_parameters.wkey_invalid_assigns "@[Completely invalid destination@ for %a.@ \ Ignoring.@]" pp_assign_free_alloc out; None diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml index 5471f4b343ffdf7d312a50bdf3420e27ebf77731..5eb874d2566e44e9e243f6d50027377060d47373 100644 --- a/src/plugins/value/value_parameters.ml +++ b/src/plugins/value/value_parameters.ml @@ -98,6 +98,8 @@ let () = set_warn_status wkey_missing_loop_unroll Log.Winactive let wkey_missing_loop_unroll_for = register_warn_category "missing-loop-unroll:for" let () = set_warn_status wkey_missing_loop_unroll_for Log.Winactive let wkey_signed_overflow = register_warn_category "signed-overflow" +let wkey_invalid_assigns = register_warn_category "invalid-assigns" +let () = set_warn_status wkey_invalid_assigns Log.Wfeedback module ForceValues = WithOutput diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli index fe24f33b22e81e956807ffba17fae01f421217a2..a5f62e9cff6d10c4d4ebaef1a4dae9da8b8294f2 100644 --- a/src/plugins/value/value_parameters.mli +++ b/src/plugins/value/value_parameters.mli @@ -204,6 +204,9 @@ val wkey_missing_loop_unroll_for : warn_category (** Warning category for signed overflows *) val wkey_signed_overflow : warn_category +(** Warning category for 'completely invalid' assigns clause *) +val wkey_invalid_assigns : warn_category + (** Debug category used to print information about invalid pointer comparisons*) val dkey_pointer_comparison: category diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle index e27e83c8af3557509f71e9dee55793438f58b39d..35235461d13ed2ecd8659d12fcde6992bb47ce76 100644 --- a/tests/builtins/oracle/imprecise.res.oracle +++ b/tests/builtins/oracle/imprecise.res.oracle @@ -39,7 +39,7 @@ [eva] computing for function f <- invalid_assigns_imprecise <- main. Called from tests/builtins/imprecise.c:11. [eva] using specification for function f -[eva] tests/builtins/imprecise.c:11: Warning: +[eva:invalid-assigns] tests/builtins/imprecise.c:11: Completely invalid destination for assigns clause *p. Ignoring. [eva] Done for function f [eva] Recording results for invalid_assigns_imprecise diff --git a/tests/libc/oracle/libgen_h.res.oracle b/tests/libc/oracle/libgen_h.res.oracle index ca158666adf08acb2890a53b2ae8fecfddb3e132..a5ac900a0e19e23678ca830eeef10d3ef012d55b 100644 --- a/tests/libc/oracle/libgen_h.res.oracle +++ b/tests/libc/oracle/libgen_h.res.oracle @@ -15,7 +15,7 @@ Called from tests/libc/libgen_h.c:11. [eva] tests/libc/libgen_h.c:11: function basename: precondition 'null_or_valid_string_path' got status valid. -[eva] tests/libc/libgen_h.c:11: Warning: +[eva:invalid-assigns] tests/libc/libgen_h.c:11: Completely invalid destination for assigns clause *(path + (0 ..)). Ignoring. [eva] Done for function basename [eva:alarm] tests/libc/libgen_h.c:12: Warning: assertion got status unknown. @@ -30,7 +30,7 @@ Called from tests/libc/libgen_h.c:16. [eva] tests/libc/libgen_h.c:16: function dirname: precondition 'null_or_valid_string_path' got status valid. -[eva] tests/libc/libgen_h.c:16: Warning: +[eva:invalid-assigns] tests/libc/libgen_h.c:16: Completely invalid destination for assigns clause *(path + (0 ..)). Ignoring. [eva] Done for function dirname [eva:alarm] tests/libc/libgen_h.c:17: Warning: assertion got status unknown. diff --git a/tests/libc/oracle/string_h.res.oracle b/tests/libc/oracle/string_h.res.oracle index 75780c1ba4a10561b67f6deb39440fddbcfbf8cb..55c5afe6dad117fc0beb325fa0f45052db727460 100644 --- a/tests/libc/oracle/string_h.res.oracle +++ b/tests/libc/oracle/string_h.res.oracle @@ -134,7 +134,7 @@ function strtok: precondition 'valid_string_delim' got status valid. [eva] tests/libc/string_h.c:72: function strtok, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status valid. -[eva] tests/libc/string_h.c:72: Warning: +[eva:invalid-assigns] tests/libc/string_h.c:72: Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring. [eva] Done for function strtok [eva:alarm] tests/libc/string_h.c:73: Warning: assertion got status unknown. @@ -144,7 +144,7 @@ function strtok: precondition 'valid_string_delim' got status valid. [eva:alarm] tests/libc/string_h.c:75: Warning: function strtok, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status unknown. -[eva] tests/libc/string_h.c:75: Warning: +[eva:invalid-assigns] tests/libc/string_h.c:75: Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring. [eva] Done for function strtok [eva:alarm] tests/libc/string_h.c:76: Warning: @@ -221,7 +221,7 @@ function strtok_r: precondition 'valid_saveptr' got status valid. [eva] tests/libc/string_h.c:102: function strtok_r, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status valid. -[eva] tests/libc/string_h.c:102: Warning: +[eva:invalid-assigns] tests/libc/string_h.c:102: Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring. [eva] Done for function strtok_r [eva:alarm] tests/libc/string_h.c:103: Warning: assertion got status unknown. @@ -233,7 +233,7 @@ function strtok_r: precondition 'valid_saveptr' got status valid. [eva:alarm] tests/libc/string_h.c:105: Warning: function strtok_r, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status unknown. -[eva] tests/libc/string_h.c:105: Warning: +[eva:invalid-assigns] tests/libc/string_h.c:105: Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring. [eva] Done for function strtok_r [eva:alarm] tests/libc/string_h.c:106: Warning: diff --git a/tests/value/oracle/leaf_spec.0.res.oracle b/tests/value/oracle/leaf_spec.0.res.oracle index 761d38bcf9e226c2597073376f838576ca755dd9..4dda7f7cf8b0609d64b17c78ec40d983449de12b 100644 --- a/tests/value/oracle/leaf_spec.0.res.oracle +++ b/tests/value/oracle/leaf_spec.0.res.oracle @@ -27,7 +27,7 @@ [kernel:annot:missing-spec] tests/value/leaf_spec.i:22: Warning: Neither code nor specification for function k, generating default assigns from the prototype [eva] using specification for function k -[eva] tests/value/leaf_spec.i:22: Warning: +[eva:invalid-assigns] tests/value/leaf_spec.i:22: Completely invalid destination for assigns clause *l. Ignoring. [eva] Done for function k [eva] computing for function k0 <- main. diff --git a/tests/value/oracle/leaf_spec.1.res.oracle b/tests/value/oracle/leaf_spec.1.res.oracle index 666a0ee653ea406fd618ea0f479ba41d7741adf0..aa1978e94dfdb9044fb6881d77a2a219b2701da0 100644 --- a/tests/value/oracle/leaf_spec.1.res.oracle +++ b/tests/value/oracle/leaf_spec.1.res.oracle @@ -9,9 +9,9 @@ [kernel:annot:missing-spec] tests/value/leaf_spec.i:27: Warning: Neither code nor specification for function f, generating default assigns from the prototype [eva] using specification for function f -[eva] tests/value/leaf_spec.i:27: Warning: +[eva:invalid-assigns] tests/value/leaf_spec.i:27: Completely invalid destination for assigns clause *x. Ignoring. -[eva] tests/value/leaf_spec.i:27: Warning: +[eva:invalid-assigns] tests/value/leaf_spec.i:27: Completely invalid destination for assigns clause *y. Ignoring. [eva] Done for function f [eva] Recording results for main1