From 654db452c39f1a993c40a2e87eba5e0929613aa4 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 4 Oct 2021 10:28:01 +0200
Subject: [PATCH] [Eva] add warning key unknown-size
---
.../e-acsl/tests/bts/oracle/bts2406.res.oracle | 2 +-
src/plugins/value/domains/cvalue/cvalue_init.ml | 1 +
src/plugins/value/engine/initialization.ml | 1 +
src/plugins/value/value_parameters.ml | 1 +
src/plugins/value/value_parameters.mli | 3 +++
tests/builtins/oracle/imprecise.res.oracle | 14 +++++++-------
tests/misc/oracle/audit-out.json | 2 +-
tests/value/oracle/abstract_struct_1.res.oracle | 2 +-
tests/value/oracle/array_zero_length.0.res.oracle | 6 +++---
tests/value/oracle/array_zero_length.1.res.oracle | 6 +++---
tests/value/oracle/empty_union.res.oracle | 2 +-
tests/value/oracle/extern.res.oracle | 4 ++--
tests/value/oracle/library.res.oracle | 2 +-
tests/value/oracle/not_ct_array_arg.res.oracle | 2 +-
tests/value/oracle/unknown_sizeof.0.res.oracle | 2 +-
tests/value/oracle/unknown_sizeof.1.res.oracle | 2 +-
16 files changed, 29 insertions(+), 23 deletions(-)
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2406.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2406.res.oracle
index 7204dfeb385..7c1384a1c04 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2406.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2406.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva] tests/bts/bts2406.c:5: Warning:
+[eva:unknown-size] tests/bts/bts2406.c:5: Warning:
during initialization of variable 'tab', size of type 'char const []'
cannot be computed (Size of array without number of elements.)
diff --git a/src/plugins/value/domains/cvalue/cvalue_init.ml b/src/plugins/value/domains/cvalue/cvalue_init.ml
index d0470699ed5..4b5bc5babc0 100644
--- a/src/plugins/value/domains/cvalue/cvalue_init.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_init.ml
@@ -46,6 +46,7 @@ let make_well hidden_base state loc =
let warn_unknown_size_aux pp v (messt, t) =
Value_parameters.warning ~once:true ~current:true
+ ~wkey:Value_parameters.wkey_unknown_size
"@[during initialization@ of %a,@ size of@ type '%a'@ cannot be@ computed@ \
(%s)@]" pp v Printer.pp_typ t messt
diff --git a/src/plugins/value/engine/initialization.ml b/src/plugins/value/engine/initialization.ml
index eacfe860a70..fd50fbc2765 100644
--- a/src/plugins/value/engine/initialization.ml
+++ b/src/plugins/value/engine/initialization.ml
@@ -63,6 +63,7 @@ let warn_unknown_size vi =
with Cil.SizeOfError (s, t)->
let pp fmt v = Format.fprintf fmt "variable '%a'" Printer.pp_varinfo v in
Value_parameters.warning ~once:true ~current:true
+ ~wkey:Value_parameters.wkey_unknown_size
"@[during initialization@ of %a,@ size of@ type '%a'@ cannot be@ \
computed@ (%s)@]" pp vi Printer.pp_typ t s;
true
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 541665b1fd3..e1ebdb444a6 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -110,6 +110,7 @@ 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
let wkey_experimental = register_warn_category "experimental"
+let wkey_unknown_size = register_warn_category "unknown-size"
module ForceValues =
WithOutput
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 0f73cd9d921..0442dbcc0bb 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -195,6 +195,9 @@ val wkey_invalid_assigns : warn_category
(** Warning category for experimental domains or features. *)
val wkey_experimental : warn_category
+(** Warning category for 'size of type T cannot be computed'. *)
+val wkey_unknown_size : 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 9c0bdaeb89b..8476bec8b0a 100644
--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -3,22 +3,22 @@
Calling undeclared function gm_f2. Old style K&R code?
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
-[eva] tests/builtins/imprecise.c:27: Warning:
+[eva:unknown-size] tests/builtins/imprecise.c:27: Warning:
during initialization of variable 'v1', size of type 'struct s' cannot be
computed (abstract type 'struct s')
-[eva] tests/builtins/imprecise.c:27: Warning:
+[eva:unknown-size] tests/builtins/imprecise.c:27: Warning:
during initialization of variable 'v2', size of type 'struct s' cannot be
computed (abstract type 'struct s')
-[eva] tests/builtins/imprecise.c:28: Warning:
+[eva:unknown-size] tests/builtins/imprecise.c:28: Warning:
during initialization of variable 'v3', size of type 'struct u' cannot be
computed (abstract type 'struct u')
-[eva] tests/builtins/imprecise.c:28: Warning:
+[eva:unknown-size] tests/builtins/imprecise.c:28: Warning:
during initialization of variable 'v5', size of type 'struct u' cannot be
computed (abstract type 'struct u')
-[eva] tests/builtins/imprecise.c:83: Warning:
+[eva:unknown-size] tests/builtins/imprecise.c:83: Warning:
during initialization of variable 's1', size of type 'struct s' cannot be
computed (abstract type 'struct s')
-[eva] tests/builtins/imprecise.c:83: Warning:
+[eva:unknown-size] tests/builtins/imprecise.c:83: Warning:
during initialization of variable 's2', size of type 'struct s' cannot be
computed (abstract type 'struct s')
[eva] Initial state computed
@@ -587,7 +587,7 @@
[eva] Computing initial state
[eva:initial-state]
creating variable S_0_t with imprecise size (type struct s [2])
-[eva] tests/builtins/imprecise.c:29: Warning:
+[eva:unknown-size] tests/builtins/imprecise.c:29: Warning:
during initialization of variable 't', size of type 'struct s' cannot be
computed (abstract type 'struct s')
[eva:initial-state]
diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json
index 144491fa6a5..e66c217886a 100644
--- a/tests/misc/oracle/audit-out.json
+++ b/tests/misc/oracle/audit-out.json
@@ -40,7 +40,7 @@
"*", "alarm", "builtins", "builtins:missing-spec",
"builtins:override", "experimental", "libc", "libc:unsupported-spec",
"locals-escaping", "loop-unroll", "malloc", "malloc:imprecise",
- "signed-overflow", "taint"
+ "signed-overflow", "taint", "unknown-size"
],
"disabled": [
"garbled-mix", "invalid-assigns", "loop-unroll:auto",
diff --git a/tests/value/oracle/abstract_struct_1.res.oracle b/tests/value/oracle/abstract_struct_1.res.oracle
index 9b49a1f929f..21ac4586438 100644
--- a/tests/value/oracle/abstract_struct_1.res.oracle
+++ b/tests/value/oracle/abstract_struct_1.res.oracle
@@ -4,7 +4,7 @@
[eva] Computing initial state
[eva:initial-state]
creating variable S_data_0_S_repositories with imprecise size (type struct abstracttype [2])
-[eva] tests/value/abstract_struct_1.c:10: Warning:
+[eva:unknown-size] tests/value/abstract_struct_1.c:10: Warning:
during initialization of variable 'repositories', size of
type 'struct abstracttype' cannot be computed
(abstract type 'struct abstracttype')
diff --git a/tests/value/oracle/array_zero_length.0.res.oracle b/tests/value/oracle/array_zero_length.0.res.oracle
index e74e0ef0bd8..faae80dcde3 100644
--- a/tests/value/oracle/array_zero_length.0.res.oracle
+++ b/tests/value/oracle/array_zero_length.0.res.oracle
@@ -7,13 +7,13 @@
zero-length arrays are a compiler extension
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
-[eva] tests/value/array_zero_length.i:8: Warning:
+[eva:unknown-size] tests/value/array_zero_length.i:8: Warning:
during initialization of variable 'T', size of type 'char []' cannot be
computed (Size of array without number of elements.)
-[eva] tests/value/array_zero_length.i:10: Warning:
+[eva:unknown-size] tests/value/array_zero_length.i:10: Warning:
during initialization of variable 'V', size of type 'char [][2]' cannot be
computed (Size of array without number of elements.)
-[eva] tests/value/array_zero_length.i:11: Warning:
+[eva:unknown-size] tests/value/array_zero_length.i:11: Warning:
during initialization of variable 'W', size of type 'char [][0]' cannot be
computed (Size of array without number of elements.)
[eva] Initial state computed
diff --git a/tests/value/oracle/array_zero_length.1.res.oracle b/tests/value/oracle/array_zero_length.1.res.oracle
index 1b90339b79a..6c127b6f93b 100644
--- a/tests/value/oracle/array_zero_length.1.res.oracle
+++ b/tests/value/oracle/array_zero_length.1.res.oracle
@@ -7,13 +7,13 @@
zero-length arrays are a compiler extension
[eva] Analyzing an incomplete application starting at main
[eva] Computing initial state
-[eva] tests/value/array_zero_length.i:8: Warning:
+[eva:unknown-size] tests/value/array_zero_length.i:8: Warning:
during initialization of variable 'T', size of type 'char []' cannot be
computed (Size of array without number of elements.)
-[eva] tests/value/array_zero_length.i:10: Warning:
+[eva:unknown-size] tests/value/array_zero_length.i:10: Warning:
during initialization of variable 'V', size of type 'char [][2]' cannot be
computed (Size of array without number of elements.)
-[eva] tests/value/array_zero_length.i:11: Warning:
+[eva:unknown-size] tests/value/array_zero_length.i:11: Warning:
during initialization of variable 'W', size of type 'char [][0]' cannot be
computed (Size of array without number of elements.)
[eva] Initial state computed
diff --git a/tests/value/oracle/empty_union.res.oracle b/tests/value/oracle/empty_union.res.oracle
index 43959a75b22..b40a0e4e931 100644
--- a/tests/value/oracle/empty_union.res.oracle
+++ b/tests/value/oracle/empty_union.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/value/empty_union.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
-[eva] tests/value/empty_union.c:59: Warning:
+[eva:unknown-size] tests/value/empty_union.c:59: Warning:
during initialization of variable 'f1', size of type 'int []' cannot be
computed (Size of array without number of elements.)
[eva] Initial state computed
diff --git a/tests/value/oracle/extern.res.oracle b/tests/value/oracle/extern.res.oracle
index d8f8c702bdc..96f7d06bbcf 100644
--- a/tests/value/oracle/extern.res.oracle
+++ b/tests/value/oracle/extern.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing tests/value/extern.i (no preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
-[eva] tests/value/extern.i:6: Warning:
+[eva:unknown-size] tests/value/extern.i:6: Warning:
during initialization of variable 'T3', size of type 'int []' cannot be
computed (Size of array without number of elements.)
-[eva] tests/value/extern.i:7: Warning:
+[eva:unknown-size] tests/value/extern.i:7: Warning:
during initialization of variable 'T4', size of type 'int const []' cannot be
computed (Size of array without number of elements.)
[eva] tests/value/extern.i:16: no size specified for array, assuming 0
diff --git a/tests/value/oracle/library.res.oracle b/tests/value/oracle/library.res.oracle
index 16be4cd6f9d..c7062b1e46c 100644
--- a/tests/value/oracle/library.res.oracle
+++ b/tests/value/oracle/library.res.oracle
@@ -3,7 +3,7 @@
[eva] Computing initial state
[eva:initial-state]
creating variable S_0_p_ss with imprecise size (type struct ss [2])
-[eva] tests/value/library.i:57: Warning:
+[eva:unknown-size] tests/value/library.i:57: Warning:
during initialization of variable 'ss', size of type 'struct ss' cannot be
computed (abstract type 'struct ss')
[eva:initial-state]
diff --git a/tests/value/oracle/not_ct_array_arg.res.oracle b/tests/value/oracle/not_ct_array_arg.res.oracle
index 36128624020..6d5487a3c95 100644
--- a/tests/value/oracle/not_ct_array_arg.res.oracle
+++ b/tests/value/oracle/not_ct_array_arg.res.oracle
@@ -6,7 +6,7 @@
v ∈ [--..--]
[eva:initial-state]
creating variable S_tb with imprecise size (type int [10][a])
-[eva] tests/value/not_ct_array_arg.i:9: Warning:
+[eva:unknown-size] tests/value/not_ct_array_arg.i:9: Warning:
during initialization of variable 'tb', size of type 'int [a]' cannot be
computed (Array with non-constant length.)
[eva:alarm] tests/value/not_ct_array_arg.i:10: Warning:
diff --git a/tests/value/oracle/unknown_sizeof.0.res.oracle b/tests/value/oracle/unknown_sizeof.0.res.oracle
index e4442be010b..688bcadb820 100644
--- a/tests/value/oracle/unknown_sizeof.0.res.oracle
+++ b/tests/value/oracle/unknown_sizeof.0.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/value/unknown_sizeof.i (no preprocessing)
[eva] Analyzing a complete application starting at main1
[eva] Computing initial state
-[eva] tests/value/unknown_sizeof.i:8: Warning:
+[eva:unknown-size] tests/value/unknown_sizeof.i:8: Warning:
during initialization of variable 's', size of type 'struct s' cannot be
computed (abstract type 'struct s')
[eva] Initial state computed
diff --git a/tests/value/oracle/unknown_sizeof.1.res.oracle b/tests/value/oracle/unknown_sizeof.1.res.oracle
index 8c627f52259..da75d08fb99 100644
--- a/tests/value/oracle/unknown_sizeof.1.res.oracle
+++ b/tests/value/oracle/unknown_sizeof.1.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/value/unknown_sizeof.i (no preprocessing)
[eva] Analyzing a complete application starting at main2
[eva] Computing initial state
-[eva] tests/value/unknown_sizeof.i:8: Warning:
+[eva:unknown-size] tests/value/unknown_sizeof.i:8: Warning:
during initialization of variable 's', size of type 'struct s' cannot be
computed (abstract type 'struct s')
[eva] Initial state computed
--
GitLab