[Tests] adds symblocs_SUITES = value

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

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

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

tests/value/oracle_symblocs/alias.0.res.oracle

+103,104c103,104
+<   t ∈ {1; 2; 4}
+<   u ∈ {2; 3; 4; 5}
+---
+>   t ∈ {4}
+>   u ∈ {5}
+110c110
+<   t2 ∈ {0; 3; 6}
+---
+>   t2 ∈ {6}

tests/value/oracle_symblocs/alias.4.res.oracle

+80c80
+<   y ∈ {0; 3; 77}
+---
+>   y ∈ {77}

tests/value/oracle_symblocs/alias.5.res.oracle

+167c167
+<   y ∈ {0; 3; 77}
+---
+>   y ∈ {77}

tests/value/oracle_symblocs/alias.6.res.oracle

+86c86
+<   x ∈ {0; 4; 33}
+---
+>   x ∈ {33}

tests/value/oracle_symblocs/bitwise_pointer.res.oracle

+62c62
+<   x ∈ [0..9]
+---
+>   x ∈ {5}
+75c75
+<   x1 ∈ [0..9]
+---
+>   x1 ∈ {5}

tests/value/oracle_symblocs/bitwise_reduction.res.oracle

+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}

tests/value/oracle_symblocs/builtins_split.res.oracle

+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}

tests/value/oracle_symblocs/domains_function.res.oracle

+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}

tests/value/oracle_symblocs/incompatible_states.res.oracle

+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)

tests/value/oracle_symblocs/library.res.oracle

+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));

tests/value/oracle_symblocs/non_natural.res.oracle

+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.

tests/value/oracle_symblocs/offsetmap.0.res.oracle

+40d39
+< [eva] Recording results for g
+42a42
+> [eva] Recording results for g

tests/value/oracle_symblocs/offsetmap.1.res.oracle

+40d39
+< [eva] Recording results for g
+42a42
+> [eva] Recording results for g

tests/value/oracle_symblocs/plevel.res.oracle

+12d11
+< [eva] Recording results for main
+13a13
+> [eva] Recording results for main

tests/value/oracle_symblocs/ptr_relation.0.res.oracle

+23c23
+<   i ∈ {0; 77; 333}
+---
+>   i ∈ {77}

tests/value/oracle_symblocs/redundant_alarms.res.oracle

+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;

tests/value/oracle_symblocs/relations2.res.oracle

+132d131
+< [eva] relations2.i:57: Frama_C_show_each_NO2: