diff --git a/tests/value/domains.i b/tests/value/domains.i
index 4d00d8b9d74ca6102a5ac5e120d4be8f742a5338..cbb0f5f20a9dee7d263eff606510a57ba775fb5b 100644
--- a/tests/value/domains.i
+++ b/tests/value/domains.i
@@ -1,5 +1,9 @@
+/* run.config
+ LOG: domains_dump_0
+ STDOPT: #"-eva-domains sign,equality,bitwise,symbolic-locations,gauges,octagon,multidim -eva-msg-key=d-equality,d-symbolic-locations,d-gauges,d-octagon,d-multidim,d-bitwise,d-sign -eva-warn-key experimental=inactive"
+*/
/* run.config*
- STDOPT: #"-eva-domains sign,equality,bitwise,symbolic-locations,gauges,octagon,multidim"
+ DONTRUN: avoids duplication of domains_dump oracle
*/
volatile int nondet;
@@ -41,4 +45,9 @@ void main (int a) {
/* Tests the bitwise domain: a == 8, no division by zero. */
a = (a | 8) & 8;
r = 10 / a;
+
+ /* Tests printing of domains. */
+ Frama_C_domain_show_each(a, i, j, k, r);
+ Frama_C_dump_each();
+ Frama_C_dump_each_file_domains_dump();
}
diff --git a/tests/value/oracle/domains.res.oracle b/tests/value/oracle/domains.res.oracle
index d4fe3a14f49259e070e14ca2d9d70d781afec137..b18995538801113b434bfd61172445ea64c4403d 100644
--- a/tests/value/oracle/domains.res.oracle
+++ b/tests/value/oracle/domains.res.oracle
@@ -1,12 +1,126 @@
[kernel] Parsing domains.i (no preprocessing)
-[eva:experimental] Warning: The multidim domain is experimental.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
-[eva:partition] domains.i:12: starting to merge loop iterations
-[eva:partition] domains.i:30: starting to merge loop iterations
+[eva:partition] domains.i:16: starting to merge loop iterations
+[eva:partition] domains.i:34: starting to merge loop iterations
+[eva] domains.i:50:
+ Frama_C_domain_show_each:
+ a : # cvalue: {8}
+ # equality:
+ # symbolic-locations: (not implemented)
+ # octagon: (not implemented)
+ # gauges: (not implemented)
+ # sign: +
+ # bitwise: (not implemented)
+ # multidim: {8}
+ i : # cvalue: [1..99]
+ # equality:
+ # symbolic-locations: (not implemented)
+ # octagon: (not implemented)
+ # gauges: (not implemented)
+ # sign: +
+ # bitwise: (not implemented)
+ # multidim: [1..99]
+ j : # cvalue: [10..210]
+ # equality:
+ # symbolic-locations: (not implemented)
+ # octagon: (not implemented)
+ # gauges: (not implemented)
+ # sign: +
+ # bitwise: (not implemented)
+ # multidim: [10..210]
+ k : # cvalue: [2..100]
+ # equality: {k = ((i - j) + 1) + j}
+ # symbolic-locations: (not implemented)
+ # octagon: (not implemented)
+ # gauges: (not implemented)
+ # sign: -0+
+ # bitwise: (not implemented)
+ # multidim: [2..100]
+ r : # cvalue: {1}
+ # equality:
+ # symbolic-locations: (not implemented)
+ # octagon: (not implemented)
+ # gauges: (not implemented)
+ # sign: 0+
+ # bitwise: (not implemented)
+ # multidim: {1}
+[eva] domains.i:51:
+ Frama_C_dump_each:
+ # cvalue:
+ nondet ∈ [--..--]
+ a ∈ {8}
+ i ∈ [1..99]
+ j ∈ [10..210]
+ k ∈ [2..100]
+ r ∈ {1}
+ t[0..63] ∈ [--..--] or UNINITIALIZED
+ [64] ∈ [--..--]
+ [65..99] ∈ [--..--] or UNINITIALIZED
+ b1 ∈ {0; 1}
+ b2 ∈ {0; 1}
+ # equality:
+ {k = ((i - j) + 1) + j}
+ # symbolic-locations:
+ V: {[ t[i] -> [-2147483648..2147483647]
+ t[i] / i -> [-2147483648..2147483647]
+ i - j -> [-209..89]
+ t[k - 1] -> [-2147483648..2147483647] ]}
+ Z: {[ t[i] -> i; t[1..99]
+ t[i] / i -> i; t[1..99]
+ i - j -> i; j
+ t[k - 1] -> k; t[1..99] ]}
+ I: {[ i -> {t[i], t[i] / i, i - j}
+ j -> {i - j}
+ k -> {t[k - 1]}
+ t -> {t[i], t[i] / i, t[k - 1]} ]}
+ S: {[ i -> {t[i], t[i] / i, i - j}
+ j -> {i - j}
+ k -> {t[k - 1]}
+ t -> {t[i], t[i] / i, t[k - 1]} ]}
+ # octagon:
+ {[ i + j ∈ [11..309]
+ j + k ∈ [12..310]
+ j - k ∈ [-90..208]
+ ]}
+ # gauges:
+ V: [{[ a -> {8}
+ i -> [-2147483648..2147483647]
+ j -> [10..210]
+ k -> [-2147483847..2147483848]
+ r -> {1}
+ b1 -> {0; 1}
+ b2 -> {0; 1} ]}]
+
+ # sign:
+ {[ a -> +
+ i -> +
+ j -> +
+ r -> 0+ ]}
+ # bitwise:
+ a[bits 0 to 2] ∈ {0}
+ [bits 3 to 3] ∈ {1}
+ [bits 4 to 31] ∈ {0}
+ # multidim:
+ ({[ a -> ({8}, {})
+ i -> ([1..99], {t})
+ j -> ([10..210], {})
+ k -> ([2..100], {t})
+ r -> ({1}, {})
+ t -> ({
+ [0 .. k - 2] = [-2147483648..2147483647],
+ [k - 1] = [-2147483648..2147483647],
+ [k .. 99] = [-2147483648..2147483647]
+ },
+ {})
+ b1 -> ({0; 1}, {})
+ b2 -> ({0; 1}, {}) ]},
+ None)
+ ==END OF DUMP==
+[eva] domains.i:52: Dumping state in file 'domains_dump_0'
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/domains_dump_0 b/tests/value/oracle/domains_dump_0
new file mode 100644
index 0000000000000000000000000000000000000000..243759089da3fcd59305557fa40fab8634a5e850
--- /dev/null
+++ b/tests/value/oracle/domains_dump_0
@@ -0,0 +1,70 @@
+DUMPING STATE at file domains.i line 52
+# cvalue:
+nondet ∈ [--..--]
+a ∈ {8}
+i ∈ [1..99]
+j ∈ [10..210]
+k ∈ [2..100]
+r ∈ {1}
+t[0..63] ∈ [--..--] or UNINITIALIZED
+ [64] ∈ [--..--]
+ [65..99] ∈ [--..--] or UNINITIALIZED
+b1 ∈ {0; 1}
+b2 ∈ {0; 1}
+# equality:
+{k = ((i - j) + 1) + j}
+# symbolic-locations:
+V: {[ t[i] -> [-2147483648..2147483647]
+ t[i] / i -> [-2147483648..2147483647]
+ i - j -> [-209..89]
+ t[k - 1] -> [-2147483648..2147483647] ]}
+Z: {[ t[i] -> i; t[1..99]
+ t[i] / i -> i; t[1..99]
+ i - j -> i; j
+ t[k - 1] -> k; t[1..99] ]}
+I: {[ i -> {t[i], t[i] / i, i - j}
+ j -> {i - j}
+ k -> {t[k - 1]}
+ t -> {t[i], t[i] / i, t[k - 1]} ]}
+S: {[ i -> {t[i], t[i] / i, i - j}
+ j -> {i - j}
+ k -> {t[k - 1]}
+ t -> {t[i], t[i] / i, t[k - 1]} ]}
+# octagon:
+{[ i + j ∈ [11..309]
+ j + k ∈ [12..310]
+ j - k ∈ [-90..208]
+ ]}
+# gauges:
+V: [{[ a -> {8}
+ i -> [-2147483648..2147483647]
+ j -> [10..210]
+ k -> [-2147483847..2147483848]
+ r -> {1}
+ b1 -> {0; 1}
+ b2 -> {0; 1} ]}]
+
+# sign:
+{[ a -> +
+ i -> +
+ j -> +
+ r -> 0+ ]}
+# bitwise:
+a[bits 0 to 2] ∈ {0}
+ [bits 3 to 3] ∈ {1}
+ [bits 4 to 31] ∈ {0}
+# multidim:
+({[ a -> ({8}, {})
+ i -> ([1..99], {t})
+ j -> ([10..210], {})
+ k -> ([2..100], {t})
+ r -> ({1}, {})
+ t -> ({
+ [0 .. k - 2] = [-2147483648..2147483647],
+ [k - 1] = [-2147483648..2147483647],
+ [k .. 99] = [-2147483648..2147483647]
+ },
+ {})
+ b1 -> ({0; 1}, {})
+ b2 -> ({0; 1}, {}) ]},
+ None)