From 598800a59d3ad4db6414e39bda9d30597e43117a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 17 Sep 2024 16:56:34 +0200
Subject: [PATCH] [Eva] Offsetmap: removes some feedback messages about
approximations.
In offsetmaps, removes a reference to change the feedback emitted when
approximating the write of large memory locations.
Instead, the main offsetmap functor takes an additional parameter about
whether such messages should be emitted. Only the offsetmaps build by the
Eva cvalue domain emits these messages, as write approximations may have a
significant impact on the analysis precision.
Offsetmaps used to represent memory zones or dependiencies do not emit
these messages, which were most often insignificant and instable
(as many plug-ins and Eva domains use memory zones in various ways).
---
src/kernel_services/abstract_interp/cvalue.ml | 6 +-
.../abstract_interp/lmap_bitwise.ml | 4 --
.../abstract_interp/lmap_bitwise.mli | 2 -
.../abstract_interp/offsetmap.ml | 66 +++++++++++--------
.../abstract_interp/offsetmap.mli | 13 ++--
.../abstract_interp/offsetmap_bitwise_sig.ml | 5 --
.../abstract_interp/offsetmap_sig.ml | 4 --
src/plugins/from/from_memory.ml | 2 -
tests/builtins/oracle/imprecise.res.oracle | 8 ---
.../builtins/oracle/linked_list.1.res.oracle | 8 ---
tests/builtins/oracle/memcpy.0.res.oracle | 2 -
.../oracle_equality/imprecise.res.oracle | 11 ----
.../oracle_equality/linked_list.1.res.oracle | 24 -------
.../oracle_gauges/linked_list.1.res.oracle | 2 +-
.../oracle_gauges/memcpy.0.res.oracle | 4 +-
.../oracle_octagon/imprecise.res.oracle | 11 ----
.../oracle_octagon/linked_list.1.res.oracle | 18 -----
.../oracle_symblocs/imprecise.res.oracle | 11 ----
.../oracle_symblocs/linked_list.1.res.oracle | 18 -----
tests/value/oracle/assigns.res.oracle | 2 -
.../oracle/multidim-relations.res.oracle | 14 ----
tests/value/oracle/multidim.res.oracle | 22 -------
tests/value/oracle/non_natural.res.oracle | 52 ---------------
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 | 4 --
.../value/oracle_apron/offsetmap.0.res.oracle | 8 +--
.../value/oracle_apron/offsetmap.1.res.oracle | 8 +--
.../value/oracle_apron/offsetmap.2.res.oracle | 4 +-
.../value/oracle_equality/assigns.res.oracle | 6 --
.../multidim-relations.res.oracle | 18 -----
.../value/oracle_equality/multidim.res.oracle | 28 --------
.../oracle_equality/non_natural.res.oracle | 52 ---------------
.../oracle_equality/offsetmap.0.res.oracle | 4 --
.../oracle_equality/offsetmap.1.res.oracle | 4 --
.../oracle_equality/offsetmap.2.res.oracle | 4 --
tests/value/oracle_equality/plevel.res.oracle | 4 --
.../oracle_gauges/non_natural.res.oracle | 34 ++++------
tests/value/oracle_octagon/assigns.res.oracle | 6 --
.../multidim-relations.res.oracle | 18 -----
.../value/oracle_octagon/multidim.res.oracle | 28 --------
.../oracle_octagon/non_natural.res.oracle | 45 -------------
.../oracle_octagon/offsetmap.0.res.oracle | 4 --
.../oracle_octagon/offsetmap.1.res.oracle | 4 --
.../oracle_octagon/offsetmap.2.res.oracle | 4 --
tests/value/oracle_octagon/plevel.res.oracle | 4 --
.../value/oracle_symblocs/assigns.res.oracle | 6 --
.../multidim-relations.res.oracle | 18 -----
.../value/oracle_symblocs/multidim.res.oracle | 28 --------
.../oracle_symblocs/non_natural.res.oracle | 52 ---------------
.../oracle_symblocs/offsetmap.0.res.oracle | 4 --
.../oracle_symblocs/offsetmap.1.res.oracle | 4 --
.../oracle_symblocs/offsetmap.2.res.oracle | 4 --
tests/value/oracle_symblocs/plevel.res.oracle | 4 --
55 files changed, 79 insertions(+), 647 deletions(-)
delete mode 100644 tests/builtins/oracle_equality/imprecise.res.oracle
delete mode 100644 tests/builtins/oracle_equality/linked_list.1.res.oracle
delete mode 100644 tests/builtins/oracle_octagon/imprecise.res.oracle
delete mode 100644 tests/builtins/oracle_octagon/linked_list.1.res.oracle
delete mode 100644 tests/builtins/oracle_symblocs/imprecise.res.oracle
delete mode 100644 tests/builtins/oracle_symblocs/linked_list.1.res.oracle
delete mode 100644 tests/value/oracle_equality/assigns.res.oracle
delete mode 100644 tests/value/oracle_equality/multidim-relations.res.oracle
delete mode 100644 tests/value/oracle_equality/multidim.res.oracle
delete mode 100644 tests/value/oracle_equality/non_natural.res.oracle
delete mode 100644 tests/value/oracle_equality/offsetmap.0.res.oracle
delete mode 100644 tests/value/oracle_equality/offsetmap.1.res.oracle
delete mode 100644 tests/value/oracle_equality/offsetmap.2.res.oracle
delete mode 100644 tests/value/oracle_equality/plevel.res.oracle
delete mode 100644 tests/value/oracle_octagon/assigns.res.oracle
delete mode 100644 tests/value/oracle_octagon/multidim-relations.res.oracle
delete mode 100644 tests/value/oracle_octagon/multidim.res.oracle
delete mode 100644 tests/value/oracle_octagon/non_natural.res.oracle
delete mode 100644 tests/value/oracle_octagon/offsetmap.0.res.oracle
delete mode 100644 tests/value/oracle_octagon/offsetmap.1.res.oracle
delete mode 100644 tests/value/oracle_octagon/offsetmap.2.res.oracle
delete mode 100644 tests/value/oracle_octagon/plevel.res.oracle
delete mode 100644 tests/value/oracle_symblocs/assigns.res.oracle
delete mode 100644 tests/value/oracle_symblocs/multidim-relations.res.oracle
delete mode 100644 tests/value/oracle_symblocs/multidim.res.oracle
delete mode 100644 tests/value/oracle_symblocs/non_natural.res.oracle
delete mode 100644 tests/value/oracle_symblocs/offsetmap.0.res.oracle
delete mode 100644 tests/value/oracle_symblocs/offsetmap.1.res.oracle
delete mode 100644 tests/value/oracle_symblocs/offsetmap.2.res.oracle
delete mode 100644 tests/value/oracle_symblocs/plevel.res.oracle
diff --git a/src/kernel_services/abstract_interp/cvalue.ml b/src/kernel_services/abstract_interp/cvalue.ml
index 0f70fa34a69..18befa2c686 100644
--- a/src/kernel_services/abstract_interp/cvalue.ml
+++ b/src/kernel_services/abstract_interp/cvalue.ml
@@ -925,7 +925,11 @@ module V_Or_Uninitialized = struct
end
module V_Offsetmap = struct
- include Offsetmap.Make(V_Or_Uninitialized)
+ module Params = struct
+ let approximation_feedback = true
+ end
+
+ include Offsetmap.Make (V_Or_Uninitialized) (Params)
let from_string s =
(* Iterate on s + null terminator; same signature as List.fold_left *)
diff --git a/src/kernel_services/abstract_interp/lmap_bitwise.ml b/src/kernel_services/abstract_interp/lmap_bitwise.ml
index 04ca90b91a1..af05661e44a 100644
--- a/src/kernel_services/abstract_interp/lmap_bitwise.ml
+++ b/src/kernel_services/abstract_interp/lmap_bitwise.ml
@@ -85,8 +85,6 @@ module type Location_map_bitwise = sig
val shape: map -> LOffset.t Hptmap.Shape(Base.Base).t
- val imprecise_write_msg: string ref
-
val clear_caches: unit -> unit
end
@@ -173,8 +171,6 @@ struct
type map = LBase.t
- let imprecise_write_msg = LOffset.imprecise_write_msg
-
let find_or_default b m =
try LBase.find b m
with Not_found -> default_offsetmap b
diff --git a/src/kernel_services/abstract_interp/lmap_bitwise.mli b/src/kernel_services/abstract_interp/lmap_bitwise.mli
index ef6adf28c8b..e0b78eaabe4 100644
--- a/src/kernel_services/abstract_interp/lmap_bitwise.mli
+++ b/src/kernel_services/abstract_interp/lmap_bitwise.mli
@@ -137,8 +137,6 @@ module type Location_map_bitwise = sig
val shape: map -> LOffset.t Hptmap.Shape(Base.Base).t
- val imprecise_write_msg: string ref
-
(** Clear the caches local to this module. Beware that they are not
project-aware, and that you must call them at every project switch. *)
val clear_caches: unit -> unit
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index cce3aad8668..60d836c7675 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -104,7 +104,19 @@ let get_plevel () = !plevel
let debug = false
-module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
+
+module type Parameters = sig
+ val approximation_feedback: bool
+end
+
+module Default_Parameters = struct
+ let approximation_feedback = false
+end
+
+module Make
+ (V : Offsetmap_lattice_with_isotropy.S)
+ (Params: Parameters)
+= struct
open Format
@@ -1841,8 +1853,6 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
aux_update mn mx curr_off tree
;;
- let imprecise_write_msg = ref "locations to update in array"
-
exception Update_Result_is_bottom
(* Returns [true] iff [update_aux_tr_offsets] will approximate the set
@@ -1880,19 +1890,19 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
if number <=~ Integer.of_int plevel || period =~ size then
update_itvs ~exact ~mn ~mx ~period ~size v curr_off t
else begin
- if size <~ period then
+ if size <~ period && Params.approximation_feedback then
(* We are going to write the locations that are between [size+1] and
[period] unnecessarily, warn the user *)
Abstract_interp.feedback_approximation
- "more than %d(%a) %s. Approximating."
- plevel pretty_int number !imprecise_write_msg;
+ "more than %d(%a) locations to update in array. Approximating."
+ plevel pretty_int number;
let abs_max = pred (mx +~ size) in
let v =
if Int.is_zero (period %~ size) then v
else
let origin = Origin.(current Misalign_write) in
let v' = V.topify_with_origin origin v in
- if not (V.equal v v') then
+ if not (V.equal v v') && Params.approximation_feedback then
Abstract_interp.feedback_approximation
"approximating value to write.";
v'
@@ -2063,7 +2073,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
| Node (_, _, Empty, _, Empty, _, _, v', _) -> not (V.equal v v')
| _ -> true (* at least two nodes *)
in
- if imprecise then
+ if imprecise && Params.approximation_feedback then
Abstract_interp.feedback_approximation
"too many locations to update in array. Approximating.";
update ~validity ~exact ~offsets ~size v dst
@@ -2216,30 +2226,28 @@ end
(* --- Intervals --- *)
(* -------------------------------------------------------------------------- *)
-module Int_Intervals_Map = struct
+module Boolean_Value = struct
+ include Datatype.Bool
- include Make(struct
- include Datatype.Bool
+ let bottom = false
+ let join = (||)
+ let is_included b1 b2 = b2 || not b1
+ let merge_neutral_element = bottom
- let bottom = false
- let join = (||)
- let is_included b1 b2 = b2 || not b1
- let merge_neutral_element = bottom
+ let pretty_typ _ fmt v = pretty fmt v
- let pretty_typ _ fmt v = pretty fmt v
+ include FullyIsotropic
+end
- include FullyIsotropic
- end)
+module Int_Intervals_Map = struct
+
+ include Make (Boolean_Value) (Default_Parameters)
include Make_Narrow(struct
let top = true
let narrow = (&&)
end)
- let () =
- imprecise_write_msg := "elements to enumerate"
-
-
(* In this auxiliary module, intervals are pairs [(curr_off, m)] where [m]
has type [bool Offsetmap.t]. However, in order to avoid boxing,
functions sometimes take two arguments: first the current offset,
@@ -2793,12 +2801,14 @@ module Make_bitwise(V: sig
include Lattice_type.With_Top with type t := t
end) = struct
- include Make(struct
- include V
- include FullyIsotropic
- let merge_neutral_element = bottom
- let pretty_typ _ fmt v = pretty fmt v
- end)
+ module Isotropic_Value = struct
+ include V
+ include FullyIsotropic
+ let merge_neutral_element = bottom
+ let pretty_typ _ fmt v = pretty fmt v
+ end
+
+ include Make (Isotropic_Value) (Default_Parameters)
type intervals = Int_Intervals.intervals
diff --git a/src/kernel_services/abstract_interp/offsetmap.mli b/src/kernel_services/abstract_interp/offsetmap.mli
index 51e246111f5..d0950cfab57 100644
--- a/src/kernel_services/abstract_interp/offsetmap.mli
+++ b/src/kernel_services/abstract_interp/offsetmap.mli
@@ -22,12 +22,17 @@
(** Maps from intervals to values. *)
+module type Parameters = sig
+ (** Should offsetmaps emit feedback messages when approximating the write of
+ large memory locations? *)
+ val approximation_feedback: bool
+end
+
(** Maps from intervals to values. The documentation of the returned
maps is in module {!Offsetmap_sig}. *)
-module Make (V : Offsetmap_lattice_with_isotropy.S) :
- Offsetmap_sig.S
- with type v = V.t
- and type widen_hint = V.widen_hint
+module Make (V : Offsetmap_lattice_with_isotropy.S) (_: Parameters) :
+ Offsetmap_sig.S with type v = V.t
+ and type widen_hint = V.widen_hint
(**/**)
(* Exported as Int_Intervals, do not use this module directly *)
diff --git a/src/kernel_services/abstract_interp/offsetmap_bitwise_sig.ml b/src/kernel_services/abstract_interp/offsetmap_bitwise_sig.ml
index 7da3311185c..d736be4315f 100644
--- a/src/kernel_services/abstract_interp/offsetmap_bitwise_sig.ml
+++ b/src/kernel_services/abstract_interp/offsetmap_bitwise_sig.ml
@@ -157,9 +157,4 @@ module type S = sig
project-aware, and that you must call them at every project switch. *)
val clear_caches: unit -> unit
-
- (**/**)
-
- val imprecise_write_msg: string ref
-
end
diff --git a/src/kernel_services/abstract_interp/offsetmap_sig.ml b/src/kernel_services/abstract_interp/offsetmap_sig.ml
index d81994f3664..3e05e3cd024 100644
--- a/src/kernel_services/abstract_interp/offsetmap_sig.ml
+++ b/src/kernel_services/abstract_interp/offsetmap_sig.ml
@@ -284,10 +284,6 @@ module type S = sig
(** {2 Misc} *)
- val imprecise_write_msg: string ref
- (** The message "more than N <imprecise_msg_write>. Approximating." is displayed
- when the offsetmap must update too many locations in one operation. *)
-
(** Clear the caches local to this module. Beware that they are not
project-aware, and that you must call them at every project switch. *)
val clear_caches: unit -> unit
diff --git a/src/plugins/from/from_memory.ml b/src/plugins/from/from_memory.ml
index 2abd4055519..ac4353aa432 100644
--- a/src/plugins/from/from_memory.ml
+++ b/src/plugins/from/from_memory.ml
@@ -196,8 +196,6 @@ let collapse_return x = x
(* ----- Pretty-printing ---------------------------------------------------- *)
-let () = imprecise_write_msg := "dependencies to update"
-
let pretty_skip = function
| DepsOrUnassigned.DepsBottom -> true
| DepsOrUnassigned.Unassigned -> true
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index 4e35f99b2bb..9ce39e3c01e 100644
--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -229,15 +229,7 @@
[eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
[eva] Recording results for many_writes
[from] Computing for function many_writes
-[kernel:approximation] imprecise.c:111:
- more than 200(300) dependencies to update. Approximating.
-[kernel:approximation] imprecise.c:114:
- more than 200(300) dependencies to update. Approximating.
[from] Done for function many_writes
-[kernel:approximation] imprecise.c:111:
- more than 200(300) elements to enumerate. Approximating.
-[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.
Called from imprecise.c:151.
diff --git a/tests/builtins/oracle/linked_list.1.res.oracle b/tests/builtins/oracle/linked_list.1.res.oracle
index 09e482693eb..916c9e2bba8 100644
--- a/tests/builtins/oracle/linked_list.1.res.oracle
+++ b/tests/builtins/oracle/linked_list.1.res.oracle
@@ -811,8 +811,6 @@
has generated a garbled mix of addresses
for assigns clause __fc_stdout->__fc_FILE_data.
[eva] Done for function printf_va_1
-[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:
out of bounds read. assert \valid_read(&curr->val);
@@ -820,8 +818,6 @@
Called from linked_list.c:51.
[eva] Done for function printf_va_1
[eva] Recording results for main
-[kernel:approximation] linked_list.c:44:
- more than 100(128) elements to enumerate. Approximating.
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function malloc:
@@ -843,10 +839,6 @@
[from] Computing for function malloc
[from] Done for function malloc
[from] Computing for function main
-[kernel:approximation] linked_list.c:43:
- more than 100(128) dependencies to update. Approximating.
-[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
[from] Done for function main
diff --git a/tests/builtins/oracle/memcpy.0.res.oracle b/tests/builtins/oracle/memcpy.0.res.oracle
index 4f0cb38f1d5..e683bebda9f 100644
--- a/tests/builtins/oracle/memcpy.0.res.oracle
+++ b/tests/builtins/oracle/memcpy.0.res.oracle
@@ -52,8 +52,6 @@
too many locations to update in array. Approximating.
[kernel:approximation] memcpy.c:53:
more than 150(1000) locations to update in array. 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.
diff --git a/tests/builtins/oracle_equality/imprecise.res.oracle b/tests/builtins/oracle_equality/imprecise.res.oracle
deleted file mode 100644
index d869951cfc1..00000000000
--- a/tests/builtins/oracle_equality/imprecise.res.oracle
+++ /dev/null
@@ -1,11 +0,0 @@
-220a221,222
-> [kernel:approximation] imprecise.c:111:
-> more than 200(300) elements to enumerate. Approximating.
-228a231,232
-> [kernel:approximation] imprecise.c:114:
-> more than 200(300) elements to enumerate. Approximating.
-237,240d240
-< [kernel:approximation] imprecise.c:111:
-< more than 200(300) elements to enumerate. Approximating.
-< [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
deleted file mode 100644
index f39a4d73328..00000000000
--- a/tests/builtins/oracle_equality/linked_list.1.res.oracle
+++ /dev/null
@@ -1,24 +0,0 @@
-488a489,490
-> [kernel:approximation] linked_list.c:19:
-> more than 100(127) elements to enumerate. Approximating.
-542a545,546
-> [kernel:approximation] linked_list.c:43:
-> more than 100(127) elements to enumerate. Approximating.
-544a549,550
-> [kernel:approximation] linked_list.c:44:
-> more than 100(127) elements to enumerate. Approximating.
-673a680,681
-> [kernel:approximation] linked_list.c:19:
-> more than 100(128) elements to enumerate. Approximating.
-718a727,728
-> [kernel:approximation] linked_list.c:43:
-> more than 100(128) elements to enumerate. Approximating.
-720a731,732
-> [kernel:approximation] linked_list.c:44:
-> more than 100(128) elements to enumerate. Approximating.
-814,815d825
-< [kernel:approximation] linked_list.c:51:
-< more than 100(128) elements to enumerate. Approximating.
-823,824d832
-< [kernel:approximation] linked_list.c:44:
-< more than 100(128) elements to enumerate. Approximating.
diff --git a/tests/builtins/oracle_gauges/linked_list.1.res.oracle b/tests/builtins/oracle_gauges/linked_list.1.res.oracle
index b4dd8f6901b..3399b568933 100644
--- a/tests/builtins/oracle_gauges/linked_list.1.res.oracle
+++ b/tests/builtins/oracle_gauges/linked_list.1.res.oracle
@@ -1,4 +1,4 @@
-821a822,827
+819a820,825
> [eva] computing for function printf_va_1 <- main.
> Called from linked_list.c:51.
> [eva] Done for function printf_va_1
diff --git a/tests/builtins/oracle_gauges/memcpy.0.res.oracle b/tests/builtins/oracle_gauges/memcpy.0.res.oracle
index de497bfb3c3..7fa2ad9c849 100644
--- a/tests/builtins/oracle_gauges/memcpy.0.res.oracle
+++ b/tests/builtins/oracle_gauges/memcpy.0.res.oracle
@@ -1,5 +1,5 @@
-149a150,151
+147a148,149
> [eva] memcpy.c:100: Call to builtin memcpy
> [eva] memcpy.c:100: Call to builtin memcpy
-375a378
+373a376
> [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
deleted file mode 100644
index d869951cfc1..00000000000
--- a/tests/builtins/oracle_octagon/imprecise.res.oracle
+++ /dev/null
@@ -1,11 +0,0 @@
-220a221,222
-> [kernel:approximation] imprecise.c:111:
-> more than 200(300) elements to enumerate. Approximating.
-228a231,232
-> [kernel:approximation] imprecise.c:114:
-> more than 200(300) elements to enumerate. Approximating.
-237,240d240
-< [kernel:approximation] imprecise.c:111:
-< more than 200(300) elements to enumerate. Approximating.
-< [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
deleted file mode 100644
index be4a941dc0f..00000000000
--- a/tests/builtins/oracle_octagon/linked_list.1.res.oracle
+++ /dev/null
@@ -1,18 +0,0 @@
-542a543,544
-> [kernel:approximation] linked_list.c:43:
-> more than 100(127) elements to enumerate. Approximating.
-544a547,548
-> [kernel:approximation] linked_list.c:44:
-> more than 100(127) elements to enumerate. Approximating.
-718a723,724
-> [kernel:approximation] linked_list.c:43:
-> more than 100(128) elements to enumerate. Approximating.
-720a727,728
-> [kernel:approximation] linked_list.c:44:
-> more than 100(128) elements to enumerate. Approximating.
-814,815d821
-< [kernel:approximation] linked_list.c:51:
-< more than 100(128) elements to enumerate. Approximating.
-823,824d828
-< [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
deleted file mode 100644
index d869951cfc1..00000000000
--- a/tests/builtins/oracle_symblocs/imprecise.res.oracle
+++ /dev/null
@@ -1,11 +0,0 @@
-220a221,222
-> [kernel:approximation] imprecise.c:111:
-> more than 200(300) elements to enumerate. Approximating.
-228a231,232
-> [kernel:approximation] imprecise.c:114:
-> more than 200(300) elements to enumerate. Approximating.
-237,240d240
-< [kernel:approximation] imprecise.c:111:
-< more than 200(300) elements to enumerate. Approximating.
-< [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
deleted file mode 100644
index be4a941dc0f..00000000000
--- a/tests/builtins/oracle_symblocs/linked_list.1.res.oracle
+++ /dev/null
@@ -1,18 +0,0 @@
-542a543,544
-> [kernel:approximation] linked_list.c:43:
-> more than 100(127) elements to enumerate. Approximating.
-544a547,548
-> [kernel:approximation] linked_list.c:44:
-> more than 100(127) elements to enumerate. Approximating.
-718a723,724
-> [kernel:approximation] linked_list.c:43:
-> more than 100(128) elements to enumerate. Approximating.
-720a727,728
-> [kernel:approximation] linked_list.c:44:
-> more than 100(128) elements to enumerate. Approximating.
-814,815d821
-< [kernel:approximation] linked_list.c:51:
-< more than 100(128) elements to enumerate. Approximating.
-823,824d828
-< [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 9807e0d1eb0..5f6d7ad67fb 100644
--- a/tests/value/oracle/assigns.res.oracle
+++ b/tests/value/oracle/assigns.res.oracle
@@ -152,8 +152,6 @@
[eva] using specification for function f_main4_1
[kernel:approximation] assigns.i:104:
more than 200(1000) locations to update in array. Approximating.
-[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.
diff --git a/tests/value/oracle/multidim-relations.res.oracle b/tests/value/oracle/multidim-relations.res.oracle
index 52556e31f52..7db1f31483f 100644
--- a/tests/value/oracle/multidim-relations.res.oracle
+++ b/tests/value/oracle/multidim-relations.res.oracle
@@ -17,12 +17,6 @@
[kernel:approximation] multidim-relations.c:21:
more than 1(175) locations to update in array. Approximating.
[eva] Recording results for init_array
-[kernel:approximation] multidim-relations.c:19:
- more than 1(350) elements to enumerate. Approximating.
-[kernel:approximation] multidim-relations.c:20:
- more than 1(350) elements to enumerate. Approximating.
-[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.
Called from multidim-relations.c:36.
@@ -43,8 +37,6 @@
[eva:alarm] multidim-relations.c:31: Warning:
out of bounds read. assert \valid_read(t[index].ptr);
[eva] Recording results for use_array
-[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
[eva] Done for function main
@@ -156,12 +148,6 @@
[349].ptr ∈ {{ NULL ; &g }}
index ∈ [0..349]
[from] Computing for function init_array
-[kernel:approximation] multidim-relations.c:19:
- more than 1(350) dependencies to update. Approximating.
-[kernel:approximation] multidim-relations.c:20:
- more than 1(350) dependencies to update. Approximating.
-[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
[from] Done for function set_null
diff --git a/tests/value/oracle/multidim.res.oracle b/tests/value/oracle/multidim.res.oracle
index 9454cf0b06a..bde20fa2538 100644
--- a/tests/value/oracle/multidim.res.oracle
+++ b/tests/value/oracle/multidim.res.oracle
@@ -131,10 +131,6 @@
r : # cvalue: [--..--]
# multidim: { .f = [-3.40282346639e+38 .. 3.40282346639e+38], .i = T }
[eva] Recording results for main3
-[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.
@@ -202,10 +198,6 @@
[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: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.
@@ -229,8 +221,6 @@
[eva] Done for function main9
[eva] Recording results for main
[eva] Done for function main
-[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] ∈ [--..--]
@@ -274,10 +264,6 @@
[from] Computing for function main2
[from] Done for function main2
[from] Computing for function main3
-[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
@@ -288,14 +274,6 @@
[from] Computing for function main6
[from] Done for function main6
[from] Computing for function main7
-[kernel:approximation] multidim.c:136:
- more than 1(1000) dependencies to update. Approximating.
-[kernel:approximation] multidim.c:137:
- more than 1(1000) dependencies to update. Approximating.
-[kernel:approximation] multidim.c:140:
- more than 1(1000) dependencies to update. Approximating.
-[kernel:approximation] multidim.c:141:
- more than 1(1000) dependencies to update. Approximating.
[from] Done for function main7
[from] Computing for function main8
[from] Done for function main8
diff --git a/tests/value/oracle/non_natural.res.oracle b/tests/value/oracle/non_natural.res.oracle
index d08c3af2ef4..740a2e0c5bb 100644
--- a/tests/value/oracle/non_natural.res.oracle
+++ b/tests/value/oracle/non_natural.res.oracle
@@ -121,26 +121,6 @@
(tmp_2 from from++)
[eva] non_natural.i:22: Frama_C_show_each: {{ &p2 + [0..--],0%32 }}
[eva] Recording results for duff1
-[kernel:approximation] non_natural.i:23:
- more than 200(12501) elements to enumerate. Approximating.
-[kernel:approximation] non_natural.i:23:
- more than 200(12500) elements to enumerate. Approximating.
-[kernel:approximation] non_natural.i:24:
- more than 200(12501) elements to enumerate. Approximating.
-[kernel:approximation] non_natural.i:24:
- more than 200(12500) elements to enumerate. Approximating.
-[kernel:approximation] non_natural.i:25:
- more than 200(12500) elements to enumerate. Approximating.
-[kernel:approximation] non_natural.i:26:
- more than 200(12500) elements to enumerate. Approximating.
-[kernel:approximation] non_natural.i:27:
- more than 200(12500) elements to enumerate. Approximating.
-[kernel:approximation] non_natural.i:28:
- more than 200(12500) elements to enumerate. Approximating.
-[kernel:approximation] non_natural.i:29:
- more than 200(12500) elements to enumerate. Approximating.
-[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:
accessing out of bounds index. assert 0 ≤ o;
@@ -277,40 +257,8 @@
[eva:final-states] Values at end of function main:
[from] Computing for function duff1
-[kernel:approximation] non_natural.i:23:
- more than 200(12500) dependencies to update. Approximating.
-[kernel:approximation] non_natural.i:24:
- more than 200(12500) dependencies to update. Approximating.
-[kernel:approximation] non_natural.i:25:
- more than 200(12500) dependencies to update. Approximating.
-[kernel:approximation] non_natural.i:26:
- more than 200(12500) dependencies to update. Approximating.
-[kernel:approximation] non_natural.i:27:
- more than 200(12500) dependencies to update. Approximating.
-[kernel:approximation] non_natural.i:28:
- more than 200(12500) dependencies to update. Approximating.
-[kernel:approximation] non_natural.i:29:
- more than 200(12500) dependencies to update. Approximating.
-[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:approximation] non_natural.i:39:
- more than 200(12500) dependencies to update. Approximating.
-[kernel:approximation] non_natural.i:40:
- more than 200(12500) dependencies to update. Approximating.
-[kernel:approximation] non_natural.i:41:
- more than 200(12500) dependencies to update. Approximating.
-[kernel:approximation] non_natural.i:42:
- more than 200(12500) dependencies to update. Approximating.
-[kernel:approximation] non_natural.i:43:
- more than 200(12500) dependencies to update. Approximating.
-[kernel:approximation] non_natural.i:44:
- more than 200(12500) dependencies to update. Approximating.
-[kernel:approximation] non_natural.i:45:
- more than 200(12500) dependencies to update. Approximating.
-[kernel:approximation] non_natural.i:46:
- more than 200(12500) dependencies to update. Approximating.
[from] Done for function duff2
[from] Computing for function main1
[from] Done for function main1
diff --git a/tests/value/oracle/offsetmap.0.res.oracle b/tests/value/oracle/offsetmap.0.res.oracle
index ff12d80b523..06aae55336a 100644
--- a/tests/value/oracle/offsetmap.0.res.oracle
+++ b/tests/value/oracle/offsetmap.0.res.oracle
@@ -38,8 +38,6 @@
[eva:alarm] offsetmap.i:66: Warning:
accessing out of bounds index. assert i_0 < 10000000;
[eva] Recording results for g
-[kernel:approximation] offsetmap.i:68:
- more than 200(10000000) elements to enumerate. Approximating.
[eva] Done for function g
[eva] computing for function h <- main.
Called from offsetmap.i:110.
diff --git a/tests/value/oracle/offsetmap.1.res.oracle b/tests/value/oracle/offsetmap.1.res.oracle
index 97213131b7b..6dc51d73f9d 100644
--- a/tests/value/oracle/offsetmap.1.res.oracle
+++ b/tests/value/oracle/offsetmap.1.res.oracle
@@ -38,8 +38,6 @@
[eva:alarm] offsetmap.i:66: Warning:
accessing out of bounds index. assert i_0 < 10000000;
[eva] Recording results for g
-[kernel:approximation] offsetmap.i:68:
- more than 200(10000000) elements to enumerate. Approximating.
[eva] Done for function g
[eva] computing for function h <- main.
Called from offsetmap.i:110.
diff --git a/tests/value/oracle/offsetmap.2.res.oracle b/tests/value/oracle/offsetmap.2.res.oracle
index 7f2b0dde2a9..da25a3bf694 100644
--- a/tests/value/oracle/offsetmap.2.res.oracle
+++ b/tests/value/oracle/offsetmap.2.res.oracle
@@ -38,8 +38,6 @@
[eva:alarm] offsetmap.i:66: Warning:
accessing out of bounds index. assert i_0 < 10000000;
[eva] Recording results for g
-[kernel:approximation] offsetmap.i:68:
- more than 200(10000000) elements to enumerate. Approximating.
[eva] Done for function g
[eva] computing for function h <- main.
Called from offsetmap.i:110.
diff --git a/tests/value/oracle/plevel.res.oracle b/tests/value/oracle/plevel.res.oracle
index db9c5081b00..e6ceb709ffe 100644
--- a/tests/value/oracle/plevel.res.oracle
+++ b/tests/value/oracle/plevel.res.oracle
@@ -10,8 +10,6 @@
[kernel:approximation] plevel.i:21:
more than 40(65) locations to update in array. Approximating.
[eva] Recording results for main
-[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:
@@ -104,8 +102,6 @@
i2 ∈ [0..64]
p ∈ {{ &t + [0x2000..0x2040] }}
[from] Computing for function main
-[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_apron/offsetmap.0.res.oracle b/tests/value/oracle_apron/offsetmap.0.res.oracle
index de3bcc8259f..f97a9675c5b 100644
--- a/tests/value/oracle_apron/offsetmap.0.res.oracle
+++ b/tests/value/oracle_apron/offsetmap.0.res.oracle
@@ -1,19 +1,19 @@
-80,81c80
+78,79c78
< a[bits 0 to 7] ∈ {1; 6}
< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
---
> a ∈ {1; 6}
-83,84c82
+81,82c80
< a7[bits 0 to 7] ∈ {1}
< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
---
> a7 ∈ {1}
-142,143c140
+140,141c138
< a[bits 0 to 7] ∈ {1; 6}
< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
---
> a ∈ {1; 6}
-145,146c142
+143,144c140
< a7[bits 0 to 7] ∈ {1}
< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
---
diff --git a/tests/value/oracle_apron/offsetmap.1.res.oracle b/tests/value/oracle_apron/offsetmap.1.res.oracle
index 54a3c9f4893..7ec4d7af6c9 100644
--- a/tests/value/oracle_apron/offsetmap.1.res.oracle
+++ b/tests/value/oracle_apron/offsetmap.1.res.oracle
@@ -1,19 +1,19 @@
-85,86c85
+83,84c83
< a[bits 0 to 7] ∈ {1; 6}
< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
---
> a ∈ {1; 6}
-88,89c87
+86,87c85
< a7[bits 0 to 7] ∈ {1}
< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
---
> a7 ∈ {1}
-138,139c136
+136,137c134
< a[bits 0 to 7] ∈ {1; 6}
< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
---
> a ∈ {1; 6}
-141,142c138
+139,140c136
< a7[bits 0 to 7] ∈ {1}
< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
---
diff --git a/tests/value/oracle_apron/offsetmap.2.res.oracle b/tests/value/oracle_apron/offsetmap.2.res.oracle
index 52b123a5270..6e8472b1c20 100644
--- a/tests/value/oracle_apron/offsetmap.2.res.oracle
+++ b/tests/value/oracle_apron/offsetmap.2.res.oracle
@@ -1,4 +1,4 @@
-80,85c80,82
+78,83c78,80
< a[bits 0 to 7] ∈ {1; 6}
< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
< b[bits 0 to 7] ∈ {0; 1}
@@ -9,7 +9,7 @@
> a ∈ {1; 6}
> b ∈ {0; 1}
> a7 ∈ {1}
-143,148c140,142
+141,146c138,140
< a[bits 0 to 7] ∈ {1; 6}
< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
< b[bits 0 to 7] ∈ {0; 1}
diff --git a/tests/value/oracle_equality/assigns.res.oracle b/tests/value/oracle_equality/assigns.res.oracle
deleted file mode 100644
index d72e7dacacb..00000000000
--- a/tests/value/oracle_equality/assigns.res.oracle
+++ /dev/null
@@ -1,6 +0,0 @@
-154,155d153
-< more than 200(1000) locations to update in array. Approximating.
-< [kernel:approximation] assigns.i:104:
-156a155,156
-> [kernel:approximation] assigns.i:104:
-> more than 200(1000) locations to update in array. Approximating.
diff --git a/tests/value/oracle_equality/multidim-relations.res.oracle b/tests/value/oracle_equality/multidim-relations.res.oracle
deleted file mode 100644
index 925ce57878a..00000000000
--- a/tests/value/oracle_equality/multidim-relations.res.oracle
+++ /dev/null
@@ -1,18 +0,0 @@
-15,19d14
-< [kernel:approximation] multidim-relations.c:20:
-< more than 1(350) locations to update in array. Approximating.
-< [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:approximation] multidim-relations.c:20:
-24a22,23
-> more than 1(175) locations to update in array. Approximating.
-> [kernel:approximation] multidim-relations.c:21:
-25a25
-> [eva] Recording results for init_array
-45d44
-< [eva] Recording results for use_array
-47a47
-> [eva] Recording results for use_array
diff --git a/tests/value/oracle_equality/multidim.res.oracle b/tests/value/oracle_equality/multidim.res.oracle
deleted file mode 100644
index 135ef2c480c..00000000000
--- a/tests/value/oracle_equality/multidim.res.oracle
+++ /dev/null
@@ -1,28 +0,0 @@
-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
deleted file mode 100644
index b0440a8d6a5..00000000000
--- a/tests/value/oracle_equality/non_natural.res.oracle
+++ /dev/null
@@ -1,52 +0,0 @@
-57a58,59
-> [kernel:approximation] non_natural.i:30:
-> more than 200(12500) elements to enumerate. Approximating.
-63a66,69
-> [kernel:approximation] non_natural.i:23:
-> more than 200(12500) elements to enumerate. Approximating.
-> [kernel:approximation] non_natural.i:23:
-> more than 200(12501) elements to enumerate. Approximating.
-68a75,78
-> [kernel:approximation] non_natural.i:24:
-> more than 200(12500) elements to enumerate. Approximating.
-> [kernel:approximation] non_natural.i:24:
-> more than 200(12501) elements to enumerate. Approximating.
-76a87,88
-> [kernel:approximation] non_natural.i:25:
-> more than 200(12500) elements to enumerate. Approximating.
-84a97,98
-> [kernel:approximation] non_natural.i:26:
-> more than 200(12500) elements to enumerate. Approximating.
-92a107,108
-> [kernel:approximation] non_natural.i:27:
-> more than 200(12500) elements to enumerate. Approximating.
-100a117,118
-> [kernel:approximation] non_natural.i:28:
-> more than 200(12500) elements to enumerate. Approximating.
-108a127,128
-> [kernel:approximation] non_natural.i:29:
-> more than 200(12500) elements to enumerate. Approximating.
-124,143d143
-< [kernel:approximation] non_natural.i:23:
-< more than 200(12501) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:23:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:24:
-< more than 200(12501) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:24:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:25:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:26:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:27:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:28:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:29:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:30:
-< more than 200(12500) elements to enumerate. Approximating.
-194a195,196
-> [kernel:approximation] non_natural.i:39:
-> more than 200(12500) elements to enumerate. Approximating.
diff --git a/tests/value/oracle_equality/offsetmap.0.res.oracle b/tests/value/oracle_equality/offsetmap.0.res.oracle
deleted file mode 100644
index 6bebb89e738..00000000000
--- a/tests/value/oracle_equality/offsetmap.0.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-40d39
-< [eva] Recording results for g
-42a42
-> [eva] Recording results for g
diff --git a/tests/value/oracle_equality/offsetmap.1.res.oracle b/tests/value/oracle_equality/offsetmap.1.res.oracle
deleted file mode 100644
index 6bebb89e738..00000000000
--- a/tests/value/oracle_equality/offsetmap.1.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-40d39
-< [eva] Recording results for g
-42a42
-> [eva] Recording results for g
diff --git a/tests/value/oracle_equality/offsetmap.2.res.oracle b/tests/value/oracle_equality/offsetmap.2.res.oracle
deleted file mode 100644
index 6bebb89e738..00000000000
--- a/tests/value/oracle_equality/offsetmap.2.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-40d39
-< [eva] Recording results for g
-42a42
-> [eva] Recording results for g
diff --git a/tests/value/oracle_equality/plevel.res.oracle b/tests/value/oracle_equality/plevel.res.oracle
deleted file mode 100644
index d19a038f2cb..00000000000
--- a/tests/value/oracle_equality/plevel.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-12d11
-< [eva] Recording results for main
-14a14
-> [eva] Recording results for main
diff --git a/tests/value/oracle_gauges/non_natural.res.oracle b/tests/value/oracle_gauges/non_natural.res.oracle
index 54c2059a1fb..2757e23b58d 100644
--- a/tests/value/oracle_gauges/non_natural.res.oracle
+++ b/tests/value/oracle_gauges/non_natural.res.oracle
@@ -59,59 +59,53 @@
< out of bounds read. assert \valid_read(tmp_2);
< (tmp_2 from from++)
< [eva] non_natural.i:22: Frama_C_show_each: {{ &p2 + [0..--],0%32 }}
-125,126d74
-< more than 200(12501) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:23:
-129,130d76
-< more than 200(12501) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:24:
-189,192c135
+169,172c119
< [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++)
---
> [eva] non_natural.i:38: Frama_C_show_each: {{ &p2 + [0..399968],0%32 }}
-195,197d137
+175,177d121
< [eva:alarm] non_natural.i:40: Warning:
< out of bounds write. assert \valid(tmp_1);
< (tmp_1 from to++)
-200,205d139
+180,185d123
< [eva:alarm] non_natural.i:41: Warning:
< out of bounds write. assert \valid(tmp_3);
< (tmp_3 from to++)
< [eva:alarm] non_natural.i:41: Warning:
< out of bounds read. assert \valid_read(tmp_4);
< (tmp_4 from from++)
-208,213d141
+188,193d125
< [eva:alarm] non_natural.i:42: Warning:
< out of bounds write. assert \valid(tmp_5);
< (tmp_5 from to++)
< [eva:alarm] non_natural.i:42: Warning:
< out of bounds read. assert \valid_read(tmp_6);
< (tmp_6 from from++)
-216,221d143
+196,201d127
< [eva:alarm] non_natural.i:43: Warning:
< out of bounds write. assert \valid(tmp_7);
< (tmp_7 from to++)
< [eva:alarm] non_natural.i:43: Warning:
< out of bounds read. assert \valid_read(tmp_8);
< (tmp_8 from from++)
-224,229d145
+204,209d129
< [eva:alarm] non_natural.i:44: Warning:
< out of bounds write. assert \valid(tmp_9);
< (tmp_9 from to++)
< [eva:alarm] non_natural.i:44: Warning:
< out of bounds read. assert \valid_read(tmp_10);
< (tmp_10 from from++)
-232,237d147
+212,217d131
< [eva:alarm] non_natural.i:45: Warning:
< out of bounds write. assert \valid(tmp_11);
< (tmp_11 from to++)
< [eva:alarm] non_natural.i:45: Warning:
< out of bounds read. assert \valid_read(tmp_12);
< (tmp_12 from from++)
-240,253d149
+220,233d133
< [eva:alarm] non_natural.i:46: Warning:
< out of bounds write. assert \valid(tmp_13);
< (tmp_13 from to++)
@@ -126,19 +120,19 @@
< out of bounds read. assert \valid_read(tmp_2);
< (tmp_2 from from++)
< [eva] non_natural.i:38: Frama_C_show_each: {{ &p2 + [0..--],0%32 }}
-262,263c158,159
+242,243c142,143
< to ∈ {{ &p2 + [32..--],0%32 }}
< from ∈ {{ &p1 + [32..--],0%32 }}
---
> to ∈ {{ &p2 + [32..400000],0%32 }}
> from ∈ {{ &p1 + [32..400000],0%32 }}
-267,268c163,164
+247,248c147,148
< to ∈ {{ &p2 + [32..--],0%32 }}
< from ∈ {{ &p1 + [32..--],0%32 }}
---
> to ∈ {{ &p2 + [32..400000],0%32 }}
> from ∈ {{ &p1 + [32..400000],0%32 }}
-324,326c220,228
+272,274c172,180
< p2[0] FROM to; from; count; p1[0..100000] (and SELF)
< [1..99992] FROM to; from; count; p1[0..100001] (and SELF)
< [99993] FROM to; from; count; p1[1..100001] (and SELF)
@@ -152,7 +146,7 @@
> [6] FROM to; from; count; p1[0..99998] (and SELF)
> [7..99992] FROM to; from; count; p1[0..99999] (and SELF)
> [99993] FROM to; from; count; p1[1..99999] (and SELF)
-334,336c236,244
+282,284c188,196
< p2[0] FROM to; from; count; p1[0..100000] (and SELF)
< [1..99992] FROM to; from; count; p1[0..100001] (and SELF)
< [99993] FROM to; from; count; p1[1..100001] (and SELF)
@@ -166,11 +160,11 @@
> [6] FROM to; from; count; p1[0..99998] (and SELF)
> [7..99992] FROM to; from; count; p1[0..99999] (and SELF)
> [99993] FROM to; from; count; p1[1..99999] (and SELF)
-354c262
+302c214
< p1[0..100001]
---
> p1[0..99999]
-359c267
+307c219
< p1[0..100001]
---
> p1[0..99999]
diff --git a/tests/value/oracle_octagon/assigns.res.oracle b/tests/value/oracle_octagon/assigns.res.oracle
deleted file mode 100644
index d72e7dacacb..00000000000
--- a/tests/value/oracle_octagon/assigns.res.oracle
+++ /dev/null
@@ -1,6 +0,0 @@
-154,155d153
-< more than 200(1000) locations to update in array. Approximating.
-< [kernel:approximation] assigns.i:104:
-156a155,156
-> [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
deleted file mode 100644
index 925ce57878a..00000000000
--- a/tests/value/oracle_octagon/multidim-relations.res.oracle
+++ /dev/null
@@ -1,18 +0,0 @@
-15,19d14
-< [kernel:approximation] multidim-relations.c:20:
-< more than 1(350) locations to update in array. Approximating.
-< [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:approximation] multidim-relations.c:20:
-24a22,23
-> more than 1(175) locations to update in array. Approximating.
-> [kernel:approximation] multidim-relations.c:21:
-25a25
-> [eva] Recording results for init_array
-45d44
-< [eva] Recording results for use_array
-47a47
-> [eva] Recording results for use_array
diff --git a/tests/value/oracle_octagon/multidim.res.oracle b/tests/value/oracle_octagon/multidim.res.oracle
deleted file mode 100644
index 135ef2c480c..00000000000
--- a/tests/value/oracle_octagon/multidim.res.oracle
+++ /dev/null
@@ -1,28 +0,0 @@
-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
deleted file mode 100644
index 510ad3e0141..00000000000
--- a/tests/value/oracle_octagon/non_natural.res.oracle
+++ /dev/null
@@ -1,45 +0,0 @@
-57a58,59
-> [kernel:approximation] non_natural.i:30:
-> more than 200(12500) elements to enumerate. Approximating.
-63a66,67
-> [kernel:approximation] non_natural.i:23:
-> more than 200(12500) elements to enumerate. Approximating.
-68a73,74
-> [kernel:approximation] non_natural.i:24:
-> more than 200(12500) elements to enumerate. Approximating.
-76a83,84
-> [kernel:approximation] non_natural.i:25:
-> more than 200(12500) elements to enumerate. Approximating.
-84a93,94
-> [kernel:approximation] non_natural.i:26:
-> more than 200(12500) elements to enumerate. Approximating.
-92a103,104
-> [kernel:approximation] non_natural.i:27:
-> more than 200(12500) elements to enumerate. Approximating.
-100a113,114
-> [kernel:approximation] non_natural.i:28:
-> more than 200(12500) elements to enumerate. Approximating.
-108a123,124
-> [kernel:approximation] non_natural.i:29:
-> more than 200(12500) elements to enumerate. Approximating.
-126,127d141
-< [kernel:approximation] non_natural.i:23:
-< more than 200(12500) elements to enumerate. Approximating.
-130,143d143
-< [kernel:approximation] non_natural.i:24:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:25:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:26:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:27:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:28:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:29:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:30:
-< more than 200(12500) elements to enumerate. Approximating.
-194a195,196
-> [kernel:approximation] non_natural.i:39:
-> more than 200(12500) elements to enumerate. Approximating.
diff --git a/tests/value/oracle_octagon/offsetmap.0.res.oracle b/tests/value/oracle_octagon/offsetmap.0.res.oracle
deleted file mode 100644
index 6bebb89e738..00000000000
--- a/tests/value/oracle_octagon/offsetmap.0.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-40d39
-< [eva] Recording results for g
-42a42
-> [eva] Recording results for g
diff --git a/tests/value/oracle_octagon/offsetmap.1.res.oracle b/tests/value/oracle_octagon/offsetmap.1.res.oracle
deleted file mode 100644
index 6bebb89e738..00000000000
--- a/tests/value/oracle_octagon/offsetmap.1.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-40d39
-< [eva] Recording results for g
-42a42
-> [eva] Recording results for g
diff --git a/tests/value/oracle_octagon/offsetmap.2.res.oracle b/tests/value/oracle_octagon/offsetmap.2.res.oracle
deleted file mode 100644
index 6bebb89e738..00000000000
--- a/tests/value/oracle_octagon/offsetmap.2.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-40d39
-< [eva] Recording results for g
-42a42
-> [eva] Recording results for g
diff --git a/tests/value/oracle_octagon/plevel.res.oracle b/tests/value/oracle_octagon/plevel.res.oracle
deleted file mode 100644
index d19a038f2cb..00000000000
--- a/tests/value/oracle_octagon/plevel.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-12d11
-< [eva] Recording results for main
-14a14
-> [eva] Recording results for main
diff --git a/tests/value/oracle_symblocs/assigns.res.oracle b/tests/value/oracle_symblocs/assigns.res.oracle
deleted file mode 100644
index d72e7dacacb..00000000000
--- a/tests/value/oracle_symblocs/assigns.res.oracle
+++ /dev/null
@@ -1,6 +0,0 @@
-154,155d153
-< more than 200(1000) locations to update in array. Approximating.
-< [kernel:approximation] assigns.i:104:
-156a155,156
-> [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
deleted file mode 100644
index 925ce57878a..00000000000
--- a/tests/value/oracle_symblocs/multidim-relations.res.oracle
+++ /dev/null
@@ -1,18 +0,0 @@
-15,19d14
-< [kernel:approximation] multidim-relations.c:20:
-< more than 1(350) locations to update in array. Approximating.
-< [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:approximation] multidim-relations.c:20:
-24a22,23
-> more than 1(175) locations to update in array. Approximating.
-> [kernel:approximation] multidim-relations.c:21:
-25a25
-> [eva] Recording results for init_array
-45d44
-< [eva] Recording results for use_array
-47a47
-> [eva] Recording results for use_array
diff --git a/tests/value/oracle_symblocs/multidim.res.oracle b/tests/value/oracle_symblocs/multidim.res.oracle
deleted file mode 100644
index 135ef2c480c..00000000000
--- a/tests/value/oracle_symblocs/multidim.res.oracle
+++ /dev/null
@@ -1,28 +0,0 @@
-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
deleted file mode 100644
index 9ac7a8268f4..00000000000
--- a/tests/value/oracle_symblocs/non_natural.res.oracle
+++ /dev/null
@@ -1,52 +0,0 @@
-57a58,59
-> [kernel:approximation] non_natural.i:30:
-> more than 200(12500) elements to enumerate. Approximating.
-63a66,69
-> [kernel:approximation] non_natural.i:23:
-> more than 200(12501) elements to enumerate. Approximating.
-> [kernel:approximation] non_natural.i:23:
-> more than 200(12500) elements to enumerate. Approximating.
-68a75,78
-> [kernel:approximation] non_natural.i:24:
-> more than 200(12501) elements to enumerate. Approximating.
-> [kernel:approximation] non_natural.i:24:
-> more than 200(12500) elements to enumerate. Approximating.
-76a87,88
-> [kernel:approximation] non_natural.i:25:
-> more than 200(12500) elements to enumerate. Approximating.
-84a97,98
-> [kernel:approximation] non_natural.i:26:
-> more than 200(12500) elements to enumerate. Approximating.
-92a107,108
-> [kernel:approximation] non_natural.i:27:
-> more than 200(12500) elements to enumerate. Approximating.
-100a117,118
-> [kernel:approximation] non_natural.i:28:
-> more than 200(12500) elements to enumerate. Approximating.
-108a127,128
-> [kernel:approximation] non_natural.i:29:
-> more than 200(12500) elements to enumerate. Approximating.
-124,143d143
-< [kernel:approximation] non_natural.i:23:
-< more than 200(12501) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:23:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:24:
-< more than 200(12501) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:24:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:25:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:26:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:27:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:28:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:29:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel:approximation] non_natural.i:30:
-< more than 200(12500) elements to enumerate. Approximating.
-194a195,196
-> [kernel:approximation] non_natural.i:39:
-> more than 200(12500) elements to enumerate. Approximating.
diff --git a/tests/value/oracle_symblocs/offsetmap.0.res.oracle b/tests/value/oracle_symblocs/offsetmap.0.res.oracle
deleted file mode 100644
index 6bebb89e738..00000000000
--- a/tests/value/oracle_symblocs/offsetmap.0.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-40d39
-< [eva] Recording results for g
-42a42
-> [eva] Recording results for g
diff --git a/tests/value/oracle_symblocs/offsetmap.1.res.oracle b/tests/value/oracle_symblocs/offsetmap.1.res.oracle
deleted file mode 100644
index 6bebb89e738..00000000000
--- a/tests/value/oracle_symblocs/offsetmap.1.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-40d39
-< [eva] Recording results for g
-42a42
-> [eva] Recording results for g
diff --git a/tests/value/oracle_symblocs/offsetmap.2.res.oracle b/tests/value/oracle_symblocs/offsetmap.2.res.oracle
deleted file mode 100644
index 6bebb89e738..00000000000
--- a/tests/value/oracle_symblocs/offsetmap.2.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-40d39
-< [eva] Recording results for g
-42a42
-> [eva] Recording results for g
diff --git a/tests/value/oracle_symblocs/plevel.res.oracle b/tests/value/oracle_symblocs/plevel.res.oracle
deleted file mode 100644
index d19a038f2cb..00000000000
--- a/tests/value/oracle_symblocs/plevel.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-12d11
-< [eva] Recording results for main
-14a14
-> [eva] Recording results for main
--
GitLab