From e9b12b5f7c9a75e3bdf0011efd3cb989badbe327 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Thu, 6 Jun 2019 11:31:04 +0200
Subject: [PATCH] [Eva] change 'invalid assigns' clause warning to feedback
---
src/plugins/value/engine/transfer_specification.ml | 1 +
src/plugins/value/value_parameters.ml | 2 ++
src/plugins/value/value_parameters.mli | 3 +++
tests/builtins/oracle/imprecise.res.oracle | 2 +-
tests/libc/oracle/libgen_h.res.oracle | 4 ++--
tests/libc/oracle/string_h.res.oracle | 8 ++++----
tests/value/oracle/leaf_spec.0.res.oracle | 2 +-
tests/value/oracle/leaf_spec.1.res.oracle | 4 ++--
8 files changed, 16 insertions(+), 10 deletions(-)
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index 5515e44a3b8..d5438b227de 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 5471f4b343f..5eb874d2566 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 fe24f33b22e..a5f62e9cff6 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 e27e83c8af3..35235461d13 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 ca158666adf..a5ac900a0e1 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 75780c1ba4a..55c5afe6dad 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 761d38bcf9e..4dda7f7cf8b 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 666a0ee653e..aa1978e94df 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
--
GitLab