diff --git a/src/kernel_services/abstract_interp/abstract_interp.ml b/src/kernel_services/abstract_interp/abstract_interp.ml
index 8556519564248f3cd6f260e6479949b4c6e52ee7..109cf2d8e185ba8b3bcce0224d3537e61edc3845 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.ml
+++ b/src/kernel_services/abstract_interp/abstract_interp.ml
@@ -25,7 +25,11 @@ exception Error_Bottom
exception Not_less_than
exception Can_not_subdiv
-let msg_emitter = Lattice_messages.register "Abstract_interp"
+let dkey = Kernel.register_category "approximation"
+let () = Kernel.add_debug_keys dkey
+
+let feedback_approximation format =
+ Kernel.feedback ~dkey ~current:true ~once:true format
type truth = True | False | Unknown
@@ -269,8 +273,7 @@ module Int = struct
let nb_loop = e_div (sub sup inf) step in
let rec fold_incr ~counter ~inf acc =
if equal counter onethousand then
- Lattice_messages.emit_costly msg_emitter
- "enumerating %a integers" pretty nb_loop;
+ feedback_approximation "enumerating %a integers" pretty nb_loop;
if le inf sup then begin
(* Format.printf "Int.fold: %a@\n" pretty inf; *)
fold_incr ~counter:(succ counter) ~inf:(add step inf) (f inf acc)
@@ -278,8 +281,7 @@ module Int = struct
in
let rec fold_decr ~counter ~sup acc =
if equal counter onethousand then
- Lattice_messages.emit_costly msg_emitter
- "enumerating %a integers" pretty nb_loop;
+ feedback_approximation "enumerating %a integers" pretty nb_loop;
if le inf sup then begin
(* Format.printf "Int.fold: %a@\n" pretty inf; *)
fold_decr ~counter:(succ counter) ~sup:(add step sup) (f sup acc)
diff --git a/src/kernel_services/abstract_interp/abstract_interp.mli b/src/kernel_services/abstract_interp/abstract_interp.mli
index 5fcbdcdd7b74c9f0cca30fad29d1a1da287bad9e..9316a481170a92b2a51a59913935feaaecee239b 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.mli
+++ b/src/kernel_services/abstract_interp/abstract_interp.mli
@@ -23,6 +23,8 @@
(** Functors for generic lattices implementations.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
+val feedback_approximation: ('a, Format.formatter, unit) format -> 'a
+
exception Error_Top
(** Raised by some functions when encountering a top value. *)
diff --git a/src/kernel_services/abstract_interp/int_interval.ml b/src/kernel_services/abstract_interp/int_interval.ml
index 4ec276b83bb77282cd29d98d1e38549bec679c03..21565bdbb10fba7beb7f422c2b482092239ad37d 100644
--- a/src/kernel_services/abstract_interp/int_interval.ml
+++ b/src/kernel_services/abstract_interp/int_interval.ml
@@ -22,9 +22,6 @@
open Abstract_interp
-let emitter = Lattice_messages.register "Int_interval";;
-let log_imprecision s = Lattice_messages.emit_imprecision emitter s
-
(* Represents the interval between [min] and [max], congruent to [rem] modulo
[modulo]. A value of [None] for [min] (resp. [max]) represents -infinity
(resp. +infinity). [modulo] is > 0, and [0 <= rem < modulo]. *)
@@ -683,12 +680,11 @@ let div_range x ymn ymx =
let max = Int.max (Int.max c1 c2) (Int.max c3 c4) in
inject_range (Some min) (Some max)
| _ ->
- log_imprecision "Ival.div_range";
top
let div x y =
match y.min, y.max with
- | None, _ | _, None -> log_imprecision "Ival.div"; `Value top
+ | None, _ | _, None -> `Value top
| Some min, Some max ->
let result_pos =
if Int.gt max Int.zero
diff --git a/src/kernel_services/abstract_interp/int_set.ml b/src/kernel_services/abstract_interp/int_set.ml
index 43f46c43e38f18cc00b5df92c864ccf42085a00f..852f06a86f2cd4527550febc6a9c654aa66689ae 100644
--- a/src/kernel_services/abstract_interp/int_set.ml
+++ b/src/kernel_services/abstract_interp/int_set.ml
@@ -30,9 +30,6 @@ let set_small_cardinal i = small_cardinal := i
let debug_cardinal = false
-let emitter = Lattice_messages.register "Int_set";;
-let log_imprecision s = Lattice_messages.emit_imprecision emitter s
-
(* Small sets of integers, implemented as sorted non-empty arrays. *)
type set = Int.t array
@@ -335,7 +332,6 @@ let set_to_ival_under set =
(* Else: arbitrarily drop some elements of the under approximation. *)
else
let a = Array.make !small_cardinal Int.zero in
- log_imprecision "Ival.set_to_ival_under";
try
ignore (Int.Set.fold (fun elt i ->
if i = !small_cardinal then raise Exit;
diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml
index ed4c2b7551ea874e91173209e5be2972144b197f..dfa194dc7a3121bc8c120beb00ea2c48a11cc813 100644
--- a/src/kernel_services/abstract_interp/int_val.ml
+++ b/src/kernel_services/abstract_interp/int_val.ml
@@ -27,9 +27,6 @@ open Bottom.Operators
let small_cardinal = Int_set.get_small_cardinal
let small_cardinal_Int () = Int.of_int (small_cardinal ())
-let emitter = Lattice_messages.register "Int_val"
-let log_imprecision s = Lattice_messages.emit_imprecision emitter s
-
type widen_hint = Datatype.Integer.Set.t
(* --------------------------------- Datatype ------------------------------- *)
@@ -315,7 +312,6 @@ let diff_if_one value rem =
| _ -> `Value value
let diff value rem =
- log_imprecision "Ival.diff";
diff_if_one value rem
(* ------------------------------- Lattice ---------------------------------- *)
@@ -426,8 +422,6 @@ let add_under v1 v2 =
| Set s1, Set s2 -> `Value (inject_set_or_top (Int_set.add_under s1 s2))
| Itv i1, Itv i2 -> Int_interval.add_under i1 i2 >>-: inject_itv
| Set s, Itv i | Itv i, Set s ->
- if Int_set.cardinal s <> 1
- then log_imprecision "Ival.add_int_under";
(* This is precise if [s] has only one element. Otherwise, this is not worse
than another computation. *)
`Value (Itv (Int_interval.add_singleton_int (Int_set.min s) i))
@@ -527,7 +521,6 @@ let shift_aux scale op (x: t) (y: t) =
let factor = check_make ~min ~max ~rem:Int.zero ~modu in
op x factor
with Z.Overflow ->
- Lattice_messages.emit_imprecision emitter "Ival.shift_aux";
(* We only preserve the sign of the result *)
if is_included x positive_integers then positive_integers
else
@@ -659,9 +652,7 @@ let extract_bits ~start ~stop = function
let dived = scale_div ~pos:true (Int.two_power start) d in
let factor = Int.two_power (Int.length start stop) in
scale_rem ~pos:true factor dived
- with Z.Overflow ->
- Lattice_messages.emit_imprecision emitter "Ival.extract_bits";
- top
+ with Z.Overflow -> top
let make = check_make
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index dd3c6a9e3ed1db9fe8fbebe7cd2aa18d56ec5264..7d64c801fb99d13edc99597d07ac6b5c3860a20b 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -24,9 +24,6 @@ open Abstract_interp
open Lattice_bounds
open Bottom.Operators
-let emitter = Lattice_messages.register "Ival"
-let log_imprecision s = Lattice_messages.emit_imprecision emitter s
-
module type Type = sig
(* Binary abstract operations do not model precisely float/integer operations.
It is the responsibility of the callers to have two operands of the same
@@ -667,7 +664,6 @@ let diff_if_one value rem =
| _, _ -> value
let diff value rem =
- log_imprecision "Ival.diff";
diff_if_one value rem
(* This function is an iterator, but it needs [diff_if_one] just above. *)
diff --git a/src/kernel_services/abstract_interp/lattice_messages.ml b/src/kernel_services/abstract_interp/lattice_messages.ml
deleted file mode 100644
index 969b8a61dd96da2583d19b4cf4225906701c3854..0000000000000000000000000000000000000000
--- a/src/kernel_services/abstract_interp/lattice_messages.ml
+++ /dev/null
@@ -1,61 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-type t =
- | Approximation of string
- | Imprecision of string
- | Costly of string
- | Unsoundness of string
-
-type emitter = unit
-
-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
-;;
-
-let register _name = ()
-
-let emit_approximation emitter = Format.kfprintf (fun _fmt ->
- let str = Format.flush_str_formatter() in
- emit emitter (Approximation str)) Format.str_formatter
-;;
-
-let emit_costly emitter = Format.kfprintf (fun _fmt ->
- let str = Format.flush_str_formatter() in
- emit emitter (Costly str)) Format.str_formatter
-;;
-
-let emit_imprecision emitter str =
- emit emitter (Imprecision str)
-;;
-
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/abstract_interp/lattice_messages.mli b/src/kernel_services/abstract_interp/lattice_messages.mli
deleted file mode 100644
index 9cb5cce0628a879bbf70b80c6034f5af5012b34d..0000000000000000000000000000000000000000
--- a/src/kernel_services/abstract_interp/lattice_messages.mli
+++ /dev/null
@@ -1,50 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(** Message and logging facility for abstract lattices. *)
-
-type t =
- | Approximation of string
- (** Abstract transfer function that intentionally approximates its result *)
- | Imprecision of string
- (** Abstract transfer function not fully implemented *)
- | Costly of string
- (** Abstract operation will be costly *)
- | Unsoundness of string
- (** Unsound abstract operation *)
-
-type emitter
-
-(** Register a new emitter for a message. *)
-val register: string -> emitter;;
-
-(** Emit a message. *)
-val emit: emitter -> t -> unit
-val emit_imprecision: emitter -> string -> unit
-val emit_approximation: emitter -> ('a, Format.formatter, unit) format -> 'a
-val emit_costly: emitter -> ('a, Format.formatter, unit) format -> 'a
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index 148cd8beb4c6ae1f739c2796f8fdafc8da61c180..7c4689e11b9c9a5a39f9b53e1abf41783c5a661c 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -24,8 +24,6 @@ open Abstract_interp
open Locations
open Lattice_bounds
-let msg_emitter = Lattice_messages.register "Lmap";;
-
type 'a default_contents =
| Bottom
| Top of 'a
@@ -201,7 +199,7 @@ struct
in
match loc with
| Location_Bits.Top (Base.SetLattice.Top, orig) ->
- Lattice_messages.emit_approximation msg_emitter
+ Abstract_interp.feedback_approximation
"writing at a completely unknown address @[%a@]"
Origin.pretty_as_reason orig;
raise Result_is_top
@@ -526,7 +524,7 @@ struct
!had_non_bottom, result
| Location_Bits.Top (top, orig) ->
if not (Base.SetLattice.equal top Base.SetLattice.top) then
- Lattice_messages.emit_approximation msg_emitter
+ Abstract_interp.feedback_approximation
"writing somewhere in @[%a@]@[%a@]."
Base.SetLattice.pretty top
Origin.pretty_as_reason orig;
diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index c65885af13a597fbc99e5cdd8fd536a6ae12e5c4..56d9349940e31cfd98502a2f2952a0be9b2ab22a 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -24,8 +24,6 @@ open Cil_types
open Cil
open Abstract_interp
-let emitter = Lattice_messages.register "Locations"
-
module Initial_Values = struct
let v = [ [Base.null,Ival.zero];
[Base.null,Ival.one];
@@ -548,7 +546,7 @@ let int_base_size_of_varinfo v =
let s = Int.of_int s in
Int_Base.inject s
with Cil.SizeOfError (msg, _) ->
- Lattice_messages.emit_approximation emitter
+ Abstract_interp.feedback_approximation
"imprecise size for variable %a (%s)" Printer.pp_varinfo v msg;
Int_Base.top
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index a22454c830a9499e98f9ec8f2bad41e40e549c46..43fe9f3436bfe5ec33cd1110eebdf858558f11ac 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -38,8 +38,6 @@ let ( %~ ) = Integer.e_rem
let succ = Integer.succ
let pred = Integer.pred
-let msg_emitter = Lattice_messages.register "Offsetmap"
-
(** Offsetmaps are unbalanced trees that map intervals to values, with
the additional properties that the shape of the tree is entirely determined
by the intervals that are mapped (see function [is_above] for the ordering).
@@ -1885,7 +1883,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
if size <~ period then
(* We are going to write the locations that are between [size+1] and
[period] unnecessarily, warn the user *)
- Lattice_messages.emit_approximation msg_emitter
+ Abstract_interp.feedback_approximation
"more than %d(%a) %s. Approximating."
plevel pretty_int number !imprecise_write_msg;
let abs_max = pred (mx +~ size) in
@@ -1895,7 +1893,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
let origin = Origin.(current Misalign_write) in
let v' = V.topify_with_origin origin v in
if not (V.equal v v') then
- Lattice_messages.emit_approximation msg_emitter
+ Abstract_interp.feedback_approximation
"approximating value to write.";
v'
in
@@ -2066,7 +2064,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
| _ -> true (* at least two nodes *)
in
if imprecise then
- Lattice_messages.emit_approximation msg_emitter
+ Abstract_interp.feedback_approximation
"too many locations to update in array. Approximating.";
update ~validity ~exact ~offsets ~size v dst
diff --git a/src/kernel_services/plugin_entry_points/log.mli b/src/kernel_services/plugin_entry_points/log.mli
index d9edffdc5e6080af494920f9076ddcb5a031e6c1..bff4b4c1ddd96304bec45c0f9c3d830746ee12a3 100644
--- a/src/kernel_services/plugin_entry_points/log.mli
+++ b/src/kernel_services/plugin_entry_points/log.mli
@@ -280,8 +280,8 @@ module type Messages = sig
val register_category: string -> category
(** register a new debugging/verbose category.
- Note: categories must be added (e.g. via [add_debug_keys])
- after registration.
+ Note: to enable a category's messages by default, add it
+ (e.g. via [add_debug_keys]) after registration.
@since Fluorine-20130401
*)
@@ -310,14 +310,17 @@ module type Messages = sig
(** returns all registered categories. *)
val add_debug_keys : category -> unit
- (** adds categories corresponding to string (including potential
- subcategories) to the set of categories for which messages are
- to be displayed. The string must have been registered beforehand.
+ (** [add_debug_keys s] enables the emission of messages for the categories
+ corresponding to [s], including potential subcategories (e.g. [a]
+ and [a:b] for string [a:b]).
+ The string must have been registered beforehand.
@since Fluorine-20130401 use categories instead of plain string
*)
val del_debug_keys: category -> unit
- (** removes the given categories from the set for which messages are printed.
+ (** [add_debug_keys s] disables the emission of messages for the categories
+ corresponding to [s], including potential subcategories (e.g. [a]
+ and [a:b] for string [a:b]).
The string must have been registered beforehand.
@since Fluorine-20130401
*)
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index e9a2b40bda7a15f15e13d336e0fafcc3fa849d96..4e35f99b2bbf5d803ba7decea317aa0676a14471 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 b51e860fb2cc9d319d8dc588d68e517a18573841..09e482693ebcc69dd6f91f8992e1c8777fc4e18d 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 774d89fc40dda7ca63cd40f7fe7644081a2a7b0e..f3394b79601cb472c3ea8ed91ec056a8da9bef01 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 9633a07ab0e31c0bef97b7be3027233c2a4bf0db..d869951cfc1be3164af5e93b37a6d197148aac57 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 08a077ea283d0d72948ad4ac7cc139699f42818e..f39a4d733285ec8d04d42eda42999584f45b72d3 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 5e4fbca1c4a14c624435c5b4d0c53eded4b69870..de497bfb3c31b3f80ecd2116fae3572baa8ea539 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 9633a07ab0e31c0bef97b7be3027233c2a4bf0db..d869951cfc1be3164af5e93b37a6d197148aac57 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 166d64faad77cf59fe2003c8dda6ac23d5adf97d..be4a941dc0feddec3e613ff8c030f02294e890d4 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 9633a07ab0e31c0bef97b7be3027233c2a4bf0db..d869951cfc1be3164af5e93b37a6d197148aac57 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 166d64faad77cf59fe2003c8dda6ac23d5adf97d..be4a941dc0feddec3e613ff8c030f02294e890d4 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 110f45908bae6a5907c06fea0ab8efd97a7332c5..9807e0d1eb08e82e3a703f8adb11447241ef35f5 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 b1030ddaf977af058e338597fcfcfe3a21784347..52556e31f524c29ad4f43a53b96d38169fd50a27 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 c4e9465407fd96d671eb527f3df02309a7fb50a4..9454cf0b06ae4e0d9ae2bd7d9774abf5315df96b 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 63882b2cb854348ae9ac35c93939370e9238aec3..d08c3af2ef493470ab4b0626799a5d2506b3742f 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 479f9ea51af0339ef2bb27d509311ae60c658dd8..ff12d80b5234e794ef89cbfe6ebec38a9028f81e 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 d4033b4c6a51235d0b47922c0a7d5a863f79d709..97213131b7b77948a47277c85ca49107461d524e 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 33d782cf04bc117c1285caaed11cb7033a6038b6..7f2b0dde2a94602c62c536533b9a20e92e7ee2cf 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 cef8ba7c8efc1bf83f168322df1c7d05cbf57711..db9c5081b00ff082a29f573f7ea7977afff9d04a 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 f423e4eb8cc93ea8dd508d87d6f093838268f3b4..d72e7dacacb9742e5d6d103753a1c18bd67e3a64 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 1306d9d6c575eaba355d3aa332df2ba32c5ef554..3ed40cfb17bb1523772f49eb7066115547a62c45 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 174d88b2cb0958bb6578a57ae620aef2e75a1bad..925ce57878a424c3185defccbb5e17f79a27119d 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 949bc2e8b3ac72296427a5ca325ec8ff49bb572a..135ef2c480cebc2bffa53589b3311856a450d795 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 10937ade1eb8718fd63fea37a336c372eb48eec5..b0440a8d6a5a417b5e0a2eefeb0652444c7fe67b 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 80295e5723f5bf368e511c973dba796ddd937095..d19a038f2cb62353c97e3e6ede7f83a949ef654e 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 087a06fb508cf64f10b27f25fab056fa094a526e..edf0ba686cb3ab809f0b87c32a069a018a0a33cc 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 d1550923f34b316df820546276a61d03fddce37a..54c2059a1fbf0498cb1fb166080e42fc58a6bec5 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 f423e4eb8cc93ea8dd508d87d6f093838268f3b4..d72e7dacacb9742e5d6d103753a1c18bd67e3a64 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 174d88b2cb0958bb6578a57ae620aef2e75a1bad..925ce57878a424c3185defccbb5e17f79a27119d 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 949bc2e8b3ac72296427a5ca325ec8ff49bb572a..135ef2c480cebc2bffa53589b3311856a450d795 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 69bedb2f07ed82521b0114e6fe43424a93bfd128..510ad3e0141419299d5133c7d211dc5c16bd5f9b 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 80295e5723f5bf368e511c973dba796ddd937095..d19a038f2cb62353c97e3e6ede7f83a949ef654e 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 f423e4eb8cc93ea8dd508d87d6f093838268f3b4..d72e7dacacb9742e5d6d103753a1c18bd67e3a64 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 174d88b2cb0958bb6578a57ae620aef2e75a1bad..925ce57878a424c3185defccbb5e17f79a27119d 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 949bc2e8b3ac72296427a5ca325ec8ff49bb572a..135ef2c480cebc2bffa53589b3311856a450d795 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 bcfcfe9b73aba3286cdfd9e5d2ff8b18f89d0439..9ac7a8268f45a9a01104cb14355f746ac8d5e0ab 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 80295e5723f5bf368e511c973dba796ddd937095..d19a038f2cb62353c97e3e6ede7f83a949ef654e 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