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 7204dfeb385390bb901569f8c0105af8c35aa9f3..7c1384a1c04f5c52a72a6548da780955c26fe900 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 d0470699ed5248b3e780ba5997ce89d184d76799..4b5bc5babc0439df5f2b280692b404430064d0d0 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 eacfe860a70ae2f7fcf39af02fed264399c8a898..fd50fbc2765a12ec632190cd693e342373e59021 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 541665b1fd31aa9c5f7ed058c5e250985d19a737..e1ebdb444a629b48de1a4a035ca971c42e172067 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 0f73cd9d921aab4ce4ec6e808b028006353f1904..0442dbcc0bb22414545f59df80dc386b49b15061 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 9c0bdaeb89bb8954cd0fcfc549cff751f13df684..8476bec8b0a085f4b2d5f8ed375e25f98750da43 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 144491fa6a5834a1f5605477986cab4a7ad975b6..e66c217886a6480270b73f72f1060e85a8bea2fd 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 9b49a1f929f0d9be13a5749a0520708770076c68..21ac4586438d50d7a0d28f5272a0ee544a3d88bb 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 e74e0ef0bd84ccb3d91adb66ba28a5cd81aa5937..faae80dcde3324cace21bc468b72edc700af869e 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 1b90339b79a210f4bd4e74a18cfc5d44d1e68180..6c127b6f93be1a1ef7c1a1d49ef6725d273d9332 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 43959a75b22ca032276910afe27ebb5de76d2f91..b40a0e4e931051e9ac780d22207fb056c1a4d17c 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 d8f8c702bdc3391f49e286f128d3f81cd60af37e..96f7d06bbcffdea41084563f44381377bb7fc332 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 16be4cd6f9d1bd4e952d9eebfe1bfd3987072a4d..c7062b1e46c8c97dc58421908876fd802f45debb 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 36128624020dc7072242b008cd89cc5bbef3aac2..6d5487a3c95b3cbf34b691b75ac3291e01601906 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 e4442be010b0e63772318a085791003f4a4571eb..688bcadb820fc9db0217556c1ae22bcdf647456e 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 8c627f52259403df7d0955a4e6d085e612ac6500..da75d08fb996a4f0ef8c211e7b4ac33f15cb06ae 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