From ede59c555d105390c481de4b0c952d06fa384189 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 19 Jul 2024 18:46:02 +0200
Subject: [PATCH] [kernel] add a dkey for lattice_messages
---
.../abstract_interp/lattice_messages.ml | 5 +-
tests/builtins/oracle/imprecise.res.oracle | 17 ++--
.../builtins/oracle/linked_list.1.res.oracle | 16 ++--
tests/builtins/oracle/memcpy.0.res.oracle | 26 ++++--
.../oracle_equality/imprecise.res.oracle | 8 +-
.../oracle_equality/linked_list.1.res.oracle | 16 ++--
.../oracle_gauges/memcpy.0.res.oracle | 4 +-
.../oracle_octagon/imprecise.res.oracle | 8 +-
.../oracle_octagon/linked_list.1.res.oracle | 12 +--
.../oracle_symblocs/imprecise.res.oracle | 8 +-
.../oracle_symblocs/linked_list.1.res.oracle | 12 +--
tests/value/oracle/assigns.res.oracle | 6 +-
.../oracle/multidim-relations.res.oracle | 20 ++---
tests/value/oracle/multidim.res.oracle | 45 +++++-----
tests/value/oracle/non_natural.res.oracle | 84 +++++++++----------
tests/value/oracle/offsetmap.0.res.oracle | 2 +-
tests/value/oracle/offsetmap.1.res.oracle | 2 +-
tests/value/oracle/offsetmap.2.res.oracle | 2 +-
tests/value/oracle/plevel.res.oracle | 8 +-
.../value/oracle_equality/assigns.res.oracle | 4 +-
.../imprecise_invalid_write.res.oracle | 2 +-
.../multidim-relations.res.oracle | 8 +-
.../value/oracle_equality/multidim.res.oracle | 46 ++++++----
.../oracle_equality/non_natural.res.oracle | 42 +++++-----
tests/value/oracle_equality/plevel.res.oracle | 2 +-
.../oracle_equality/pointer_comp.res.oracle | 4 +-
.../oracle_gauges/non_natural.res.oracle | 4 +-
tests/value/oracle_octagon/assigns.res.oracle | 4 +-
.../multidim-relations.res.oracle | 8 +-
.../value/oracle_octagon/multidim.res.oracle | 46 ++++++----
.../oracle_octagon/non_natural.res.oracle | 34 ++++----
tests/value/oracle_octagon/plevel.res.oracle | 2 +-
.../value/oracle_symblocs/assigns.res.oracle | 4 +-
.../multidim-relations.res.oracle | 8 +-
.../value/oracle_symblocs/multidim.res.oracle | 46 ++++++----
.../oracle_symblocs/non_natural.res.oracle | 42 +++++-----
tests/value/oracle_symblocs/plevel.res.oracle | 2 +-
37 files changed, 330 insertions(+), 279 deletions(-)
diff --git a/src/kernel_services/abstract_interp/lattice_messages.ml b/src/kernel_services/abstract_interp/lattice_messages.ml
index 969b8a61dd9..632534aef17 100644
--- a/src/kernel_services/abstract_interp/lattice_messages.ml
+++ b/src/kernel_services/abstract_interp/lattice_messages.ml
@@ -28,13 +28,16 @@ type t =
type emitter = unit
+let dkey = Kernel.register_category "approximation"
+let () = Kernel.add_debug_keys dkey
+
let emit _emitter msg =
match msg with
| Imprecision _ -> () (* Only for debug purposes *)
| Approximation str
| Costly str
| Unsoundness str ->
- Kernel.feedback ~current:true ~once:true "%s" str
+ Kernel.feedback ~dkey ~current:true ~once:true "%s" str
;;
let register _name = ()
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index e9a2b40bda7..4e35f99b2bb 100644
--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -216,27 +216,27 @@
accessing out of bounds index. assert 0 ≤ v;
[eva:alarm] imprecise.c:111: Warning:
accessing out of bounds index. assert v < 300;
-[kernel] imprecise.c:111:
+[kernel:approximation] imprecise.c:111:
more than 200(300) locations to update in array. Approximating.
[eva:alarm] imprecise.c:112: Warning: assertion got status unknown.
[eva:alarm] imprecise.c:114: Warning:
accessing out of bounds index. assert 0 ≤ v;
[eva:alarm] imprecise.c:114: Warning:
accessing out of bounds index. assert v < 300;
-[kernel] imprecise.c:114:
+[kernel:approximation] imprecise.c:114:
more than 200(300) locations to update in array. Approximating.
-[kernel] imprecise.c:114: approximating value to write.
+[kernel:approximation] imprecise.c:114: approximating value to write.
[eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
[eva] Recording results for many_writes
[from] Computing for function many_writes
-[kernel] imprecise.c:111:
+[kernel:approximation] imprecise.c:111:
more than 200(300) dependencies to update. Approximating.
-[kernel] imprecise.c:114:
+[kernel:approximation] imprecise.c:114:
more than 200(300) dependencies to update. Approximating.
[from] Done for function many_writes
-[kernel] imprecise.c:111:
+[kernel:approximation] imprecise.c:111:
more than 200(300) elements to enumerate. Approximating.
-[kernel] imprecise.c:114:
+[kernel:approximation] imprecise.c:114:
more than 200(300) elements to enumerate. Approximating.
[eva] Done for function many_writes
[eva] computing for function overlap <- main.
@@ -252,7 +252,8 @@
[eva] imprecise.c:133: Call to builtin memset
[eva] imprecise.c:133: function memset: precondition 'valid_s' got status valid.
[eva:alarm] imprecise.c:136: Warning: assertion got status unknown.
-[kernel] imprecise.c:137: too many locations to update in array. Approximating.
+[kernel:approximation] imprecise.c:137:
+ too many locations to update in array. Approximating.
[eva:alarm] imprecise.c:140: Warning:
accessing uninitialized left-value.
assert \initialized((int *)(&t_big) + 48);
diff --git a/tests/builtins/oracle/linked_list.1.res.oracle b/tests/builtins/oracle/linked_list.1.res.oracle
index b51e860fb2c..09e482693eb 100644
--- a/tests/builtins/oracle/linked_list.1.res.oracle
+++ b/tests/builtins/oracle/linked_list.1.res.oracle
@@ -538,9 +538,9 @@
==END OF DUMP==
[eva:alarm] linked_list.c:43: Warning:
out of bounds write. assert \valid(&curr->val);
-[kernel] linked_list.c:43:
+[kernel:approximation] linked_list.c:43:
more than 100(127) locations to update in array. Approximating.
-[kernel] linked_list.c:44:
+[kernel:approximation] linked_list.c:44:
more than 100(127) locations to update in array. Approximating.
[eva] linked_list.c:40:
Frama_C_dump_each:
@@ -714,9 +714,9 @@
S_0___fc_env[0..1] ∈ [--..--]
S_1___fc_env[0..1] ∈ [--..--]
==END OF DUMP==
-[kernel] linked_list.c:43:
+[kernel:approximation] linked_list.c:43:
more than 100(128) locations to update in array. Approximating.
-[kernel] linked_list.c:44:
+[kernel:approximation] linked_list.c:44:
more than 100(128) locations to update in array. Approximating.
[eva] linked_list.c:40:
Frama_C_dump_each:
@@ -811,7 +811,7 @@
has generated a garbled mix of addresses
for assigns clause __fc_stdout->__fc_FILE_data.
[eva] Done for function printf_va_1
-[kernel] linked_list.c:51:
+[kernel:approximation] linked_list.c:51:
more than 100(128) elements to enumerate. Approximating.
[eva] linked_list.c:50: starting to merge loop iterations
[eva:alarm] linked_list.c:51: Warning:
@@ -820,7 +820,7 @@
Called from linked_list.c:51.
[eva] Done for function printf_va_1
[eva] Recording results for main
-[kernel] linked_list.c:44:
+[kernel:approximation] linked_list.c:44:
more than 100(128) elements to enumerate. Approximating.
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
@@ -843,9 +843,9 @@
[from] Computing for function malloc
[from] Done for function malloc
[from] Computing for function main
-[kernel] linked_list.c:43:
+[kernel:approximation] linked_list.c:43:
more than 100(128) dependencies to update. Approximating.
-[kernel] linked_list.c:44:
+[kernel:approximation] linked_list.c:44:
more than 100(128) dependencies to update. Approximating.
[from] Computing for function printf_va_1 <-main
[from] Done for function printf_va_1
diff --git a/tests/builtins/oracle/memcpy.0.res.oracle b/tests/builtins/oracle/memcpy.0.res.oracle
index 774d89fc40d..f3394b79601 100644
--- a/tests/builtins/oracle/memcpy.0.res.oracle
+++ b/tests/builtins/oracle/memcpy.0.res.oracle
@@ -42,20 +42,24 @@
[eva] memcpy.c:51: function memcpy: precondition 'valid_dest' got status valid.
[eva] memcpy.c:51: function memcpy: precondition 'valid_src' got status valid.
[eva] memcpy.c:51: function memcpy: precondition 'separation' got status valid.
-[kernel] memcpy.c:51: too many locations to update in array. Approximating.
+[kernel:approximation] memcpy.c:51:
+ too many locations to update in array. Approximating.
[eva] memcpy.c:53: Call to builtin memcpy
[eva] memcpy.c:53: function memcpy: precondition 'valid_dest' got status valid.
[eva] memcpy.c:53: function memcpy: precondition 'valid_src' got status valid.
[eva] memcpy.c:53: function memcpy: precondition 'separation' got status valid.
-[kernel] memcpy.c:53: too many locations to update in array. Approximating.
-[kernel] memcpy.c:53:
+[kernel:approximation] memcpy.c:53:
+ too many locations to update in array. Approximating.
+[kernel:approximation] memcpy.c:53:
more than 150(1000) locations to update in array. Approximating.
-[kernel] memcpy.c:53: more than 150(1000) elements to enumerate. Approximating.
+[kernel:approximation] memcpy.c:53:
+ more than 150(1000) elements to enumerate. Approximating.
[eva] memcpy.c:57: Call to builtin memcpy
[eva] memcpy.c:57: function memcpy: precondition 'valid_dest' got status valid.
[eva] memcpy.c:57: function memcpy: precondition 'valid_src' got status valid.
[eva] memcpy.c:57: function memcpy: precondition 'separation' got status valid.
-[kernel] memcpy.c:57: too many locations to update in array. Approximating.
+[kernel:approximation] memcpy.c:57:
+ too many locations to update in array. Approximating.
[eva] Recording results for many
[from] Computing for function many
[from] Done for function many
@@ -160,28 +164,32 @@
function memcpy: precondition 'valid_dest' got status unknown.
[eva] memcpy.c:118: function memcpy: precondition 'valid_src' got status valid.
[eva] memcpy.c:118: function memcpy: precondition 'separation' got status valid.
-[kernel] memcpy.c:118: too many locations to update in array. Approximating.
+[kernel:approximation] memcpy.c:118:
+ too many locations to update in array. Approximating.
[eva] memcpy.c:122: starting to merge loop iterations
[eva] memcpy.c:126: Call to builtin memcpy
[eva:alarm] memcpy.c:126: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
[eva] memcpy.c:126: function memcpy: precondition 'valid_src' got status valid.
[eva] memcpy.c:126: function memcpy: precondition 'separation' got status valid.
-[kernel] memcpy.c:126: too many locations to update in array. Approximating.
+[kernel:approximation] memcpy.c:126:
+ too many locations to update in array. Approximating.
[eva] memcpy.c:130: starting to merge loop iterations
[eva] memcpy.c:135: Call to builtin memcpy
[eva:alarm] memcpy.c:135: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
[eva] memcpy.c:135: function memcpy: precondition 'valid_src' got status valid.
[eva] memcpy.c:135: function memcpy: precondition 'separation' got status valid.
-[kernel] memcpy.c:135: too many locations to update in array. Approximating.
+[kernel:approximation] memcpy.c:135:
+ too many locations to update in array. Approximating.
[eva] memcpy.c:139: starting to merge loop iterations
[eva] memcpy.c:144: Call to builtin memcpy
[eva:alarm] memcpy.c:144: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
[eva] memcpy.c:144: function memcpy: precondition 'valid_src' got status valid.
[eva] memcpy.c:144: function memcpy: precondition 'separation' got status valid.
-[kernel] memcpy.c:144: too many locations to update in array. Approximating.
+[kernel:approximation] memcpy.c:144:
+ too many locations to update in array. Approximating.
[eva] memcpy.c:149: Call to builtin memcpy
[eva:alarm] memcpy.c:149: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
diff --git a/tests/builtins/oracle_equality/imprecise.res.oracle b/tests/builtins/oracle_equality/imprecise.res.oracle
index 9633a07ab0e..d869951cfc1 100644
--- a/tests/builtins/oracle_equality/imprecise.res.oracle
+++ b/tests/builtins/oracle_equality/imprecise.res.oracle
@@ -1,11 +1,11 @@
220a221,222
-> [kernel] imprecise.c:111:
+> [kernel:approximation] imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
228a231,232
-> [kernel] imprecise.c:114:
+> [kernel:approximation] imprecise.c:114:
> more than 200(300) elements to enumerate. Approximating.
237,240d240
-< [kernel] imprecise.c:111:
+< [kernel:approximation] imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
-< [kernel] imprecise.c:114:
+< [kernel:approximation] imprecise.c:114:
< more than 200(300) elements to enumerate. Approximating.
diff --git a/tests/builtins/oracle_equality/linked_list.1.res.oracle b/tests/builtins/oracle_equality/linked_list.1.res.oracle
index 08a077ea283..f39a4d73328 100644
--- a/tests/builtins/oracle_equality/linked_list.1.res.oracle
+++ b/tests/builtins/oracle_equality/linked_list.1.res.oracle
@@ -1,24 +1,24 @@
488a489,490
-> [kernel] linked_list.c:19:
+> [kernel:approximation] linked_list.c:19:
> more than 100(127) elements to enumerate. Approximating.
542a545,546
-> [kernel] linked_list.c:43:
+> [kernel:approximation] linked_list.c:43:
> more than 100(127) elements to enumerate. Approximating.
544a549,550
-> [kernel] linked_list.c:44:
+> [kernel:approximation] linked_list.c:44:
> more than 100(127) elements to enumerate. Approximating.
673a680,681
-> [kernel] linked_list.c:19:
+> [kernel:approximation] linked_list.c:19:
> more than 100(128) elements to enumerate. Approximating.
718a727,728
-> [kernel] linked_list.c:43:
+> [kernel:approximation] linked_list.c:43:
> more than 100(128) elements to enumerate. Approximating.
720a731,732
-> [kernel] linked_list.c:44:
+> [kernel:approximation] linked_list.c:44:
> more than 100(128) elements to enumerate. Approximating.
814,815d825
-< [kernel] linked_list.c:51:
+< [kernel:approximation] linked_list.c:51:
< more than 100(128) elements to enumerate. Approximating.
823,824d832
-< [kernel] linked_list.c:44:
+< [kernel:approximation] linked_list.c:44:
< more than 100(128) elements to enumerate. Approximating.
diff --git a/tests/builtins/oracle_gauges/memcpy.0.res.oracle b/tests/builtins/oracle_gauges/memcpy.0.res.oracle
index 5e4fbca1c4a..de497bfb3c3 100644
--- a/tests/builtins/oracle_gauges/memcpy.0.res.oracle
+++ b/tests/builtins/oracle_gauges/memcpy.0.res.oracle
@@ -1,5 +1,5 @@
-145a146,147
+149a150,151
> [eva] memcpy.c:100: Call to builtin memcpy
> [eva] memcpy.c:100: Call to builtin memcpy
-367a370
+375a378
> [eva] memcpy.c:231: starting to merge loop iterations
diff --git a/tests/builtins/oracle_octagon/imprecise.res.oracle b/tests/builtins/oracle_octagon/imprecise.res.oracle
index 9633a07ab0e..d869951cfc1 100644
--- a/tests/builtins/oracle_octagon/imprecise.res.oracle
+++ b/tests/builtins/oracle_octagon/imprecise.res.oracle
@@ -1,11 +1,11 @@
220a221,222
-> [kernel] imprecise.c:111:
+> [kernel:approximation] imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
228a231,232
-> [kernel] imprecise.c:114:
+> [kernel:approximation] imprecise.c:114:
> more than 200(300) elements to enumerate. Approximating.
237,240d240
-< [kernel] imprecise.c:111:
+< [kernel:approximation] imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
-< [kernel] imprecise.c:114:
+< [kernel:approximation] imprecise.c:114:
< more than 200(300) elements to enumerate. Approximating.
diff --git a/tests/builtins/oracle_octagon/linked_list.1.res.oracle b/tests/builtins/oracle_octagon/linked_list.1.res.oracle
index 166d64faad7..be4a941dc0f 100644
--- a/tests/builtins/oracle_octagon/linked_list.1.res.oracle
+++ b/tests/builtins/oracle_octagon/linked_list.1.res.oracle
@@ -1,18 +1,18 @@
542a543,544
-> [kernel] linked_list.c:43:
+> [kernel:approximation] linked_list.c:43:
> more than 100(127) elements to enumerate. Approximating.
544a547,548
-> [kernel] linked_list.c:44:
+> [kernel:approximation] linked_list.c:44:
> more than 100(127) elements to enumerate. Approximating.
718a723,724
-> [kernel] linked_list.c:43:
+> [kernel:approximation] linked_list.c:43:
> more than 100(128) elements to enumerate. Approximating.
720a727,728
-> [kernel] linked_list.c:44:
+> [kernel:approximation] linked_list.c:44:
> more than 100(128) elements to enumerate. Approximating.
814,815d821
-< [kernel] linked_list.c:51:
+< [kernel:approximation] linked_list.c:51:
< more than 100(128) elements to enumerate. Approximating.
823,824d828
-< [kernel] linked_list.c:44:
+< [kernel:approximation] linked_list.c:44:
< more than 100(128) elements to enumerate. Approximating.
diff --git a/tests/builtins/oracle_symblocs/imprecise.res.oracle b/tests/builtins/oracle_symblocs/imprecise.res.oracle
index 9633a07ab0e..d869951cfc1 100644
--- a/tests/builtins/oracle_symblocs/imprecise.res.oracle
+++ b/tests/builtins/oracle_symblocs/imprecise.res.oracle
@@ -1,11 +1,11 @@
220a221,222
-> [kernel] imprecise.c:111:
+> [kernel:approximation] imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
228a231,232
-> [kernel] imprecise.c:114:
+> [kernel:approximation] imprecise.c:114:
> more than 200(300) elements to enumerate. Approximating.
237,240d240
-< [kernel] imprecise.c:111:
+< [kernel:approximation] imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
-< [kernel] imprecise.c:114:
+< [kernel:approximation] imprecise.c:114:
< more than 200(300) elements to enumerate. Approximating.
diff --git a/tests/builtins/oracle_symblocs/linked_list.1.res.oracle b/tests/builtins/oracle_symblocs/linked_list.1.res.oracle
index 166d64faad7..be4a941dc0f 100644
--- a/tests/builtins/oracle_symblocs/linked_list.1.res.oracle
+++ b/tests/builtins/oracle_symblocs/linked_list.1.res.oracle
@@ -1,18 +1,18 @@
542a543,544
-> [kernel] linked_list.c:43:
+> [kernel:approximation] linked_list.c:43:
> more than 100(127) elements to enumerate. Approximating.
544a547,548
-> [kernel] linked_list.c:44:
+> [kernel:approximation] linked_list.c:44:
> more than 100(127) elements to enumerate. Approximating.
718a723,724
-> [kernel] linked_list.c:43:
+> [kernel:approximation] linked_list.c:43:
> more than 100(128) elements to enumerate. Approximating.
720a727,728
-> [kernel] linked_list.c:44:
+> [kernel:approximation] linked_list.c:44:
> more than 100(128) elements to enumerate. Approximating.
814,815d821
-< [kernel] linked_list.c:51:
+< [kernel:approximation] linked_list.c:51:
< more than 100(128) elements to enumerate. Approximating.
823,824d828
-< [kernel] linked_list.c:44:
+< [kernel:approximation] linked_list.c:44:
< more than 100(128) elements to enumerate. Approximating.
diff --git a/tests/value/oracle/assigns.res.oracle b/tests/value/oracle/assigns.res.oracle
index 110f45908ba..9807e0d1eb0 100644
--- a/tests/value/oracle/assigns.res.oracle
+++ b/tests/value/oracle/assigns.res.oracle
@@ -150,15 +150,15 @@
[eva] computing for function f_main4_1 <- main4 <- main.
Called from assigns.i:104.
[eva] using specification for function f_main4_1
-[kernel] assigns.i:104:
+[kernel:approximation] assigns.i:104:
more than 200(1000) locations to update in array. Approximating.
-[kernel] assigns.i:104:
+[kernel:approximation] assigns.i:104:
more than 200(1000) elements to enumerate. Approximating.
[eva] Done for function f_main4_1
[eva] computing for function f_main4_2 <- main4 <- main.
Called from assigns.i:105.
[eva] using specification for function f_main4_2
-[kernel] assigns.i:105:
+[kernel:approximation] assigns.i:105:
more than 200(1000) locations to update in array. Approximating.
[eva] Done for function f_main4_2
[eva] Recording results for main4
diff --git a/tests/value/oracle/multidim-relations.res.oracle b/tests/value/oracle/multidim-relations.res.oracle
index b1030ddaf97..52556e31f52 100644
--- a/tests/value/oracle/multidim-relations.res.oracle
+++ b/tests/value/oracle/multidim-relations.res.oracle
@@ -10,18 +10,18 @@
[eva] computing for function init_array <- main.
Called from multidim-relations.c:35.
[eva] multidim-relations.c:18: starting to merge loop iterations
-[kernel] multidim-relations.c:19:
+[kernel:approximation] multidim-relations.c:19:
more than 1(350) locations to update in array. Approximating.
-[kernel] multidim-relations.c:20:
+[kernel:approximation] multidim-relations.c:20:
more than 1(350) locations to update in array. Approximating.
-[kernel] multidim-relations.c:21:
+[kernel:approximation] multidim-relations.c:21:
more than 1(175) locations to update in array. Approximating.
[eva] Recording results for init_array
-[kernel] multidim-relations.c:19:
+[kernel:approximation] multidim-relations.c:19:
more than 1(350) elements to enumerate. Approximating.
-[kernel] multidim-relations.c:20:
+[kernel:approximation] multidim-relations.c:20:
more than 1(350) elements to enumerate. Approximating.
-[kernel] multidim-relations.c:21:
+[kernel:approximation] multidim-relations.c:21:
more than 1(175) elements to enumerate. Approximating.
[eva] Done for function init_array
[eva] computing for function set_null <- main.
@@ -43,7 +43,7 @@
[eva:alarm] multidim-relations.c:31: Warning:
out of bounds read. assert \valid_read(t[index].ptr);
[eva] Recording results for use_array
-[kernel] multidim-relations.c:31:
+[kernel:approximation] multidim-relations.c:31:
more than 1(350) elements to enumerate. Approximating.
[eva] Done for function use_array
[eva] Recording results for main
@@ -156,11 +156,11 @@
[349].ptr ∈ {{ NULL ; &g }}
index ∈ [0..349]
[from] Computing for function init_array
-[kernel] multidim-relations.c:19:
+[kernel:approximation] multidim-relations.c:19:
more than 1(350) dependencies to update. Approximating.
-[kernel] multidim-relations.c:20:
+[kernel:approximation] multidim-relations.c:20:
more than 1(350) dependencies to update. Approximating.
-[kernel] multidim-relations.c:21:
+[kernel:approximation] multidim-relations.c:21:
more than 1(175) dependencies to update. Approximating.
[from] Done for function init_array
[from] Computing for function set_null
diff --git a/tests/value/oracle/multidim.res.oracle b/tests/value/oracle/multidim.res.oracle
index c4e9465407f..9454cf0b06a 100644
--- a/tests/value/oracle/multidim.res.oracle
+++ b/tests/value/oracle/multidim.res.oracle
@@ -97,13 +97,13 @@
Called from multidim.c:189.
[eva] multidim.c:65: starting to merge loop iterations
[eva] multidim.c:64: starting to merge loop iterations
-[kernel] multidim.c:66:
+[kernel:approximation] multidim.c:66:
more than 1(20) locations to update in array. Approximating.
-[kernel] multidim.c:67:
+[kernel:approximation] multidim.c:67:
more than 1(20) locations to update in array. Approximating.
-[kernel] multidim.c:66:
+[kernel:approximation] multidim.c:66:
more than 1(28) locations to update in array. Approximating.
-[kernel] multidim.c:67:
+[kernel:approximation] multidim.c:67:
more than 1(28) locations to update in array. Approximating.
[eva] computing for function Frama_C_interval <- main3 <- main.
Called from multidim.c:70.
@@ -131,8 +131,10 @@
r : # cvalue: [--..--]
# multidim: { .f = [-3.40282346639e+38 .. 3.40282346639e+38], .i = T }
[eva] Recording results for main3
-[kernel] multidim.c:66: more than 1(28) elements to enumerate. Approximating.
-[kernel] multidim.c:67: more than 1(28) elements to enumerate. Approximating.
+[kernel:approximation] multidim.c:66:
+ more than 1(28) elements to enumerate. Approximating.
+[kernel:approximation] multidim.c:67:
+ more than 1(28) elements to enumerate. Approximating.
[eva] Done for function main3
[eva] computing for function main4 <- main.
Called from multidim.c:190.
@@ -176,13 +178,13 @@
[eva] computing for function main7 <- main.
Called from multidim.c:193.
[eva] multidim.c:134: starting to merge loop iterations
-[kernel] multidim.c:136:
+[kernel:approximation] multidim.c:136:
more than 1(1000) locations to update in array. Approximating.
-[kernel] multidim.c:137:
+[kernel:approximation] multidim.c:137:
more than 1(1000) locations to update in array. Approximating.
-[kernel] multidim.c:140:
+[kernel:approximation] multidim.c:140:
more than 1(1000) locations to update in array. Approximating.
-[kernel] multidim.c:141:
+[kernel:approximation] multidim.c:141:
more than 1(1000) locations to update in array. Approximating.
[eva] multidim.c:145:
Frama_C_domain_show_each:
@@ -200,8 +202,10 @@
[eva] multidim.c:150: Frama_C_show_each_INT: {42}
[eva] multidim.c:153: Frama_C_show_each_FLOAT: {42.}
[eva] Recording results for main7
-[kernel] multidim.c:136: more than 1(1000) elements to enumerate. Approximating.
-[kernel] multidim.c:137: more than 1(1000) elements to enumerate. Approximating.
+[kernel:approximation] multidim.c:136:
+ more than 1(1000) elements to enumerate. Approximating.
+[kernel:approximation] multidim.c:137:
+ more than 1(1000) elements to enumerate. Approximating.
[eva] Done for function main7
[eva] computing for function main8 <- main.
Called from multidim.c:194.
@@ -225,7 +229,8 @@
[eva] Done for function main9
[eva] Recording results for main
[eva] Done for function main
-[kernel] multidim.c:50: more than 1(28) elements to enumerate. Approximating.
+[kernel:approximation] multidim.c:50:
+ more than 1(28) elements to enumerate. Approximating.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main1:
z[0..3] ∈ [--..--]
@@ -269,8 +274,10 @@
[from] Computing for function main2
[from] Done for function main2
[from] Computing for function main3
-[kernel] multidim.c:66: more than 1(28) dependencies to update. Approximating.
-[kernel] multidim.c:67: more than 1(28) dependencies to update. Approximating.
+[kernel:approximation] multidim.c:66:
+ more than 1(28) dependencies to update. Approximating.
+[kernel:approximation] multidim.c:67:
+ more than 1(28) dependencies to update. Approximating.
[from] Computing for function Frama_C_interval <-main3
[from] Done for function Frama_C_interval
[from] Done for function main3
@@ -281,13 +288,13 @@
[from] Computing for function main6
[from] Done for function main6
[from] Computing for function main7
-[kernel] multidim.c:136:
+[kernel:approximation] multidim.c:136:
more than 1(1000) dependencies to update. Approximating.
-[kernel] multidim.c:137:
+[kernel:approximation] multidim.c:137:
more than 1(1000) dependencies to update. Approximating.
-[kernel] multidim.c:140:
+[kernel:approximation] multidim.c:140:
more than 1(1000) dependencies to update. Approximating.
-[kernel] multidim.c:141:
+[kernel:approximation] multidim.c:141:
more than 1(1000) dependencies to update. Approximating.
[from] Done for function main7
[from] Computing for function main8
diff --git a/tests/value/oracle/non_natural.res.oracle b/tests/value/oracle/non_natural.res.oracle
index 63882b2cb85..d08c3af2ef4 100644
--- a/tests/value/oracle/non_natural.res.oracle
+++ b/tests/value/oracle/non_natural.res.oracle
@@ -53,18 +53,18 @@
[eva] non_natural.i:22: Frama_C_show_each: {{ &p2 + {0; 32} }}
[eva] non_natural.i:22: Frama_C_show_each: {{ &p2 + {0; 32; 64} }}
[eva] non_natural.i:22: Frama_C_show_each: {{ &p2 + {0; 32; 64; 96} }}
-[kernel] non_natural.i:30:
+[kernel:approximation] non_natural.i:30:
more than 200(12500) locations to update in array. Approximating.
[eva] non_natural.i:22: Frama_C_show_each: {{ &p2 + [0..400000],0%32 }}
[eva:alarm] non_natural.i:23: Warning:
out of bounds write. assert \valid(tmp);
(tmp from to++)
-[kernel] non_natural.i:23:
+[kernel:approximation] non_natural.i:23:
more than 200(12500) locations to update in array. Approximating.
[eva:alarm] non_natural.i:24: Warning:
out of bounds write. assert \valid(tmp_1);
(tmp_1 from to++)
-[kernel] non_natural.i:24:
+[kernel:approximation] non_natural.i:24:
more than 200(12500) locations to update in array. Approximating.
[eva:alarm] non_natural.i:25: Warning:
out of bounds write. assert \valid(tmp_3);
@@ -72,7 +72,7 @@
[eva:alarm] non_natural.i:25: Warning:
out of bounds read. assert \valid_read(tmp_4);
(tmp_4 from from++)
-[kernel] non_natural.i:25:
+[kernel:approximation] non_natural.i:25:
more than 200(12500) locations to update in array. Approximating.
[eva:alarm] non_natural.i:26: Warning:
out of bounds write. assert \valid(tmp_5);
@@ -80,7 +80,7 @@
[eva:alarm] non_natural.i:26: Warning:
out of bounds read. assert \valid_read(tmp_6);
(tmp_6 from from++)
-[kernel] non_natural.i:26:
+[kernel:approximation] non_natural.i:26:
more than 200(12500) locations to update in array. Approximating.
[eva:alarm] non_natural.i:27: Warning:
out of bounds write. assert \valid(tmp_7);
@@ -88,7 +88,7 @@
[eva:alarm] non_natural.i:27: Warning:
out of bounds read. assert \valid_read(tmp_8);
(tmp_8 from from++)
-[kernel] non_natural.i:27:
+[kernel:approximation] non_natural.i:27:
more than 200(12500) locations to update in array. Approximating.
[eva:alarm] non_natural.i:28: Warning:
out of bounds write. assert \valid(tmp_9);
@@ -96,7 +96,7 @@
[eva:alarm] non_natural.i:28: Warning:
out of bounds read. assert \valid_read(tmp_10);
(tmp_10 from from++)
-[kernel] non_natural.i:28:
+[kernel:approximation] non_natural.i:28:
more than 200(12500) locations to update in array. Approximating.
[eva:alarm] non_natural.i:29: Warning:
out of bounds write. assert \valid(tmp_11);
@@ -104,7 +104,7 @@
[eva:alarm] non_natural.i:29: Warning:
out of bounds read. assert \valid_read(tmp_12);
(tmp_12 from from++)
-[kernel] non_natural.i:29:
+[kernel:approximation] non_natural.i:29:
more than 200(12500) locations to update in array. Approximating.
[eva:alarm] non_natural.i:30: Warning:
out of bounds write. assert \valid(tmp_13);
@@ -121,25 +121,25 @@
(tmp_2 from from++)
[eva] non_natural.i:22: Frama_C_show_each: {{ &p2 + [0..--],0%32 }}
[eva] Recording results for duff1
-[kernel] non_natural.i:23:
+[kernel:approximation] non_natural.i:23:
more than 200(12501) elements to enumerate. Approximating.
-[kernel] non_natural.i:23:
+[kernel:approximation] non_natural.i:23:
more than 200(12500) elements to enumerate. Approximating.
-[kernel] non_natural.i:24:
+[kernel:approximation] non_natural.i:24:
more than 200(12501) elements to enumerate. Approximating.
-[kernel] non_natural.i:24:
+[kernel:approximation] non_natural.i:24:
more than 200(12500) elements to enumerate. Approximating.
-[kernel] non_natural.i:25:
+[kernel:approximation] non_natural.i:25:
more than 200(12500) elements to enumerate. Approximating.
-[kernel] non_natural.i:26:
+[kernel:approximation] non_natural.i:26:
more than 200(12500) elements to enumerate. Approximating.
-[kernel] non_natural.i:27:
+[kernel:approximation] non_natural.i:27:
more than 200(12500) elements to enumerate. Approximating.
-[kernel] non_natural.i:28:
+[kernel:approximation] non_natural.i:28:
more than 200(12500) elements to enumerate. Approximating.
-[kernel] non_natural.i:29:
+[kernel:approximation] non_natural.i:29:
more than 200(12500) elements to enumerate. Approximating.
-[kernel] non_natural.i:30:
+[kernel:approximation] non_natural.i:30:
more than 200(12500) elements to enumerate. Approximating.
[eva] Done for function duff1
[eva:alarm] non_natural.i:58: Warning:
@@ -184,18 +184,18 @@
[eva] non_natural.i:38: Frama_C_show_each: {{ &p2 + {0; 32} }}
[eva] non_natural.i:38: Frama_C_show_each: {{ &p2 + {0; 32; 64} }}
[eva] non_natural.i:38: Frama_C_show_each: {{ &p2 + {0; 32; 64; 96} }}
-[kernel] non_natural.i:46:
+[kernel:approximation] non_natural.i:46:
more than 200(12500) locations to update in array. Approximating.
[eva] non_natural.i:38: Frama_C_show_each: {{ &p2 + [0..400000],0%32 }}
[eva:alarm] non_natural.i:39: Warning:
out of bounds write. assert \valid(tmp);
(tmp from to++)
-[kernel] non_natural.i:39:
+[kernel:approximation] non_natural.i:39:
more than 200(12500) locations to update in array. Approximating.
[eva:alarm] non_natural.i:40: Warning:
out of bounds write. assert \valid(tmp_1);
(tmp_1 from to++)
-[kernel] non_natural.i:40:
+[kernel:approximation] non_natural.i:40:
more than 200(12500) locations to update in array. Approximating.
[eva:alarm] non_natural.i:41: Warning:
out of bounds write. assert \valid(tmp_3);
@@ -203,7 +203,7 @@
[eva:alarm] non_natural.i:41: Warning:
out of bounds read. assert \valid_read(tmp_4);
(tmp_4 from from++)
-[kernel] non_natural.i:41:
+[kernel:approximation] non_natural.i:41:
more than 200(12500) locations to update in array. Approximating.
[eva:alarm] non_natural.i:42: Warning:
out of bounds write. assert \valid(tmp_5);
@@ -211,7 +211,7 @@
[eva:alarm] non_natural.i:42: Warning:
out of bounds read. assert \valid_read(tmp_6);
(tmp_6 from from++)
-[kernel] non_natural.i:42:
+[kernel:approximation] non_natural.i:42:
more than 200(12500) locations to update in array. Approximating.
[eva:alarm] non_natural.i:43: Warning:
out of bounds write. assert \valid(tmp_7);
@@ -219,7 +219,7 @@
[eva:alarm] non_natural.i:43: Warning:
out of bounds read. assert \valid_read(tmp_8);
(tmp_8 from from++)
-[kernel] non_natural.i:43:
+[kernel:approximation] non_natural.i:43:
more than 200(12500) locations to update in array. Approximating.
[eva:alarm] non_natural.i:44: Warning:
out of bounds write. assert \valid(tmp_9);
@@ -227,7 +227,7 @@
[eva:alarm] non_natural.i:44: Warning:
out of bounds read. assert \valid_read(tmp_10);
(tmp_10 from from++)
-[kernel] non_natural.i:44:
+[kernel:approximation] non_natural.i:44:
more than 200(12500) locations to update in array. Approximating.
[eva:alarm] non_natural.i:45: Warning:
out of bounds write. assert \valid(tmp_11);
@@ -235,7 +235,7 @@
[eva:alarm] non_natural.i:45: Warning:
out of bounds read. assert \valid_read(tmp_12);
(tmp_12 from from++)
-[kernel] non_natural.i:45:
+[kernel:approximation] non_natural.i:45:
more than 200(12500) locations to update in array. Approximating.
[eva:alarm] non_natural.i:46: Warning:
out of bounds write. assert \valid(tmp_13);
@@ -277,39 +277,39 @@
[eva:final-states] Values at end of function main:
[from] Computing for function duff1
-[kernel] non_natural.i:23:
+[kernel:approximation] non_natural.i:23:
more than 200(12500) dependencies to update. Approximating.
-[kernel] non_natural.i:24:
+[kernel:approximation] non_natural.i:24:
more than 200(12500) dependencies to update. Approximating.
-[kernel] non_natural.i:25:
+[kernel:approximation] non_natural.i:25:
more than 200(12500) dependencies to update. Approximating.
-[kernel] non_natural.i:26:
+[kernel:approximation] non_natural.i:26:
more than 200(12500) dependencies to update. Approximating.
-[kernel] non_natural.i:27:
+[kernel:approximation] non_natural.i:27:
more than 200(12500) dependencies to update. Approximating.
-[kernel] non_natural.i:28:
+[kernel:approximation] non_natural.i:28:
more than 200(12500) dependencies to update. Approximating.
-[kernel] non_natural.i:29:
+[kernel:approximation] non_natural.i:29:
more than 200(12500) dependencies to update. Approximating.
-[kernel] non_natural.i:30:
+[kernel:approximation] non_natural.i:30:
more than 200(12500) dependencies to update. Approximating.
[from] Done for function duff1
[from] Computing for function duff2
-[kernel] non_natural.i:39:
+[kernel:approximation] non_natural.i:39:
more than 200(12500) dependencies to update. Approximating.
-[kernel] non_natural.i:40:
+[kernel:approximation] non_natural.i:40:
more than 200(12500) dependencies to update. Approximating.
-[kernel] non_natural.i:41:
+[kernel:approximation] non_natural.i:41:
more than 200(12500) dependencies to update. Approximating.
-[kernel] non_natural.i:42:
+[kernel:approximation] non_natural.i:42:
more than 200(12500) dependencies to update. Approximating.
-[kernel] non_natural.i:43:
+[kernel:approximation] non_natural.i:43:
more than 200(12500) dependencies to update. Approximating.
-[kernel] non_natural.i:44:
+[kernel:approximation] non_natural.i:44:
more than 200(12500) dependencies to update. Approximating.
-[kernel] non_natural.i:45:
+[kernel:approximation] non_natural.i:45:
more than 200(12500) dependencies to update. Approximating.
-[kernel] non_natural.i:46:
+[kernel:approximation] non_natural.i:46:
more than 200(12500) dependencies to update. Approximating.
[from] Done for function duff2
[from] Computing for function main1
diff --git a/tests/value/oracle/offsetmap.0.res.oracle b/tests/value/oracle/offsetmap.0.res.oracle
index 479f9ea51af..ff12d80b523 100644
--- a/tests/value/oracle/offsetmap.0.res.oracle
+++ b/tests/value/oracle/offsetmap.0.res.oracle
@@ -38,7 +38,7 @@
[eva:alarm] offsetmap.i:66: Warning:
accessing out of bounds index. assert i_0 < 10000000;
[eva] Recording results for g
-[kernel] offsetmap.i:68:
+[kernel:approximation] offsetmap.i:68:
more than 200(10000000) elements to enumerate. Approximating.
[eva] Done for function g
[eva] computing for function h <- main.
diff --git a/tests/value/oracle/offsetmap.1.res.oracle b/tests/value/oracle/offsetmap.1.res.oracle
index d4033b4c6a5..97213131b7b 100644
--- a/tests/value/oracle/offsetmap.1.res.oracle
+++ b/tests/value/oracle/offsetmap.1.res.oracle
@@ -38,7 +38,7 @@
[eva:alarm] offsetmap.i:66: Warning:
accessing out of bounds index. assert i_0 < 10000000;
[eva] Recording results for g
-[kernel] offsetmap.i:68:
+[kernel:approximation] offsetmap.i:68:
more than 200(10000000) elements to enumerate. Approximating.
[eva] Done for function g
[eva] computing for function h <- main.
diff --git a/tests/value/oracle/offsetmap.2.res.oracle b/tests/value/oracle/offsetmap.2.res.oracle
index 33d782cf04b..7f2b0dde2a9 100644
--- a/tests/value/oracle/offsetmap.2.res.oracle
+++ b/tests/value/oracle/offsetmap.2.res.oracle
@@ -38,7 +38,7 @@
[eva:alarm] offsetmap.i:66: Warning:
accessing out of bounds index. assert i_0 < 10000000;
[eva] Recording results for g
-[kernel] offsetmap.i:68:
+[kernel:approximation] offsetmap.i:68:
more than 200(10000000) elements to enumerate. Approximating.
[eva] Done for function g
[eva] computing for function h <- main.
diff --git a/tests/value/oracle/plevel.res.oracle b/tests/value/oracle/plevel.res.oracle
index cef8ba7c8ef..db9c5081b00 100644
--- a/tests/value/oracle/plevel.res.oracle
+++ b/tests/value/oracle/plevel.res.oracle
@@ -7,10 +7,11 @@
i ∈ [--..--]
[eva:alarm] plevel.i:11: Warning: assertion got status unknown.
[eva:alarm] plevel.i:13: Warning: assertion got status unknown.
-[kernel] plevel.i:21:
+[kernel:approximation] plevel.i:21:
more than 40(65) locations to update in array. Approximating.
[eva] Recording results for main
-[kernel] plevel.i:21: more than 40(65) elements to enumerate. Approximating.
+[kernel:approximation] plevel.i:21:
+ more than 40(65) elements to enumerate. Approximating.
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
@@ -103,7 +104,8 @@
i2 ∈ [0..64]
p ∈ {{ &t + [0x2000..0x2040] }}
[from] Computing for function main
-[kernel] plevel.i:21: more than 40(65) dependencies to update. Approximating.
+[kernel:approximation] plevel.i:21:
+ more than 40(65) dependencies to update. Approximating.
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
diff --git a/tests/value/oracle_equality/assigns.res.oracle b/tests/value/oracle_equality/assigns.res.oracle
index f423e4eb8cc..d72e7dacacb 100644
--- a/tests/value/oracle_equality/assigns.res.oracle
+++ b/tests/value/oracle_equality/assigns.res.oracle
@@ -1,6 +1,6 @@
154,155d153
< more than 200(1000) locations to update in array. Approximating.
-< [kernel] assigns.i:104:
+< [kernel:approximation] assigns.i:104:
156a155,156
-> [kernel] assigns.i:104:
+> [kernel:approximation] assigns.i:104:
> more than 200(1000) locations to update in array. Approximating.
diff --git a/tests/value/oracle_equality/imprecise_invalid_write.res.oracle b/tests/value/oracle_equality/imprecise_invalid_write.res.oracle
index 1306d9d6c57..3ed40cfb17b 100644
--- a/tests/value/oracle_equality/imprecise_invalid_write.res.oracle
+++ b/tests/value/oracle_equality/imprecise_invalid_write.res.oracle
@@ -1,3 +1,3 @@
27a28,29
-> [kernel] imprecise_invalid_write.i:9:
+> [kernel:approximation] imprecise_invalid_write.i:9:
> imprecise size for variable main1 (Undefined sizeof on a function.)
diff --git a/tests/value/oracle_equality/multidim-relations.res.oracle b/tests/value/oracle_equality/multidim-relations.res.oracle
index 174d88b2cb0..925ce57878a 100644
--- a/tests/value/oracle_equality/multidim-relations.res.oracle
+++ b/tests/value/oracle_equality/multidim-relations.res.oracle
@@ -1,15 +1,15 @@
15,19d14
-< [kernel] multidim-relations.c:20:
+< [kernel:approximation] multidim-relations.c:20:
< more than 1(350) locations to update in array. Approximating.
-< [kernel] multidim-relations.c:21:
+< [kernel:approximation] multidim-relations.c:21:
< more than 1(175) locations to update in array. Approximating.
< [eva] Recording results for init_array
22a18,19
> more than 1(350) locations to update in array. Approximating.
-> [kernel] multidim-relations.c:20:
+> [kernel:approximation] multidim-relations.c:20:
24a22,23
> more than 1(175) locations to update in array. Approximating.
-> [kernel] multidim-relations.c:21:
+> [kernel:approximation] multidim-relations.c:21:
25a25
> [eva] Recording results for init_array
45d44
diff --git a/tests/value/oracle_equality/multidim.res.oracle b/tests/value/oracle_equality/multidim.res.oracle
index 949bc2e8b3a..135ef2c480c 100644
--- a/tests/value/oracle_equality/multidim.res.oracle
+++ b/tests/value/oracle_equality/multidim.res.oracle
@@ -1,18 +1,28 @@
-101a102
-> [kernel] multidim.c:66: more than 1(20) elements to enumerate. Approximating.
-103a105
-> [kernel] multidim.c:67: more than 1(20) elements to enumerate. Approximating.
-105a108
-> [kernel] multidim.c:66: more than 1(28) elements to enumerate. Approximating.
-107a111
-> [kernel] multidim.c:67: more than 1(28) elements to enumerate. Approximating.
-134,135d137
-< [kernel] multidim.c:66: more than 1(28) elements to enumerate. Approximating.
-< [kernel] multidim.c:67: more than 1(28) elements to enumerate. Approximating.
-180a183
-> [kernel] multidim.c:136: more than 1(1000) elements to enumerate. Approximating.
-182a186
-> [kernel] multidim.c:137: more than 1(1000) elements to enumerate. Approximating.
-203,204d206
-< [kernel] multidim.c:136: more than 1(1000) elements to enumerate. Approximating.
-< [kernel] multidim.c:137: more than 1(1000) elements to enumerate. Approximating.
+101a102,103
+> [kernel:approximation] multidim.c:66:
+> more than 1(20) elements to enumerate. Approximating.
+103a106,107
+> [kernel:approximation] multidim.c:67:
+> more than 1(20) elements to enumerate. Approximating.
+105a110,111
+> [kernel:approximation] multidim.c:66:
+> more than 1(28) elements to enumerate. Approximating.
+107a114,115
+> [kernel:approximation] multidim.c:67:
+> more than 1(28) elements to enumerate. Approximating.
+134,137d141
+< [kernel:approximation] multidim.c:66:
+< more than 1(28) elements to enumerate. Approximating.
+< [kernel:approximation] multidim.c:67:
+< more than 1(28) elements to enumerate. Approximating.
+182a187,188
+> [kernel:approximation] multidim.c:136:
+> more than 1(1000) elements to enumerate. Approximating.
+184a191,192
+> [kernel:approximation] multidim.c:137:
+> more than 1(1000) elements to enumerate. Approximating.
+205,208d212
+< [kernel:approximation] multidim.c:136:
+< more than 1(1000) elements to enumerate. Approximating.
+< [kernel:approximation] multidim.c:137:
+< more than 1(1000) elements to enumerate. Approximating.
diff --git a/tests/value/oracle_equality/non_natural.res.oracle b/tests/value/oracle_equality/non_natural.res.oracle
index 10937ade1eb..b0440a8d6a5 100644
--- a/tests/value/oracle_equality/non_natural.res.oracle
+++ b/tests/value/oracle_equality/non_natural.res.oracle
@@ -1,52 +1,52 @@
57a58,59
-> [kernel] non_natural.i:30:
+> [kernel:approximation] non_natural.i:30:
> more than 200(12500) elements to enumerate. Approximating.
63a66,69
-> [kernel] non_natural.i:23:
+> [kernel:approximation] non_natural.i:23:
> more than 200(12500) elements to enumerate. Approximating.
-> [kernel] non_natural.i:23:
+> [kernel:approximation] non_natural.i:23:
> more than 200(12501) elements to enumerate. Approximating.
68a75,78
-> [kernel] non_natural.i:24:
+> [kernel:approximation] non_natural.i:24:
> more than 200(12500) elements to enumerate. Approximating.
-> [kernel] non_natural.i:24:
+> [kernel:approximation] non_natural.i:24:
> more than 200(12501) elements to enumerate. Approximating.
76a87,88
-> [kernel] non_natural.i:25:
+> [kernel:approximation] non_natural.i:25:
> more than 200(12500) elements to enumerate. Approximating.
84a97,98
-> [kernel] non_natural.i:26:
+> [kernel:approximation] non_natural.i:26:
> more than 200(12500) elements to enumerate. Approximating.
92a107,108
-> [kernel] non_natural.i:27:
+> [kernel:approximation] non_natural.i:27:
> more than 200(12500) elements to enumerate. Approximating.
100a117,118
-> [kernel] non_natural.i:28:
+> [kernel:approximation] non_natural.i:28:
> more than 200(12500) elements to enumerate. Approximating.
108a127,128
-> [kernel] non_natural.i:29:
+> [kernel:approximation] non_natural.i:29:
> more than 200(12500) elements to enumerate. Approximating.
124,143d143
-< [kernel] non_natural.i:23:
+< [kernel:approximation] non_natural.i:23:
< more than 200(12501) elements to enumerate. Approximating.
-< [kernel] non_natural.i:23:
+< [kernel:approximation] non_natural.i:23:
< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] non_natural.i:24:
+< [kernel:approximation] non_natural.i:24:
< more than 200(12501) elements to enumerate. Approximating.
-< [kernel] non_natural.i:24:
+< [kernel:approximation] non_natural.i:24:
< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] non_natural.i:25:
+< [kernel:approximation] non_natural.i:25:
< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] non_natural.i:26:
+< [kernel:approximation] non_natural.i:26:
< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] non_natural.i:27:
+< [kernel:approximation] non_natural.i:27:
< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] non_natural.i:28:
+< [kernel:approximation] non_natural.i:28:
< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] non_natural.i:29:
+< [kernel:approximation] non_natural.i:29:
< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] non_natural.i:30:
+< [kernel:approximation] non_natural.i:30:
< more than 200(12500) elements to enumerate. Approximating.
194a195,196
-> [kernel] non_natural.i:39:
+> [kernel:approximation] non_natural.i:39:
> more than 200(12500) elements to enumerate. Approximating.
diff --git a/tests/value/oracle_equality/plevel.res.oracle b/tests/value/oracle_equality/plevel.res.oracle
index 80295e5723f..d19a038f2cb 100644
--- a/tests/value/oracle_equality/plevel.res.oracle
+++ b/tests/value/oracle_equality/plevel.res.oracle
@@ -1,4 +1,4 @@
12d11
< [eva] Recording results for main
-13a13
+14a14
> [eva] Recording results for main
diff --git a/tests/value/oracle_equality/pointer_comp.res.oracle b/tests/value/oracle_equality/pointer_comp.res.oracle
index 087a06fb508..edf0ba686cb 100644
--- a/tests/value/oracle_equality/pointer_comp.res.oracle
+++ b/tests/value/oracle_equality/pointer_comp.res.oracle
@@ -1,5 +1,5 @@
30a31,34
-> [kernel] pointer_comp.c:43:
+> [kernel:approximation] pointer_comp.c:43:
> imprecise size for variable g (Undefined sizeof on a function.)
-> [kernel] pointer_comp.c:43:
+> [kernel:approximation] pointer_comp.c:43:
> imprecise size for variable f (Undefined sizeof on a function.)
diff --git a/tests/value/oracle_gauges/non_natural.res.oracle b/tests/value/oracle_gauges/non_natural.res.oracle
index d1550923f34..54c2059a1fb 100644
--- a/tests/value/oracle_gauges/non_natural.res.oracle
+++ b/tests/value/oracle_gauges/non_natural.res.oracle
@@ -61,10 +61,10 @@
< [eva] non_natural.i:22: Frama_C_show_each: {{ &p2 + [0..--],0%32 }}
125,126d74
< more than 200(12501) elements to enumerate. Approximating.
-< [kernel] non_natural.i:23:
+< [kernel:approximation] non_natural.i:23:
129,130d76
< more than 200(12501) elements to enumerate. Approximating.
-< [kernel] non_natural.i:24:
+< [kernel:approximation] non_natural.i:24:
189,192c135
< [eva] non_natural.i:38: Frama_C_show_each: {{ &p2 + [0..400000],0%32 }}
< [eva:alarm] non_natural.i:39: Warning:
diff --git a/tests/value/oracle_octagon/assigns.res.oracle b/tests/value/oracle_octagon/assigns.res.oracle
index f423e4eb8cc..d72e7dacacb 100644
--- a/tests/value/oracle_octagon/assigns.res.oracle
+++ b/tests/value/oracle_octagon/assigns.res.oracle
@@ -1,6 +1,6 @@
154,155d153
< more than 200(1000) locations to update in array. Approximating.
-< [kernel] assigns.i:104:
+< [kernel:approximation] assigns.i:104:
156a155,156
-> [kernel] assigns.i:104:
+> [kernel:approximation] assigns.i:104:
> more than 200(1000) locations to update in array. Approximating.
diff --git a/tests/value/oracle_octagon/multidim-relations.res.oracle b/tests/value/oracle_octagon/multidim-relations.res.oracle
index 174d88b2cb0..925ce57878a 100644
--- a/tests/value/oracle_octagon/multidim-relations.res.oracle
+++ b/tests/value/oracle_octagon/multidim-relations.res.oracle
@@ -1,15 +1,15 @@
15,19d14
-< [kernel] multidim-relations.c:20:
+< [kernel:approximation] multidim-relations.c:20:
< more than 1(350) locations to update in array. Approximating.
-< [kernel] multidim-relations.c:21:
+< [kernel:approximation] multidim-relations.c:21:
< more than 1(175) locations to update in array. Approximating.
< [eva] Recording results for init_array
22a18,19
> more than 1(350) locations to update in array. Approximating.
-> [kernel] multidim-relations.c:20:
+> [kernel:approximation] multidim-relations.c:20:
24a22,23
> more than 1(175) locations to update in array. Approximating.
-> [kernel] multidim-relations.c:21:
+> [kernel:approximation] multidim-relations.c:21:
25a25
> [eva] Recording results for init_array
45d44
diff --git a/tests/value/oracle_octagon/multidim.res.oracle b/tests/value/oracle_octagon/multidim.res.oracle
index 949bc2e8b3a..135ef2c480c 100644
--- a/tests/value/oracle_octagon/multidim.res.oracle
+++ b/tests/value/oracle_octagon/multidim.res.oracle
@@ -1,18 +1,28 @@
-101a102
-> [kernel] multidim.c:66: more than 1(20) elements to enumerate. Approximating.
-103a105
-> [kernel] multidim.c:67: more than 1(20) elements to enumerate. Approximating.
-105a108
-> [kernel] multidim.c:66: more than 1(28) elements to enumerate. Approximating.
-107a111
-> [kernel] multidim.c:67: more than 1(28) elements to enumerate. Approximating.
-134,135d137
-< [kernel] multidim.c:66: more than 1(28) elements to enumerate. Approximating.
-< [kernel] multidim.c:67: more than 1(28) elements to enumerate. Approximating.
-180a183
-> [kernel] multidim.c:136: more than 1(1000) elements to enumerate. Approximating.
-182a186
-> [kernel] multidim.c:137: more than 1(1000) elements to enumerate. Approximating.
-203,204d206
-< [kernel] multidim.c:136: more than 1(1000) elements to enumerate. Approximating.
-< [kernel] multidim.c:137: more than 1(1000) elements to enumerate. Approximating.
+101a102,103
+> [kernel:approximation] multidim.c:66:
+> more than 1(20) elements to enumerate. Approximating.
+103a106,107
+> [kernel:approximation] multidim.c:67:
+> more than 1(20) elements to enumerate. Approximating.
+105a110,111
+> [kernel:approximation] multidim.c:66:
+> more than 1(28) elements to enumerate. Approximating.
+107a114,115
+> [kernel:approximation] multidim.c:67:
+> more than 1(28) elements to enumerate. Approximating.
+134,137d141
+< [kernel:approximation] multidim.c:66:
+< more than 1(28) elements to enumerate. Approximating.
+< [kernel:approximation] multidim.c:67:
+< more than 1(28) elements to enumerate. Approximating.
+182a187,188
+> [kernel:approximation] multidim.c:136:
+> more than 1(1000) elements to enumerate. Approximating.
+184a191,192
+> [kernel:approximation] multidim.c:137:
+> more than 1(1000) elements to enumerate. Approximating.
+205,208d212
+< [kernel:approximation] multidim.c:136:
+< more than 1(1000) elements to enumerate. Approximating.
+< [kernel:approximation] multidim.c:137:
+< more than 1(1000) elements to enumerate. Approximating.
diff --git a/tests/value/oracle_octagon/non_natural.res.oracle b/tests/value/oracle_octagon/non_natural.res.oracle
index 69bedb2f07e..510ad3e0141 100644
--- a/tests/value/oracle_octagon/non_natural.res.oracle
+++ b/tests/value/oracle_octagon/non_natural.res.oracle
@@ -1,45 +1,45 @@
57a58,59
-> [kernel] non_natural.i:30:
+> [kernel:approximation] non_natural.i:30:
> more than 200(12500) elements to enumerate. Approximating.
63a66,67
-> [kernel] non_natural.i:23:
+> [kernel:approximation] non_natural.i:23:
> more than 200(12500) elements to enumerate. Approximating.
68a73,74
-> [kernel] non_natural.i:24:
+> [kernel:approximation] non_natural.i:24:
> more than 200(12500) elements to enumerate. Approximating.
76a83,84
-> [kernel] non_natural.i:25:
+> [kernel:approximation] non_natural.i:25:
> more than 200(12500) elements to enumerate. Approximating.
84a93,94
-> [kernel] non_natural.i:26:
+> [kernel:approximation] non_natural.i:26:
> more than 200(12500) elements to enumerate. Approximating.
92a103,104
-> [kernel] non_natural.i:27:
+> [kernel:approximation] non_natural.i:27:
> more than 200(12500) elements to enumerate. Approximating.
100a113,114
-> [kernel] non_natural.i:28:
+> [kernel:approximation] non_natural.i:28:
> more than 200(12500) elements to enumerate. Approximating.
108a123,124
-> [kernel] non_natural.i:29:
+> [kernel:approximation] non_natural.i:29:
> more than 200(12500) elements to enumerate. Approximating.
126,127d141
-< [kernel] non_natural.i:23:
+< [kernel:approximation] non_natural.i:23:
< more than 200(12500) elements to enumerate. Approximating.
130,143d143
-< [kernel] non_natural.i:24:
+< [kernel:approximation] non_natural.i:24:
< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] non_natural.i:25:
+< [kernel:approximation] non_natural.i:25:
< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] non_natural.i:26:
+< [kernel:approximation] non_natural.i:26:
< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] non_natural.i:27:
+< [kernel:approximation] non_natural.i:27:
< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] non_natural.i:28:
+< [kernel:approximation] non_natural.i:28:
< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] non_natural.i:29:
+< [kernel:approximation] non_natural.i:29:
< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] non_natural.i:30:
+< [kernel:approximation] non_natural.i:30:
< more than 200(12500) elements to enumerate. Approximating.
194a195,196
-> [kernel] non_natural.i:39:
+> [kernel:approximation] non_natural.i:39:
> more than 200(12500) elements to enumerate. Approximating.
diff --git a/tests/value/oracle_octagon/plevel.res.oracle b/tests/value/oracle_octagon/plevel.res.oracle
index 80295e5723f..d19a038f2cb 100644
--- a/tests/value/oracle_octagon/plevel.res.oracle
+++ b/tests/value/oracle_octagon/plevel.res.oracle
@@ -1,4 +1,4 @@
12d11
< [eva] Recording results for main
-13a13
+14a14
> [eva] Recording results for main
diff --git a/tests/value/oracle_symblocs/assigns.res.oracle b/tests/value/oracle_symblocs/assigns.res.oracle
index f423e4eb8cc..d72e7dacacb 100644
--- a/tests/value/oracle_symblocs/assigns.res.oracle
+++ b/tests/value/oracle_symblocs/assigns.res.oracle
@@ -1,6 +1,6 @@
154,155d153
< more than 200(1000) locations to update in array. Approximating.
-< [kernel] assigns.i:104:
+< [kernel:approximation] assigns.i:104:
156a155,156
-> [kernel] assigns.i:104:
+> [kernel:approximation] assigns.i:104:
> more than 200(1000) locations to update in array. Approximating.
diff --git a/tests/value/oracle_symblocs/multidim-relations.res.oracle b/tests/value/oracle_symblocs/multidim-relations.res.oracle
index 174d88b2cb0..925ce57878a 100644
--- a/tests/value/oracle_symblocs/multidim-relations.res.oracle
+++ b/tests/value/oracle_symblocs/multidim-relations.res.oracle
@@ -1,15 +1,15 @@
15,19d14
-< [kernel] multidim-relations.c:20:
+< [kernel:approximation] multidim-relations.c:20:
< more than 1(350) locations to update in array. Approximating.
-< [kernel] multidim-relations.c:21:
+< [kernel:approximation] multidim-relations.c:21:
< more than 1(175) locations to update in array. Approximating.
< [eva] Recording results for init_array
22a18,19
> more than 1(350) locations to update in array. Approximating.
-> [kernel] multidim-relations.c:20:
+> [kernel:approximation] multidim-relations.c:20:
24a22,23
> more than 1(175) locations to update in array. Approximating.
-> [kernel] multidim-relations.c:21:
+> [kernel:approximation] multidim-relations.c:21:
25a25
> [eva] Recording results for init_array
45d44
diff --git a/tests/value/oracle_symblocs/multidim.res.oracle b/tests/value/oracle_symblocs/multidim.res.oracle
index 949bc2e8b3a..135ef2c480c 100644
--- a/tests/value/oracle_symblocs/multidim.res.oracle
+++ b/tests/value/oracle_symblocs/multidim.res.oracle
@@ -1,18 +1,28 @@
-101a102
-> [kernel] multidim.c:66: more than 1(20) elements to enumerate. Approximating.
-103a105
-> [kernel] multidim.c:67: more than 1(20) elements to enumerate. Approximating.
-105a108
-> [kernel] multidim.c:66: more than 1(28) elements to enumerate. Approximating.
-107a111
-> [kernel] multidim.c:67: more than 1(28) elements to enumerate. Approximating.
-134,135d137
-< [kernel] multidim.c:66: more than 1(28) elements to enumerate. Approximating.
-< [kernel] multidim.c:67: more than 1(28) elements to enumerate. Approximating.
-180a183
-> [kernel] multidim.c:136: more than 1(1000) elements to enumerate. Approximating.
-182a186
-> [kernel] multidim.c:137: more than 1(1000) elements to enumerate. Approximating.
-203,204d206
-< [kernel] multidim.c:136: more than 1(1000) elements to enumerate. Approximating.
-< [kernel] multidim.c:137: more than 1(1000) elements to enumerate. Approximating.
+101a102,103
+> [kernel:approximation] multidim.c:66:
+> more than 1(20) elements to enumerate. Approximating.
+103a106,107
+> [kernel:approximation] multidim.c:67:
+> more than 1(20) elements to enumerate. Approximating.
+105a110,111
+> [kernel:approximation] multidim.c:66:
+> more than 1(28) elements to enumerate. Approximating.
+107a114,115
+> [kernel:approximation] multidim.c:67:
+> more than 1(28) elements to enumerate. Approximating.
+134,137d141
+< [kernel:approximation] multidim.c:66:
+< more than 1(28) elements to enumerate. Approximating.
+< [kernel:approximation] multidim.c:67:
+< more than 1(28) elements to enumerate. Approximating.
+182a187,188
+> [kernel:approximation] multidim.c:136:
+> more than 1(1000) elements to enumerate. Approximating.
+184a191,192
+> [kernel:approximation] multidim.c:137:
+> more than 1(1000) elements to enumerate. Approximating.
+205,208d212
+< [kernel:approximation] multidim.c:136:
+< more than 1(1000) elements to enumerate. Approximating.
+< [kernel:approximation] multidim.c:137:
+< more than 1(1000) elements to enumerate. Approximating.
diff --git a/tests/value/oracle_symblocs/non_natural.res.oracle b/tests/value/oracle_symblocs/non_natural.res.oracle
index bcfcfe9b73a..9ac7a8268f4 100644
--- a/tests/value/oracle_symblocs/non_natural.res.oracle
+++ b/tests/value/oracle_symblocs/non_natural.res.oracle
@@ -1,52 +1,52 @@
57a58,59
-> [kernel] non_natural.i:30:
+> [kernel:approximation] non_natural.i:30:
> more than 200(12500) elements to enumerate. Approximating.
63a66,69
-> [kernel] non_natural.i:23:
+> [kernel:approximation] non_natural.i:23:
> more than 200(12501) elements to enumerate. Approximating.
-> [kernel] non_natural.i:23:
+> [kernel:approximation] non_natural.i:23:
> more than 200(12500) elements to enumerate. Approximating.
68a75,78
-> [kernel] non_natural.i:24:
+> [kernel:approximation] non_natural.i:24:
> more than 200(12501) elements to enumerate. Approximating.
-> [kernel] non_natural.i:24:
+> [kernel:approximation] non_natural.i:24:
> more than 200(12500) elements to enumerate. Approximating.
76a87,88
-> [kernel] non_natural.i:25:
+> [kernel:approximation] non_natural.i:25:
> more than 200(12500) elements to enumerate. Approximating.
84a97,98
-> [kernel] non_natural.i:26:
+> [kernel:approximation] non_natural.i:26:
> more than 200(12500) elements to enumerate. Approximating.
92a107,108
-> [kernel] non_natural.i:27:
+> [kernel:approximation] non_natural.i:27:
> more than 200(12500) elements to enumerate. Approximating.
100a117,118
-> [kernel] non_natural.i:28:
+> [kernel:approximation] non_natural.i:28:
> more than 200(12500) elements to enumerate. Approximating.
108a127,128
-> [kernel] non_natural.i:29:
+> [kernel:approximation] non_natural.i:29:
> more than 200(12500) elements to enumerate. Approximating.
124,143d143
-< [kernel] non_natural.i:23:
+< [kernel:approximation] non_natural.i:23:
< more than 200(12501) elements to enumerate. Approximating.
-< [kernel] non_natural.i:23:
+< [kernel:approximation] non_natural.i:23:
< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] non_natural.i:24:
+< [kernel:approximation] non_natural.i:24:
< more than 200(12501) elements to enumerate. Approximating.
-< [kernel] non_natural.i:24:
+< [kernel:approximation] non_natural.i:24:
< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] non_natural.i:25:
+< [kernel:approximation] non_natural.i:25:
< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] non_natural.i:26:
+< [kernel:approximation] non_natural.i:26:
< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] non_natural.i:27:
+< [kernel:approximation] non_natural.i:27:
< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] non_natural.i:28:
+< [kernel:approximation] non_natural.i:28:
< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] non_natural.i:29:
+< [kernel:approximation] non_natural.i:29:
< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] non_natural.i:30:
+< [kernel:approximation] non_natural.i:30:
< more than 200(12500) elements to enumerate. Approximating.
194a195,196
-> [kernel] non_natural.i:39:
+> [kernel:approximation] non_natural.i:39:
> more than 200(12500) elements to enumerate. Approximating.
diff --git a/tests/value/oracle_symblocs/plevel.res.oracle b/tests/value/oracle_symblocs/plevel.res.oracle
index 80295e5723f..d19a038f2cb 100644
--- a/tests/value/oracle_symblocs/plevel.res.oracle
+++ b/tests/value/oracle_symblocs/plevel.res.oracle
@@ -1,4 +1,4 @@
12d11
< [eva] Recording results for main
-13a13
+14a14
> [eva] Recording results for main
--
GitLab