diff --git a/tests/ptests_config b/tests/ptests_config index 5349af09d3bfc50a607cce51a3dc748d2776870a..964235ffa75bf1e1046cf6e46da138dac1d1d1aa 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 729a49e20e9cbc76a8415ad9436dbb028281cd32..7173c08e0f38a0660d4b1b9d95b0c89e4aa38097 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 b18fa6cd55f17c0d0dc958ab563caaae361af9d8..908e42246f0bce269a3aad8cbd028769ba333f30 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 0000000000000000000000000000000000000000..c234ab23c2ef7ade7fb11fd8bd401d1a710a0a37 --- /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 0000000000000000000000000000000000000000..a9bf84a72d6f486015f425b702646395d1c6d465 --- /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 0000000000000000000000000000000000000000..42399641f150901d13d034966a44680398eaa6d2 --- /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 0000000000000000000000000000000000000000..a7dfd3031756c0781ca8579ae7e21c2b0a65e1c0 --- /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 0000000000000000000000000000000000000000..f04f7077977a5a61ea7d346c6ff6f90a2e4237e4 --- /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 0000000000000000000000000000000000000000..9906de0d4748a1ac74ab6126880f5d9fc64e8f90 --- /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 0000000000000000000000000000000000000000..9e88f384bc874d83ca09c8d03373778734c95ab2 --- /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 0000000000000000000000000000000000000000..580c761d0eecaeee54cd954f62f21a4547d170b6 --- /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 0000000000000000000000000000000000000000..2b99b73cb02a2230877fe327fcfac83901e2eaf0 --- /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 0000000000000000000000000000000000000000..7414f97802c482fc12a2774225d2ae7d301f5ba4 --- /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 0000000000000000000000000000000000000000..bcfcfe9b73aba3286cdfd9e5d2ff8b18f89d0439 --- /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 0000000000000000000000000000000000000000..6bebb89e738e4c6703b3d8b869f9d852e34a9e44 --- /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 0000000000000000000000000000000000000000..6bebb89e738e4c6703b3d8b869f9d852e34a9e44 --- /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 0000000000000000000000000000000000000000..80295e5723f5bf368e511c973dba796ddd937095 --- /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 0000000000000000000000000000000000000000..0ae744ec7d6e6fcde013d15696dcf66e9f1424b5 --- /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 0000000000000000000000000000000000000000..e3d4eaf72715cfbe64452ebfbd72b8b6c5b05246 --- /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 0000000000000000000000000000000000000000..c58e8b748b82010d71f12f9f376e3ff067b60777 --- /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 0000000000000000000000000000000000000000..85c9191577e5226d6f6e6d5ed35cc7ffae07d12d --- /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 0000000000000000000000000000000000000000..49bbe86eb13a9a1e51ded1a3c2abcd78acea01c1 --- /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 0000000000000000000000000000000000000000..976b889d09710563bb3635d7a4ea4264cb506dd3 --- /dev/null +++ b/tests/value/oracle_symblocs/test.0.res.oracle @@ -0,0 +1,4 @@ +30c30 +< tmp ∈ [--..--] or UNINITIALIZED +--- +> tmp ∈ [-2147483647..2147483647] or UNINITIALIZED