diff --git a/src/plugins/eva/domains/domain_builder.ml b/src/plugins/eva/domains/domain_builder.ml
index 0305ca8a35fdbb53e57fdbe620642bffc3d7151a..5eb36d90703a1f5f995033729a1874ff84f1121a 100644
--- a/src/plugins/eva/domains/domain_builder.ml
+++ b/src/plugins/eva/domains/domain_builder.ml
@@ -291,6 +291,12 @@ end
(* -------------------------------------------------------------------------- *)
+let unique_name =
+ let counter = ref 0 in
+ fun name ->
+ incr counter;
+ name ^ string_of_int !counter
+
module Restrict
(Value: Abstract_value.S)
(Domain: Abstract.Domain.Internal with type value = Value.t)
@@ -328,11 +334,13 @@ module Restrict
transfer functions are applied accordingly. The current mode is replaced
at function calls by [mode.calls]. *)
- module Info = struct let module_name = Domain.name ^ " restricted" end
- module D = Datatype.Pair_with_collections (Domain) (Mode) (Info)
+ let info suffix =
+ let name = unique_name (Domain.name ^ " " ^ suffix) in
+ let module Info = struct let module_name = name end in
+ (module Info: Datatype.Functor_info)
- module I = struct let module_name = Domain.name ^ " option" end
- include Datatype.Option_with_collections (D) (I)
+ module D = Datatype.Pair_with_collections (Domain) (Mode) (val info "restricted")
+ include Datatype.Option_with_collections (D) (val info "option")
let name = Domain.name
let default = Domain.top, Mode.all
diff --git a/tests/value/domains_function.c b/tests/value/domains_function.c
index e81f3e8c8dca745264423d081f29bb7c163c5dbf..7102ea22c396e3eab8ecc61fdf1734ef3ba19fad 100644
--- a/tests/value/domains_function.c
+++ b/tests/value/domains_function.c
@@ -1,5 +1,6 @@
/* run.config*
STDOPT: #"-eva-domains-function symbolic-locations:infer+w,symbolic-locations:use+r,symbolic-locations:test_propagation-,symbolic-locations:enabled,symbolic-locations:disabled-,symbolic-locations:recursively_enabled+"
+ STDOPT: #"-eva @EVA_CONFIG@ -main test_successive_runs -eva-domains-function octagon:need_symbolic_locations,symbolic-locations:need_octagon -then -eva-domains-function symbolic-locations:need_symbolic_locations,octagon:need_octagon"
*/
#include <__fc_builtin.h>
@@ -121,3 +122,25 @@ void main () {
recursively_enabled ();
test_propagation ();
}
+
+
+int need_octagon(int x, int y) {
+ if (x < y)
+ return y - x;
+ else
+ return x - y;
+}
+
+int need_symbolic_locations(int x, int y) {
+ int *p = undet ? &x : &y;
+ if (*p < 10) return *p;
+ return 0;
+}
+
+void test_successive_runs (void) {
+ int a = Frama_C_interval(-100, 100);
+ int b = Frama_C_interval(-100, 100);
+ int abs_diff = need_octagon(a, b);
+ int bounded = need_symbolic_locations(abs_diff, abs_diff);
+ //@ check 0 <= bounded < 10;
+}
diff --git a/tests/value/oracle/domains_function.res.oracle b/tests/value/oracle/domains_function.0.res.oracle
similarity index 83%
rename from tests/value/oracle/domains_function.res.oracle
rename to tests/value/oracle/domains_function.0.res.oracle
index b1050fa92af30c1a108018657d54cf82c6883434..b0dcbe8be76de6eb9ee9ddd6faa6c10b2fc22352 100644
--- a/tests/value/oracle/domains_function.res.oracle
+++ b/tests/value/oracle/domains_function.0.res.oracle
@@ -7,96 +7,96 @@
i ∈ {0}
result ∈ {0}
t[0..9] ∈ {0}
-[eva] domains_function.c:117: starting to merge loop iterations
+[eva] domains_function.c:118: starting to merge loop iterations
[eva] computing for function Frama_C_interval <- main.
- Called from domains_function.c:119.
+ Called from domains_function.c:120.
[eva] using specification for function Frama_C_interval
-[eva] domains_function.c:119:
+[eva] domains_function.c:120:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function test <- main.
- Called from domains_function.c:120.
-[eva] domains_function.c:92: Frama_C_show_each_top: [-2147483648..2147483647]
+ Called from domains_function.c:121.
+[eva] domains_function.c:93: Frama_C_show_each_top: [-2147483648..2147483647]
[eva] computing for function enabled <- test <- main.
- Called from domains_function.c:93.
+ Called from domains_function.c:94.
[eva] Recording results for enabled
[eva] Done for function enabled
-[eva] domains_function.c:94: Frama_C_show_each_singleton: {0}
+[eva] domains_function.c:95: Frama_C_show_each_singleton: {0}
[eva] computing for function not_enabled <- test <- main.
- Called from domains_function.c:95.
-[eva] domains_function.c:77: Frama_C_show_each_top: [-2147483648..2147483647]
+ Called from domains_function.c:96.
+[eva] domains_function.c:78: Frama_C_show_each_top: [-2147483648..2147483647]
[eva] Recording results for not_enabled
[eva] Done for function not_enabled
-[eva] domains_function.c:96: Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] domains_function.c:97: Frama_C_show_each_top: [-2147483648..2147483647]
[eva] computing for function disabled <- test <- main.
- Called from domains_function.c:97.
-[eva] domains_function.c:84: Frama_C_show_each_top: [-2147483648..2147483647]
+ Called from domains_function.c:98.
+[eva] domains_function.c:85: Frama_C_show_each_top: [-2147483648..2147483647]
[eva] Recording results for disabled
[eva] Done for function disabled
-[eva] domains_function.c:98: Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] domains_function.c:99: Frama_C_show_each_top: [-2147483648..2147483647]
[eva] Recording results for test
[eva] Done for function test
[eva] computing for function recursively_enabled <- main.
- Called from domains_function.c:121.
-[eva] domains_function.c:107: Frama_C_show_each_singleton: {4}
+ Called from domains_function.c:122.
+[eva] domains_function.c:108: Frama_C_show_each_singleton: {4}
[eva] computing for function enabled <- recursively_enabled <- main.
- Called from domains_function.c:108.
+ Called from domains_function.c:109.
[eva] Recording results for enabled
[eva] Done for function enabled
-[eva] domains_function.c:109: Frama_C_show_each_singleton: {0}
+[eva] domains_function.c:110: Frama_C_show_each_singleton: {0}
[eva] computing for function not_enabled <- recursively_enabled <- main.
- Called from domains_function.c:110.
-[eva] domains_function.c:77: Frama_C_show_each_top: {1}
+ Called from domains_function.c:111.
+[eva] domains_function.c:78: Frama_C_show_each_top: {1}
[eva] Recording results for not_enabled
[eva] Done for function not_enabled
-[eva] domains_function.c:111: Frama_C_show_each_singleton: {1}
+[eva] domains_function.c:112: Frama_C_show_each_singleton: {1}
[eva] computing for function disabled <- recursively_enabled <- main.
- Called from domains_function.c:112.
-[eva] domains_function.c:84: Frama_C_show_each_top: [-2147483648..2147483647]
+ Called from domains_function.c:113.
+[eva] domains_function.c:85: Frama_C_show_each_top: [-2147483648..2147483647]
[eva] Recording results for disabled
[eva] Done for function disabled
-[eva] domains_function.c:113: Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] domains_function.c:114: Frama_C_show_each_top: [-2147483648..2147483647]
[eva] Recording results for recursively_enabled
[eva] Done for function recursively_enabled
[eva] computing for function test_propagation <- main.
- Called from domains_function.c:122.
+ Called from domains_function.c:123.
[eva] computing for function infer <- test_propagation <- main.
- Called from domains_function.c:53.
+ Called from domains_function.c:54.
[eva] Recording results for infer
[eva] Done for function infer
[eva] computing for function no_use <- test_propagation <- main.
- Called from domains_function.c:54.
+ Called from domains_function.c:55.
[eva] Recording results for no_use
[eva] Done for function no_use
-[eva] domains_function.c:55: Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] domains_function.c:56: Frama_C_show_each_top: [-2147483648..2147483647]
[eva] computing for function nothing <- test_propagation <- main.
- Called from domains_function.c:56.
-[eva:alarm] domains_function.c:21: Warning:
+ Called from domains_function.c:57.
+[eva:alarm] domains_function.c:22: Warning:
signed overflow. assert -2147483648 ≤ t[i] - t[0];
-[eva:alarm] domains_function.c:21: Warning:
+[eva:alarm] domains_function.c:22: Warning:
signed overflow. assert t[i] - t[0] ≤ 2147483647;
[eva] Recording results for nothing
[eva] Done for function nothing
[eva] computing for function use <- test_propagation <- main.
- Called from domains_function.c:57.
+ Called from domains_function.c:58.
[eva] Recording results for use
[eva] Done for function use
-[eva] domains_function.c:58: Frama_C_show_each_singleton: {42}
+[eva] domains_function.c:59: Frama_C_show_each_singleton: {42}
[eva] computing for function kill <- test_propagation <- main.
- Called from domains_function.c:59.
+ Called from domains_function.c:60.
[eva] Recording results for kill
[eva] Done for function kill
[eva] computing for function use <- test_propagation <- main.
- Called from domains_function.c:60.
+ Called from domains_function.c:61.
[eva] Recording results for use
[eva] Done for function use
-[eva] domains_function.c:61: Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] domains_function.c:62: Frama_C_show_each_top: [-2147483648..2147483647]
[eva] computing for function no_infer <- test_propagation <- main.
- Called from domains_function.c:62.
+ Called from domains_function.c:63.
[eva] Recording results for no_infer
[eva] Done for function no_infer
-[eva] domains_function.c:63: Reusing old results for call to use
-[eva] domains_function.c:64: Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] domains_function.c:64: Reusing old results for call to use
+[eva] domains_function.c:65: Frama_C_show_each_top: [-2147483648..2147483647]
[eva] Recording results for test_propagation
[eva] Done for function test_propagation
[eva] Recording results for main
diff --git a/tests/value/oracle/domains_function.1.res.oracle b/tests/value/oracle/domains_function.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f61f3f2b85b1057d110eec3ea9f40041062e8763
--- /dev/null
+++ b/tests/value/oracle/domains_function.1.res.oracle
@@ -0,0 +1,112 @@
+[kernel] Parsing domains_function.c (with preprocessing)
+[eva] Analyzing a complete application starting at test_successive_runs
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ undet ∈ [--..--]
+ i ∈ {0}
+ result ∈ {0}
+ t[0..9] ∈ {0}
+[eva] computing for function Frama_C_interval <- test_successive_runs.
+ Called from domains_function.c:141.
+[eva] using specification for function Frama_C_interval
+[eva] domains_function.c:141:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- test_successive_runs.
+ Called from domains_function.c:142.
+[eva] domains_function.c:142:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function need_octagon <- test_successive_runs.
+ Called from domains_function.c:143.
+[eva] Recording results for need_octagon
+[eva] Done for function need_octagon
+[eva] computing for function need_symbolic_locations <- test_successive_runs.
+ Called from domains_function.c:144.
+[eva] Recording results for need_symbolic_locations
+[eva] Done for function need_symbolic_locations
+[eva:alarm] domains_function.c:145: Warning: check got status unknown.
+[eva] Recording results for test_successive_runs
+[eva] Done for function test_successive_runs
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function need_octagon:
+ __retres ∈ [-200..200]
+[eva:final-states] Values at end of function need_symbolic_locations:
+ p ∈ {{ &x ; &y }}
+ __retres ∈ [-200..200]
+[eva:final-states] Values at end of function test_successive_runs:
+ Frama_C_entropy_source ∈ [--..--]
+ a ∈ [-100..100]
+ b ∈ [-100..100]
+ abs_diff ∈ [-200..200]
+ bounded ∈ [-200..200]
+[eva] Analyzing a complete application starting at test_successive_runs
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ undet ∈ [--..--]
+ i ∈ {0}
+ result ∈ {0}
+ t[0..9] ∈ {0}
+[eva] computing for function Frama_C_interval <- test_successive_runs.
+ Called from domains_function.c:141.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- test_successive_runs.
+ Called from domains_function.c:142.
+[eva] Done for function Frama_C_interval
+[eva] computing for function need_octagon <- test_successive_runs.
+ Called from domains_function.c:143.
+[eva] Recording results for need_octagon
+[eva] Done for function need_octagon
+[eva] computing for function need_symbolic_locations <- test_successive_runs.
+ Called from domains_function.c:144.
+[eva] Recording results for need_symbolic_locations
+[eva] Done for function need_symbolic_locations
+[eva] domains_function.c:145: check got status valid.
+[eva] Recording results for test_successive_runs
+[eva] Done for function test_successive_runs
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function need_octagon:
+ __retres ∈ [0..200]
+[eva:final-states] Values at end of function need_symbolic_locations:
+ p ∈ {{ &x ; &y }}
+ __retres ∈ [0..9]
+[eva:final-states] Values at end of function test_successive_runs:
+ Frama_C_entropy_source ∈ [--..--]
+ a ∈ [-100..100]
+ b ∈ [-100..100]
+ abs_diff ∈ [0..200]
+ bounded ∈ [0..9]
+[from] Computing for function need_octagon
+[from] Done for function need_octagon
+[from] Computing for function need_symbolic_locations
+[from] Done for function need_symbolic_locations
+[from] Computing for function test_successive_runs
+[from] Computing for function Frama_C_interval <-test_successive_runs
+[from] Done for function Frama_C_interval
+[from] Done for function test_successive_runs
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ \result FROM Frama_C_entropy_source; min; max
+[from] Function need_octagon:
+ \result FROM x; y
+[from] Function need_symbolic_locations:
+ \result FROM undet; x; y
+[from] Function test_successive_runs:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function need_octagon:
+ __retres
+[inout] Inputs for function need_octagon:
+ \nothing
+[inout] Out (internal) for function need_symbolic_locations:
+ p; tmp; __retres
+[inout] Inputs for function need_symbolic_locations:
+ undet
+[inout] Out (internal) for function test_successive_runs:
+ Frama_C_entropy_source; a; b; abs_diff; bounded
+[inout] Inputs for function test_successive_runs:
+ Frama_C_entropy_source; undet
diff --git a/tests/value/oracle_apron/domains_function.res.oracle b/tests/value/oracle_apron/domains_function.0.res.oracle
similarity index 58%
rename from tests/value/oracle_apron/domains_function.res.oracle
rename to tests/value/oracle_apron/domains_function.0.res.oracle
index dfc16dbd1e5521d3367b5fae2667a03ac1e29129..7bd70b448da71492602e75fbd2718a2f524d75ec 100644
--- a/tests/value/oracle_apron/domains_function.res.oracle
+++ b/tests/value/oracle_apron/domains_function.0.res.oracle
@@ -1,7 +1,7 @@
98c98,101
-< [eva] domains_function.c:63: Reusing old results for call to use
+< [eva] domains_function.c:64: Reusing old results for call to use
---
> [eva] computing for function use <- test_propagation <- main.
-> Called from domains_function.c:63.
+> Called from domains_function.c:64.
> [eva] Recording results for use
> [eva] Done for function use
diff --git a/tests/value/oracle_apron/domains_function.1.res.oracle b/tests/value/oracle_apron/domains_function.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3ac4b39aeb2ff9ba5056110d6bd119d7cd34bd90
--- /dev/null
+++ b/tests/value/oracle_apron/domains_function.1.res.oracle
@@ -0,0 +1,14 @@
+34c34
+< __retres ∈ [-200..200]
+---
+> __retres ∈ [0..200]
+37c37
+< __retres ∈ [-200..200]
+---
+> __retres ∈ [0..200]
+42,43c42,43
+< abs_diff ∈ [-200..200]
+< bounded ∈ [-200..200]
+---
+> abs_diff ∈ [0..200]
+> bounded ∈ [0..200]
diff --git a/tests/value/oracle_equality/domains_function.0.res.oracle b/tests/value/oracle_equality/domains_function.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0d3df09d21d067f91afda619c343e5376bff32d1
--- /dev/null
+++ b/tests/value/oracle_equality/domains_function.0.res.oracle
@@ -0,0 +1,52 @@
+19c19
+< [eva] domains_function.c:93: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] domains_function.c:93: Frama_C_show_each_top: {3}
+27c27
+< [eva] domains_function.c:78: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] domains_function.c:78: Frama_C_show_each_top: {1}
+30c30
+< [eva] domains_function.c:97: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] domains_function.c:97: Frama_C_show_each_top: {1}
+33c33
+< [eva] domains_function.c:85: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] domains_function.c:85: Frama_C_show_each_top: {2}
+36c36
+< [eva] domains_function.c:99: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] domains_function.c:99: Frama_C_show_each_top: {2}
+55c55
+< [eva] domains_function.c:85: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] domains_function.c:85: Frama_C_show_each_top: {2}
+58c58
+< [eva] domains_function.c:114: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] domains_function.c:114: Frama_C_show_each_top: {2}
+71c71
+< [eva] domains_function.c:56: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] domains_function.c:56: Frama_C_show_each_top: {42}
+99c99
+< [eva] domains_function.c:65: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] domains_function.c:65: Frama_C_show_each_top: {42}
+106c106
+< result ∈ [--..--]
+---
+> result ∈ {2}
+120c120
+< result ∈ [--..--]
+---
+> result ∈ {1}
+125c125
+< result ∈ [--..--]
+---
+> result ∈ {2}
+128c128
+< result ∈ [--..--]
+---
+> result ∈ {2}
diff --git a/tests/value/oracle_equality/domains_function.res.oracle b/tests/value/oracle_equality/domains_function.res.oracle
deleted file mode 100644
index 792b3d12a6ca5ec8f9b3d7743707b1c0d92d369b..0000000000000000000000000000000000000000
--- a/tests/value/oracle_equality/domains_function.res.oracle
+++ /dev/null
@@ -1,52 +0,0 @@
-19c19
-< [eva] domains_function.c:92: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] domains_function.c:92: Frama_C_show_each_top: {3}
-27c27
-< [eva] domains_function.c:77: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] domains_function.c:77: Frama_C_show_each_top: {1}
-30c30
-< [eva] domains_function.c:96: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] domains_function.c:96: Frama_C_show_each_top: {1}
-33c33
-< [eva] domains_function.c:84: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] domains_function.c:84: Frama_C_show_each_top: {2}
-36c36
-< [eva] domains_function.c:98: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] domains_function.c:98: Frama_C_show_each_top: {2}
-55c55
-< [eva] domains_function.c:84: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] domains_function.c:84: Frama_C_show_each_top: {2}
-58c58
-< [eva] domains_function.c:113: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] domains_function.c:113: Frama_C_show_each_top: {2}
-71c71
-< [eva] domains_function.c:55: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] domains_function.c:55: Frama_C_show_each_top: {42}
-99c99
-< [eva] domains_function.c:64: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] domains_function.c:64: Frama_C_show_each_top: {42}
-106c106
-< result ∈ [--..--]
----
-> result ∈ {2}
-120c120
-< result ∈ [--..--]
----
-> result ∈ {1}
-125c125
-< result ∈ [--..--]
----
-> result ∈ {2}
-128c128
-< result ∈ [--..--]
----
-> result ∈ {2}
diff --git a/tests/value/oracle_multidim/domains_function.0.res.oracle b/tests/value/oracle_multidim/domains_function.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..59b6f16e4956a1abebbdd254732e80a446a79a8a
--- /dev/null
+++ b/tests/value/oracle_multidim/domains_function.0.res.oracle
@@ -0,0 +1,76 @@
+19c19
+< [eva] domains_function.c:93: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] domains_function.c:93: Frama_C_show_each_top: {3}
+27c27
+< [eva] domains_function.c:78: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] domains_function.c:78: Frama_C_show_each_top: {1}
+30c30
+< [eva] domains_function.c:97: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] domains_function.c:97: Frama_C_show_each_top: {1}
+33c33
+< [eva] domains_function.c:85: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] domains_function.c:85: Frama_C_show_each_top: {2}
+36c36
+< [eva] domains_function.c:99: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] domains_function.c:99: Frama_C_show_each_top: {2}
+55c55
+< [eva] domains_function.c:85: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] domains_function.c:85: Frama_C_show_each_top: {2}
+58c58
+< [eva] domains_function.c:114: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] domains_function.c:114: Frama_C_show_each_top: {2}
+71c71
+< [eva] domains_function.c:56: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] domains_function.c:56: Frama_C_show_each_top: {42}
+75,76d74
+< signed overflow. assert -2147483648 ≤ t[i] - t[0];
+< [eva:alarm] domains_function.c:22: Warning:
+98,99c96,100
+< [eva] domains_function.c:64: Reusing old results for call to use
+< [eva] domains_function.c:65: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] computing for function use <- test_propagation <- main.
+> Called from domains_function.c:64.
+> [eva] Recording results for use
+> [eva] Done for function use
+> [eva] domains_function.c:65: Frama_C_show_each_top: {42}
+106c107
+< result ∈ [--..--]
+---
+> result ∈ {2}
+118c119
+< result ∈ [--..--]
+---
+> result ∈ {42}
+120c121
+< result ∈ [--..--]
+---
+> result ∈ {1}
+123c124
+< tmp ∈ [--..--]
+---
+> tmp ∈ [-2147483605..2147483647]
+125c126
+< result ∈ [--..--]
+---
+> result ∈ {2}
+128c129
+< result ∈ [--..--]
+---
+> result ∈ {2}
+133c134
+< result ∈ [--..--]
+---
+> result ∈ {42}
+138c139
+< result ∈ [--..--]
+---
+> result ∈ {42}
diff --git a/tests/value/oracle_multidim/domains_function.res.oracle b/tests/value/oracle_multidim/domains_function.res.oracle
deleted file mode 100644
index fe35793aa66912b4d82c8a7bd06278cf123bec57..0000000000000000000000000000000000000000
--- a/tests/value/oracle_multidim/domains_function.res.oracle
+++ /dev/null
@@ -1,76 +0,0 @@
-19c19
-< [eva] domains_function.c:92: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] domains_function.c:92: Frama_C_show_each_top: {3}
-27c27
-< [eva] domains_function.c:77: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] domains_function.c:77: Frama_C_show_each_top: {1}
-30c30
-< [eva] domains_function.c:96: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] domains_function.c:96: Frama_C_show_each_top: {1}
-33c33
-< [eva] domains_function.c:84: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] domains_function.c:84: Frama_C_show_each_top: {2}
-36c36
-< [eva] domains_function.c:98: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] domains_function.c:98: Frama_C_show_each_top: {2}
-55c55
-< [eva] domains_function.c:84: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] domains_function.c:84: Frama_C_show_each_top: {2}
-58c58
-< [eva] domains_function.c:113: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] domains_function.c:113: Frama_C_show_each_top: {2}
-71c71
-< [eva] domains_function.c:55: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] domains_function.c:55: Frama_C_show_each_top: {42}
-75,76d74
-< signed overflow. assert -2147483648 ≤ t[i] - t[0];
-< [eva:alarm] domains_function.c:21: Warning:
-98,99c96,100
-< [eva] domains_function.c:63: Reusing old results for call to use
-< [eva] domains_function.c:64: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] computing for function use <- test_propagation <- main.
-> Called from domains_function.c:63.
-> [eva] Recording results for use
-> [eva] Done for function use
-> [eva] domains_function.c:64: Frama_C_show_each_top: {42}
-106c107
-< result ∈ [--..--]
----
-> result ∈ {2}
-118c119
-< result ∈ [--..--]
----
-> result ∈ {42}
-120c121
-< result ∈ [--..--]
----
-> result ∈ {1}
-123c124
-< tmp ∈ [--..--]
----
-> tmp ∈ [-2147483605..2147483647]
-125c126
-< result ∈ [--..--]
----
-> result ∈ {2}
-128c129
-< result ∈ [--..--]
----
-> result ∈ {2}
-133c134
-< result ∈ [--..--]
----
-> result ∈ {42}
-138c139
-< result ∈ [--..--]
----
-> result ∈ {42}
diff --git a/tests/value/oracle_octagon/domains_function.1.res.oracle b/tests/value/oracle_octagon/domains_function.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3ac4b39aeb2ff9ba5056110d6bd119d7cd34bd90
--- /dev/null
+++ b/tests/value/oracle_octagon/domains_function.1.res.oracle
@@ -0,0 +1,14 @@
+34c34
+< __retres ∈ [-200..200]
+---
+> __retres ∈ [0..200]
+37c37
+< __retres ∈ [-200..200]
+---
+> __retres ∈ [0..200]
+42,43c42,43
+< abs_diff ∈ [-200..200]
+< bounded ∈ [-200..200]
+---
+> abs_diff ∈ [0..200]
+> bounded ∈ [0..200]
diff --git a/tests/value/oracle_symblocs/domains_function.0.res.oracle b/tests/value/oracle_symblocs/domains_function.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..21a6dd7fef7774da3182f28468f31a7ee3f2bea3
--- /dev/null
+++ b/tests/value/oracle_symblocs/domains_function.0.res.oracle
@@ -0,0 +1,32 @@
+19c19
+< [eva] domains_function.c:93: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] domains_function.c:93: Frama_C_show_each_top: {3}
+27c27
+< [eva] domains_function.c:78: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] domains_function.c:78: Frama_C_show_each_top: {1}
+30c30
+< [eva] domains_function.c:97: Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] domains_function.c:97: Frama_C_show_each_top: {1}
+47,51c47
+< [eva] computing for function not_enabled <- recursively_enabled <- main.
+< Called from domains_function.c:111.
+< [eva] domains_function.c:78: Frama_C_show_each_top: {1}
+< [eva] Recording results for not_enabled
+< [eva] Done for function not_enabled
+---
+> [eva] domains_function.c:111: Reusing old results for call to not_enabled
+53,57c49
+< [eva] computing for function disabled <- recursively_enabled <- main.
+< Called from domains_function.c:113.
+< [eva] domains_function.c:85: Frama_C_show_each_top: [-2147483648..2147483647]
+< [eva] Recording results for disabled
+< [eva] Done for function disabled
+---
+> [eva] domains_function.c:113: Reusing old results for call to disabled
+120c112
+< result ∈ [--..--]
+---
+> result ∈ {1}
diff --git a/tests/value/oracle_symblocs/domains_function.1.res.oracle b/tests/value/oracle_symblocs/domains_function.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f3da9ca881e4a46f79cdf988fd926e33ae9599dc
--- /dev/null
+++ b/tests/value/oracle_symblocs/domains_function.1.res.oracle
@@ -0,0 +1,8 @@
+37c37
+< __retres ∈ [-200..200]
+---
+> __retres ∈ [-200..9]
+43c43
+< bounded ∈ [-200..200]
+---
+> bounded ∈ [-200..9]
diff --git a/tests/value/oracle_symblocs/domains_function.res.oracle b/tests/value/oracle_symblocs/domains_function.res.oracle
deleted file mode 100644
index 580c761d0eecaeee54cd954f62f21a4547d170b6..0000000000000000000000000000000000000000
--- a/tests/value/oracle_symblocs/domains_function.res.oracle
+++ /dev/null
@@ -1,32 +0,0 @@
-19c19
-< [eva] domains_function.c:92: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] domains_function.c:92: Frama_C_show_each_top: {3}
-27c27
-< [eva] domains_function.c:77: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] domains_function.c:77: Frama_C_show_each_top: {1}
-30c30
-< [eva] domains_function.c:96: Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] domains_function.c:96: Frama_C_show_each_top: {1}
-47,51c47
-< [eva] computing for function not_enabled <- recursively_enabled <- main.
-< Called from domains_function.c:110.
-< [eva] domains_function.c:77: Frama_C_show_each_top: {1}
-< [eva] Recording results for not_enabled
-< [eva] Done for function not_enabled
----
-> [eva] domains_function.c:110: Reusing old results for call to not_enabled
-53,57c49
-< [eva] computing for function disabled <- recursively_enabled <- main.
-< Called from domains_function.c:112.
-< [eva] domains_function.c:84: Frama_C_show_each_top: [-2147483648..2147483647]
-< [eva] Recording results for disabled
-< [eva] Done for function disabled
----
-> [eva] domains_function.c:112: Reusing old results for call to disabled
-120c112
-< result ∈ [--..--]
----
-> result ∈ {1}