From e2918a3831a3915030b7a52de38ba4c7433dbc44 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 29 Jan 2021 14:21:58 +0100
Subject: [PATCH] [Tests] adds symblocs_SUITES = value
---
tests/ptests_config | 4 +-
tests/test_config_octagons | 2 +-
tests/test_config_symblocs | 2 +-
.../value/oracle_symblocs/alias.0.res.oracle | 10 +++
.../value/oracle_symblocs/alias.4.res.oracle | 4 ++
.../value/oracle_symblocs/alias.5.res.oracle | 4 ++
.../value/oracle_symblocs/alias.6.res.oracle | 4 ++
.../bitwise_pointer.res.oracle | 8 +++
.../bitwise_reduction.res.oracle | 16 +++++
.../oracle_symblocs/builtins_split.res.oracle | 4 ++
.../domains_function.res.oracle | 32 +++++++++
.../incompatible_states.res.oracle | 7 ++
.../value/oracle_symblocs/library.res.oracle | 5 ++
.../oracle_symblocs/non_natural.res.oracle | 52 ++++++++++++++
.../oracle_symblocs/offsetmap.0.res.oracle | 4 ++
.../oracle_symblocs/offsetmap.1.res.oracle | 4 ++
tests/value/oracle_symblocs/plevel.res.oracle | 4 ++
.../oracle_symblocs/ptr_relation.0.res.oracle | 4 ++
.../redundant_alarms.res.oracle | 41 +++++++++++
.../oracle_symblocs/relations2.res.oracle | 2 +
.../value/oracle_symblocs/struct2.res.oracle | 27 +++++++
.../oracle_symblocs/symbolic_locs.res.oracle | 71 +++++++++++++++++++
tests/value/oracle_symblocs/test.0.res.oracle | 4 ++
23 files changed, 311 insertions(+), 4 deletions(-)
create mode 100644 tests/value/oracle_symblocs/alias.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/alias.4.res.oracle
create mode 100644 tests/value/oracle_symblocs/alias.5.res.oracle
create mode 100644 tests/value/oracle_symblocs/alias.6.res.oracle
create mode 100644 tests/value/oracle_symblocs/bitwise_pointer.res.oracle
create mode 100644 tests/value/oracle_symblocs/bitwise_reduction.res.oracle
create mode 100644 tests/value/oracle_symblocs/builtins_split.res.oracle
create mode 100644 tests/value/oracle_symblocs/domains_function.res.oracle
create mode 100644 tests/value/oracle_symblocs/incompatible_states.res.oracle
create mode 100644 tests/value/oracle_symblocs/library.res.oracle
create mode 100644 tests/value/oracle_symblocs/non_natural.res.oracle
create mode 100644 tests/value/oracle_symblocs/offsetmap.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/offsetmap.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/plevel.res.oracle
create mode 100644 tests/value/oracle_symblocs/ptr_relation.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/redundant_alarms.res.oracle
create mode 100644 tests/value/oracle_symblocs/relations2.res.oracle
create mode 100644 tests/value/oracle_symblocs/struct2.res.oracle
create mode 100644 tests/value/oracle_symblocs/symbolic_locs.res.oracle
create mode 100644 tests/value/oracle_symblocs/test.0.res.oracle
diff --git a/tests/ptests_config b/tests/ptests_config
index 5349af09d3b..964235ffa75 100644
--- a/tests/ptests_config
+++ b/tests/ptests_config
@@ -20,11 +20,11 @@ bitwise_SUITES = value
equalities_SUITES = value
gauges_SUITES = value
IGNORE= octagon_SUITES = value
-IGNORE= symbols_SUITES = value
+symblocs_SUITES = value
IGNORE= apron_SUITES = value/numerors
IGNORE= bitwise_SUITES = value/numerors
IGNORE= equalities_SUITES = value/numerors
IGNORE= gauges_SUITES = value/numerors
IGNORE= octagon_SUITES = value/numerors
-IGNORE= symbols_SUITES = value/numerors
+IGNORE= symblocs_SUITES = value/numerors
diff --git a/tests/test_config_octagons b/tests/test_config_octagons
index 729a49e20e9..7173c08e0f3 100644
--- a/tests/test_config_octagons
+++ b/tests/test_config_octagons
@@ -6,4 +6,4 @@ MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
FILTER: diff %{dep:../oracle/@PTEST_ORACLE@}
PLUGIN: @EVA_PLUGINS@
-OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
+OPT: -eva @EVA_CONFIG@ -out -input -deps
diff --git a/tests/test_config_symblocs b/tests/test_config_symblocs
index b18fa6cd55f..908e42246f0 100644
--- a/tests/test_config_symblocs
+++ b/tests/test_config_symblocs
@@ -6,4 +6,4 @@ MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
FILTER: diff %{dep:../oracle/@PTEST_ORACLE@}
PLUGIN: @EVA_PLUGINS@
-OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
+OPT: -eva @EVA_CONFIG@ -out -input -deps
diff --git a/tests/value/oracle_symblocs/alias.0.res.oracle b/tests/value/oracle_symblocs/alias.0.res.oracle
new file mode 100644
index 00000000000..c234ab23c2e
--- /dev/null
+++ b/tests/value/oracle_symblocs/alias.0.res.oracle
@@ -0,0 +1,10 @@
+103,104c103,104
+< t ∈ {1; 2; 4}
+< u ∈ {2; 3; 4; 5}
+---
+> t ∈ {4}
+> u ∈ {5}
+110c110
+< t2 ∈ {0; 3; 6}
+---
+> t2 ∈ {6}
diff --git a/tests/value/oracle_symblocs/alias.4.res.oracle b/tests/value/oracle_symblocs/alias.4.res.oracle
new file mode 100644
index 00000000000..a9bf84a72d6
--- /dev/null
+++ b/tests/value/oracle_symblocs/alias.4.res.oracle
@@ -0,0 +1,4 @@
+80c80
+< y ∈ {0; 3; 77}
+---
+> y ∈ {77}
diff --git a/tests/value/oracle_symblocs/alias.5.res.oracle b/tests/value/oracle_symblocs/alias.5.res.oracle
new file mode 100644
index 00000000000..42399641f15
--- /dev/null
+++ b/tests/value/oracle_symblocs/alias.5.res.oracle
@@ -0,0 +1,4 @@
+167c167
+< y ∈ {0; 3; 77}
+---
+> y ∈ {77}
diff --git a/tests/value/oracle_symblocs/alias.6.res.oracle b/tests/value/oracle_symblocs/alias.6.res.oracle
new file mode 100644
index 00000000000..a7dfd303175
--- /dev/null
+++ b/tests/value/oracle_symblocs/alias.6.res.oracle
@@ -0,0 +1,4 @@
+86c86
+< x ∈ {0; 4; 33}
+---
+> x ∈ {33}
diff --git a/tests/value/oracle_symblocs/bitwise_pointer.res.oracle b/tests/value/oracle_symblocs/bitwise_pointer.res.oracle
new file mode 100644
index 00000000000..f04f7077977
--- /dev/null
+++ b/tests/value/oracle_symblocs/bitwise_pointer.res.oracle
@@ -0,0 +1,8 @@
+62c62
+< x ∈ [0..9]
+---
+> x ∈ {5}
+75c75
+< x1 ∈ [0..9]
+---
+> x1 ∈ {5}
diff --git a/tests/value/oracle_symblocs/bitwise_reduction.res.oracle b/tests/value/oracle_symblocs/bitwise_reduction.res.oracle
new file mode 100644
index 00000000000..9906de0d474
--- /dev/null
+++ b/tests/value/oracle_symblocs/bitwise_reduction.res.oracle
@@ -0,0 +1,16 @@
+18c18
+< {0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
+---
+> {0; 1}, {0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
+21c21
+< {0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
+---
+> {0; 1}, {0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
+27c27
+< {{ &t + {0; 4} }}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
+---
+> {{ &t + {0; 4} }}, {0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
+30c30
+< {0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
+---
+> {0; 1}, {0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
diff --git a/tests/value/oracle_symblocs/builtins_split.res.oracle b/tests/value/oracle_symblocs/builtins_split.res.oracle
new file mode 100644
index 00000000000..9e88f384bc8
--- /dev/null
+++ b/tests/value/oracle_symblocs/builtins_split.res.oracle
@@ -0,0 +1,4 @@
+51c51
+< Frama_C_show_each_t_i_2: {1; 2; 3; 4; 5; 6; 7; 8}, {0; 4; 8; 12}
+---
+> Frama_C_show_each_t_i_2: {1; 2; 3; 4; 5; 6; 7; 8}, {8}
diff --git a/tests/value/oracle_symblocs/domains_function.res.oracle b/tests/value/oracle_symblocs/domains_function.res.oracle
new file mode 100644
index 00000000000..580c761d0ee
--- /dev/null
+++ b/tests/value/oracle_symblocs/domains_function.res.oracle
@@ -0,0 +1,32 @@
+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}
diff --git a/tests/value/oracle_symblocs/incompatible_states.res.oracle b/tests/value/oracle_symblocs/incompatible_states.res.oracle
new file mode 100644
index 00000000000..2b99b73cb02
--- /dev/null
+++ b/tests/value/oracle_symblocs/incompatible_states.res.oracle
@@ -0,0 +1,7 @@
+41,42d40
+< [eva:alarm] incompatible_states.c:53: Warning:
+< division by zero. assert t[i] ≢ 0;
+49c47
+< [scope:rm_asserts] removing 2 assertion(s)
+---
+> [scope:rm_asserts] removing 1 assertion(s)
diff --git a/tests/value/oracle_symblocs/library.res.oracle b/tests/value/oracle_symblocs/library.res.oracle
new file mode 100644
index 00000000000..7414f97802c
--- /dev/null
+++ b/tests/value/oracle_symblocs/library.res.oracle
@@ -0,0 +1,5 @@
+122,125d121
+< [eva:alarm] library.i:44: Warning:
+< non-finite float value. assert \is_finite(*pf);
+< [eva:alarm] library.i:44: Warning:
+< non-finite float value. assert \is_finite(\add_float(*pf, *pf));
diff --git a/tests/value/oracle_symblocs/non_natural.res.oracle b/tests/value/oracle_symblocs/non_natural.res.oracle
new file mode 100644
index 00000000000..bcfcfe9b73a
--- /dev/null
+++ b/tests/value/oracle_symblocs/non_natural.res.oracle
@@ -0,0 +1,52 @@
+57a58,59
+> [kernel] non_natural.i:30:
+> more than 200(12500) elements to enumerate. Approximating.
+63a66,69
+> [kernel] non_natural.i:23:
+> more than 200(12501) elements to enumerate. Approximating.
+> [kernel] non_natural.i:23:
+> more than 200(12500) elements to enumerate. Approximating.
+68a75,78
+> [kernel] non_natural.i:24:
+> more than 200(12501) elements to enumerate. Approximating.
+> [kernel] non_natural.i:24:
+> more than 200(12500) elements to enumerate. Approximating.
+76a87,88
+> [kernel] non_natural.i:25:
+> more than 200(12500) elements to enumerate. Approximating.
+84a97,98
+> [kernel] non_natural.i:26:
+> more than 200(12500) elements to enumerate. Approximating.
+92a107,108
+> [kernel] non_natural.i:27:
+> more than 200(12500) elements to enumerate. Approximating.
+100a117,118
+> [kernel] non_natural.i:28:
+> more than 200(12500) elements to enumerate. Approximating.
+108a127,128
+> [kernel] non_natural.i:29:
+> more than 200(12500) elements to enumerate. Approximating.
+124,143d143
+< [kernel] non_natural.i:23:
+< more than 200(12501) elements to enumerate. Approximating.
+< [kernel] non_natural.i:23:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] non_natural.i:24:
+< more than 200(12501) elements to enumerate. Approximating.
+< [kernel] non_natural.i:24:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] non_natural.i:25:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] non_natural.i:26:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] non_natural.i:27:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] non_natural.i:28:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] non_natural.i:29:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] non_natural.i:30:
+< more than 200(12500) elements to enumerate. Approximating.
+194a195,196
+> [kernel] 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
new file mode 100644
index 00000000000..6bebb89e738
--- /dev/null
+++ b/tests/value/oracle_symblocs/offsetmap.0.res.oracle
@@ -0,0 +1,4 @@
+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
new file mode 100644
index 00000000000..6bebb89e738
--- /dev/null
+++ b/tests/value/oracle_symblocs/offsetmap.1.res.oracle
@@ -0,0 +1,4 @@
+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
new file mode 100644
index 00000000000..80295e5723f
--- /dev/null
+++ b/tests/value/oracle_symblocs/plevel.res.oracle
@@ -0,0 +1,4 @@
+12d11
+< [eva] Recording results for main
+13a13
+> [eva] Recording results for main
diff --git a/tests/value/oracle_symblocs/ptr_relation.0.res.oracle b/tests/value/oracle_symblocs/ptr_relation.0.res.oracle
new file mode 100644
index 00000000000..0ae744ec7d6
--- /dev/null
+++ b/tests/value/oracle_symblocs/ptr_relation.0.res.oracle
@@ -0,0 +1,4 @@
+23c23
+< i ∈ {0; 77; 333}
+---
+> i ∈ {77}
diff --git a/tests/value/oracle_symblocs/redundant_alarms.res.oracle b/tests/value/oracle_symblocs/redundant_alarms.res.oracle
new file mode 100644
index 00000000000..e3d4eaf7271
--- /dev/null
+++ b/tests/value/oracle_symblocs/redundant_alarms.res.oracle
@@ -0,0 +1,41 @@
+10,13d9
+< [eva:alarm] redundant_alarms.c:12: Warning:
+< accessing uninitialized left-value. assert \initialized(p);
+< [eva:alarm] redundant_alarms.c:13: Warning:
+< accessing uninitialized left-value. assert \initialized(p);
+24,27d19
+< [eva:alarm] redundant_alarms.c:22: Warning:
+< accessing uninitialized left-value. assert \initialized(&t[i]);
+< [eva:alarm] redundant_alarms.c:23: Warning:
+< accessing uninitialized left-value. assert \initialized(&t[i]);
+38,41d29
+< [eva:alarm] redundant_alarms.c:33: Warning:
+< accessing uninitialized left-value. assert \initialized(&t[j]);
+< [eva:alarm] redundant_alarms.c:34: Warning:
+< accessing uninitialized left-value. assert \initialized(&t[i]);
+61,67d48
+< [scope:rm_asserts] removing 3 assertion(s)
+< [scope:rm_asserts] redundant_alarms.c:13:
+< removing redundant assert Eva: initialization: \initialized(p);
+< [scope:rm_asserts] redundant_alarms.c:33:
+< removing redundant assert Eva: initialization: \initialized(&t[j]);
+< [scope:rm_asserts] redundant_alarms.c:34:
+< removing redundant assert Eva: initialization: \initialized(&t[i]);
+106d86
+< /*@ assert Eva: initialization: \initialized(p); */
+108d87
+< /*@ assert Eva: initialization: \initialized(p); */
+125d103
+< /*@ assert Eva: initialization: \initialized(&t[i]); */
+127d104
+< /*@ assert Eva: initialization: \initialized(&t[i]); */
+140d116
+< /*@ assert Eva: initialization: \initialized(&t[j]); */
+142d117
+< /*@ assert Eva: initialization: \initialized(&t[i]); */
+194a170
+> int z;
+197,199d172
+< *p = 1;
+< int z = *p + 1;
+< int w = *p + 2;
diff --git a/tests/value/oracle_symblocs/relations2.res.oracle b/tests/value/oracle_symblocs/relations2.res.oracle
new file mode 100644
index 00000000000..c58e8b748b8
--- /dev/null
+++ b/tests/value/oracle_symblocs/relations2.res.oracle
@@ -0,0 +1,2 @@
+132d131
+< [eva] relations2.i:57: Frama_C_show_each_NO2:
diff --git a/tests/value/oracle_symblocs/struct2.res.oracle b/tests/value/oracle_symblocs/struct2.res.oracle
new file mode 100644
index 00000000000..85c9191577e
--- /dev/null
+++ b/tests/value/oracle_symblocs/struct2.res.oracle
@@ -0,0 +1,27 @@
+53a54,55
+> [kernel] struct2.i:78: Warning:
+> all target addresses were invalid. This path is assumed to be dead.
+57,58d58
+< accessing out of bounds index. assert 0 ≤ (int)(tab2[i] + j);
+< [eva:alarm] struct2.i:82: Warning:
+79,80d78
+< accessing out of bounds index. assert (int)(i + j) < 2;
+< [eva:alarm] struct2.i:185: Warning:
+98c96
+< [scope:rm_asserts] removing 2 assertion(s)
+---
+> [scope:rm_asserts] removing 1 assertion(s)
+136,137c134
+< tab4[0] ∈ {0; 2}
+< [1] ∈ {0}
+---
+> tab4[0..1] ∈ {0}
+140c137,138
+< tab6[0..1] ∈ {0; 2}
+---
+> tab6[0] ∈ {0}
+> [1] ∈ {2}
+211c209
+< [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0..1];
+---
+> [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0];
diff --git a/tests/value/oracle_symblocs/symbolic_locs.res.oracle b/tests/value/oracle_symblocs/symbolic_locs.res.oracle
new file mode 100644
index 00000000000..49bbe86eb13
--- /dev/null
+++ b/tests/value/oracle_symblocs/symbolic_locs.res.oracle
@@ -0,0 +1,71 @@
+19a20,25
+> # Symbolic locations domain:
+> V: {[ t[i] -> {4} ]}
+> Z: {[ t[i] -> t[0..8]; i ]}
+> I: {[ t -> {t[i]}
+> i -> {t[i]} ]}
+> S: {[ i -> {t[i]} ]}
+30a37,41
+> # Symbolic locations domain:
+> V: {[ ]}
+> Z: {[ ]}
+> I: {[ ]}
+> S: {[ ]}
+46a58,63
+> # Symbolic locations domain:
+> V: {[ t[i] -> {4} ]}
+> Z: {[ t[i] -> t[0..8]; i ]}
+> I: {[ t -> {t[i]}
+> i -> {t[i]} ]}
+> S: {[ i -> {t[i]} ]}
+57a75,79
+> # Symbolic locations domain:
+> V: {[ ]}
+> Z: {[ ]}
+> I: {[ ]}
+> S: {[ ]}
+76a99,105
+> # Symbolic locations domain:
+> V: {[ t[i] -> {{ &x }} ]}
+> Z: {[ t[i] -> t[0..8]; i ]}
+> I: {[ t -> {t[i]}
+> i -> {t[i]} ]}
+> S: {[ i -> {t[i]}
+> x -> {t[i]} ]}
+89a119,123
+> # Symbolic locations domain:
+> V: {[ ]}
+> Z: {[ ]}
+> I: {[ ]}
+> S: {[ ]}
+104a139,144
+> # Symbolic locations domain:
+> V: {[ t[i] -> {1} ]}
+> Z: {[ t[i] -> t[0..8]; i ]}
+> I: {[ t -> {t[i]}
+> i -> {t[i]} ]}
+> S: {[ i -> {t[i]} ]}
+113a154,158
+> # Symbolic locations domain:
+> V: {[ ]}
+> Z: {[ ]}
+> I: {[ ]}
+> S: {[ ]}
+128a174,178
+> # Symbolic locations domain:
+> V: {[ ]}
+> Z: {[ ]}
+> I: {[ ]}
+> S: {[ ]}
+135,137c185
+< [eva:alarm] symbolic_locs.i:111: Warning:
+< signed overflow. assert *p + 1 ≤ 2147483647;
+< [eva] symbolic_locs.i:113: Frama_C_show_each: [0..2147483647]
+---
+> [eva] symbolic_locs.i:113: Frama_C_show_each: [10001..2147483647]
+146a195,199
+> # Symbolic locations domain:
+> V: {[ ]}
+> Z: {[ ]}
+> I: {[ ]}
+> S: {[ ]}
diff --git a/tests/value/oracle_symblocs/test.0.res.oracle b/tests/value/oracle_symblocs/test.0.res.oracle
new file mode 100644
index 00000000000..976b889d097
--- /dev/null
+++ b/tests/value/oracle_symblocs/test.0.res.oracle
@@ -0,0 +1,4 @@
+30c30
+< tmp ∈ [--..--] or UNINITIALIZED
+---
+> tmp ∈ [-2147483647..2147483647] or UNINITIALIZED
--
GitLab