diff --git a/src/kernel_services/abstract_interp/cvalue.ml b/src/kernel_services/abstract_interp/cvalue.ml
index 0f70fa34a69c724a18bfa008569ffc981e691867..18befa2c68690b2f7e426867f0c1a63a1e890d30 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 04ca90b91a1f88c7162772b7a03210119cd593fa..af05661e44a6572a9f3780def7031e2226eafa76 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 ef6adf28c8be16f4ceb87c5f63eb1a7925da5269..e0b78eaabe441d81efa4144ea090bb241a0a5dda 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 cce3aad86684f1a42066c0f350b138d45b95563b..60d836c76750d3ec4e954a3bc4c11ba93dc34cc0 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 51e246111f556cacea0119df4ca1116ec125fde1..d0950cfab57af2bdeff0714623a1401c295ba0ac 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 7da3311185ca30c80aeea75b75f4f93dd04a7417..d736be4315f04352764f32f231165a0a1499e510 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 d81994f3664e48d1774ddcb0526fcdfd5d4863ae..3e05e3cd024c5eb24f6f557515d9564bed6136e3 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 2abd40555195a0aae26bc58b21ebded10672fd5c..ac4353aa432dd68b83af518da0e78d6b0b0a78ad 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 4e35f99b2bbf5d803ba7decea317aa0676a14471..9ce39e3c01e4abf49e1d0d8ed6ec935bbad2d1a0 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 09e482693ebcc69dd6f91f8992e1c8777fc4e18d..916c9e2bba809abbcd4abc13454d1183d6998a5a 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 4f0cb38f1d5dd9ab9abf9ac38dffdd1891f5c825..e683bebda9fec44017edfc23cb10fdedb187ebb5 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 d869951cfc1be3164af5e93b37a6d197148aac57..0000000000000000000000000000000000000000
--- 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 f39a4d733285ec8d04d42eda42999584f45b72d3..0000000000000000000000000000000000000000
--- 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 b4dd8f6901bfedbeff231430246bb6c77f704f48..3399b56893377bacf830b1dab266375436de9624 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 de497bfb3c31b3f80ecd2116fae3572baa8ea539..7fa2ad9c849599b9e4314ca1094afabc9d067b95 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 d869951cfc1be3164af5e93b37a6d197148aac57..0000000000000000000000000000000000000000
--- 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 be4a941dc0feddec3e613ff8c030f02294e890d4..0000000000000000000000000000000000000000
--- 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 d869951cfc1be3164af5e93b37a6d197148aac57..0000000000000000000000000000000000000000
--- 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 be4a941dc0feddec3e613ff8c030f02294e890d4..0000000000000000000000000000000000000000
--- 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 9807e0d1eb08e82e3a703f8adb11447241ef35f5..5f6d7ad67fbd51414d5aad503a4495a7dfce64d8 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 52556e31f524c29ad4f43a53b96d38169fd50a27..7db1f31483f3375d3c1e675854122b11cfad1696 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 9454cf0b06ae4e0d9ae2bd7d9774abf5315df96b..bde20fa25384bc73393a1e890d13878819f3ff9f 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 d08c3af2ef493470ab4b0626799a5d2506b3742f..740a2e0c5bb98a0f89f3383a5d0f9b2f331c9f62 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 ff12d80b5234e794ef89cbfe6ebec38a9028f81e..06aae55336ac9d0ec151ea67bf569e499e7dec6e 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 97213131b7b77948a47277c85ca49107461d524e..6dc51d73f9deb114f896384e49bee9ec04e12459 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 7f2b0dde2a94602c62c536533b9a20e92e7ee2cf..da25a3bf6947d30e936409e855b61340ccc1d48b 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 db9c5081b00ff082a29f573f7ea7977afff9d04a..e6ceb709ffe6aab641d5fddf67f5f7d4aba2faf9 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 de3bcc8259f51fdbaa5cc414730f5b47e136fb58..f97a9675c5b67ed7f382ad9db0936c0c22cdf572 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 54a3c9f489329f9a6bf1d759101941258998c93a..7ec4d7af6c99c032a5d3fa92816f9ed376959dbf 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 52b123a5270b1f90da06bb944213992a0677b987..6e8472b1c2097f46e92411bf9c3339522012e967 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 d72e7dacacb9742e5d6d103753a1c18bd67e3a64..0000000000000000000000000000000000000000
--- 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 925ce57878a424c3185defccbb5e17f79a27119d..0000000000000000000000000000000000000000
--- 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 135ef2c480cebc2bffa53589b3311856a450d795..0000000000000000000000000000000000000000
--- 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 b0440a8d6a5a417b5e0a2eefeb0652444c7fe67b..0000000000000000000000000000000000000000
--- 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 6bebb89e738e4c6703b3d8b869f9d852e34a9e44..0000000000000000000000000000000000000000
--- 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 6bebb89e738e4c6703b3d8b869f9d852e34a9e44..0000000000000000000000000000000000000000
--- 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 6bebb89e738e4c6703b3d8b869f9d852e34a9e44..0000000000000000000000000000000000000000
--- 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 d19a038f2cb62353c97e3e6ede7f83a949ef654e..0000000000000000000000000000000000000000
--- 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 54c2059a1fbf0498cb1fb166080e42fc58a6bec5..2757e23b58d3f4e670b78bc310ea7f5c2343fc50 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 d72e7dacacb9742e5d6d103753a1c18bd67e3a64..0000000000000000000000000000000000000000
--- 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 925ce57878a424c3185defccbb5e17f79a27119d..0000000000000000000000000000000000000000
--- 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 135ef2c480cebc2bffa53589b3311856a450d795..0000000000000000000000000000000000000000
--- 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 510ad3e0141419299d5133c7d211dc5c16bd5f9b..0000000000000000000000000000000000000000
--- 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 6bebb89e738e4c6703b3d8b869f9d852e34a9e44..0000000000000000000000000000000000000000
--- 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 6bebb89e738e4c6703b3d8b869f9d852e34a9e44..0000000000000000000000000000000000000000
--- 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 6bebb89e738e4c6703b3d8b869f9d852e34a9e44..0000000000000000000000000000000000000000
--- 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 d19a038f2cb62353c97e3e6ede7f83a949ef654e..0000000000000000000000000000000000000000
--- 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 d72e7dacacb9742e5d6d103753a1c18bd67e3a64..0000000000000000000000000000000000000000
--- 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 925ce57878a424c3185defccbb5e17f79a27119d..0000000000000000000000000000000000000000
--- 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 135ef2c480cebc2bffa53589b3311856a450d795..0000000000000000000000000000000000000000
--- 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 9ac7a8268f45a9a01104cb14355f746ac8d5e0ab..0000000000000000000000000000000000000000
--- 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 6bebb89e738e4c6703b3d8b869f9d852e34a9e44..0000000000000000000000000000000000000000
--- 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 6bebb89e738e4c6703b3d8b869f9d852e34a9e44..0000000000000000000000000000000000000000
--- 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 6bebb89e738e4c6703b3d8b869f9d852e34a9e44..0000000000000000000000000000000000000000
--- 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 d19a038f2cb62353c97e3e6ede7f83a949ef654e..0000000000000000000000000000000000000000
--- 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