[Eva] Changes "semantic level unrolling" into "trace partitioning" in a feedback.

src/plugins/value/engine/trace_partitioning.ml

@@ -221,7 +221,7 @@ struct
       then
         let rounded = x / slevel_display_step * slevel_display_step in
         Value_parameters.feedback ~once:true ~current:true
-          "Semantic level unrolling superposing up to %d states"
+          "Trace partitioning superposing up to %d states"
           rounded;
         max_displayed := rounded
 

tests/builtins/oracle/alloc_weak.res.oracle

@@ -42,21 +42,21 @@
 [eva] tests/builtins/alloc_weak.c:37: Call to builtin malloc
 [eva] tests/builtins/alloc_weak.c:37: allocating variable __malloc_main2_l37
 [eva] tests/builtins/alloc_weak.c:40: 
-  Semantic level unrolling superposing up to 100 states
+  Trace partitioning superposing up to 100 states
 [eva] tests/builtins/alloc_weak.c:40: 
-  Semantic level unrolling superposing up to 200 states
+  Trace partitioning superposing up to 200 states
 [eva] tests/builtins/alloc_weak.c:40: 
-  Semantic level unrolling superposing up to 300 states
+  Trace partitioning superposing up to 300 states
 [eva] tests/builtins/alloc_weak.c:40: 
-  Semantic level unrolling superposing up to 400 states
+  Trace partitioning superposing up to 400 states
 [eva] tests/builtins/alloc_weak.c:40: 
-  Semantic level unrolling superposing up to 500 states
+  Trace partitioning superposing up to 500 states
 [eva] tests/builtins/alloc_weak.c:40: 
-  Semantic level unrolling superposing up to 600 states
+  Trace partitioning superposing up to 600 states
 [eva] tests/builtins/alloc_weak.c:40: 
-  Semantic level unrolling superposing up to 700 states
+  Trace partitioning superposing up to 700 states
 [eva] tests/builtins/alloc_weak.c:40: 
-  Semantic level unrolling superposing up to 800 states
+  Trace partitioning superposing up to 800 states
 [eva] Recording results for main2
 [eva] Done for function main2
 [eva] computing for function main3 <- main.

tests/builtins/oracle/allocated.1.res.oracle

@@ -322,13 +322,13 @@
   Call to builtin Frama_C_malloc_fresh for function malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_30
 [eva] tests/builtins/allocated.c:84: 
-  Semantic level unrolling superposing up to 100 states
+  Trace partitioning superposing up to 100 states
 [eva] tests/builtins/allocated.c:84: 
-  Semantic level unrolling superposing up to 200 states
+  Trace partitioning superposing up to 200 states
 [eva] tests/builtins/allocated.c:84: 
-  Semantic level unrolling superposing up to 300 states
+  Trace partitioning superposing up to 300 states
 [eva] tests/builtins/allocated.c:84: 
-  Semantic level unrolling superposing up to 400 states
+  Trace partitioning superposing up to 400 states
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
   strong free on bases: {__malloc_main_l82_30}

tests/builtins/oracle/memcpy.res.oracle

@@ -79,7 +79,7 @@
 [eva] computing for function init <- main <- main_all.
   Called from tests/builtins/memcpy.c:65.
 [eva] tests/builtins/memcpy.c:20: 
-  Semantic level unrolling superposing up to 100 states
+  Trace partitioning superposing up to 100 states
 [eva] Recording results for init
 [from] Computing for function init
 [from] Done for function init

tests/float/oracle/some.0.res.oracle

@@ -6,16 +6,11 @@
   t[0] ∈ {1.0000000000000000}
    [1..54] ∈ {0}
   y ∈ {1.0000000000000000*2^-1}
-[eva] tests/float/some.c:11: 
-  Semantic level unrolling superposing up to 10 states
-[eva] tests/float/some.c:11: 
-  Semantic level unrolling superposing up to 20 states
-[eva] tests/float/some.c:11: 
-  Semantic level unrolling superposing up to 30 states
-[eva] tests/float/some.c:11: 
-  Semantic level unrolling superposing up to 40 states
-[eva] tests/float/some.c:11: 
-  Semantic level unrolling superposing up to 50 states
+[eva] tests/float/some.c:11: Trace partitioning superposing up to 10 states
+[eva] tests/float/some.c:11: Trace partitioning superposing up to 20 states
+[eva] tests/float/some.c:11: Trace partitioning superposing up to 30 states
+[eva] tests/float/some.c:11: Trace partitioning superposing up to 40 states
+[eva] tests/float/some.c:11: Trace partitioning superposing up to 50 states
 [eva] tests/float/some.c:16: 
   Frama_C_dump_each:
   # Cvalue domain:

tests/libc/oracle/string_c_strchr.res.oracle

@@ -5,9 +5,9 @@
 [eva:initial-state] Values of globals at initialization
   
 [eva] tests/libc/string_c_strchr.c:57: 
-  Semantic level unrolling superposing up to 100 states
+  Trace partitioning superposing up to 100 states
 [eva] tests/libc/string_c_strchr.c:59: 
-  Semantic level unrolling superposing up to 200 states
+  Trace partitioning superposing up to 200 states
 [eva] computing for function strchr <- main.
   Called from tests/libc/string_c_strchr.c:62.
 [eva] tests/libc/string_c_strchr.c:62: 
@@ -46,8 +46,7 @@
   Called from tests/libc/string_c_strchr.c:67.
 [eva] tests/libc/string_c_strchr.c:67: 
   function strchr: precondition 'valid_string_s' got status valid.
-[eva] share/libc/string.c:229: 
-  Semantic level unrolling superposing up to 100 states
+[eva] share/libc/string.c:229: Trace partitioning superposing up to 100 states
 [eva] Recording results for strchr
 [eva] Done for function strchr
 [eva] computing for function strchr <- main.
@@ -172,8 +171,7 @@
   Called from tests/libc/string_c_strchr.c:87.
 [eva] tests/libc/string_c_strchr.c:87: 
   function strchr: precondition 'valid_string_s' got status valid.
-[eva] share/libc/string.c:229: 
-  Semantic level unrolling superposing up to 200 states
+[eva] share/libc/string.c:229: Trace partitioning superposing up to 200 states
 [eva] Recording results for strchr
 [eva] Done for function strchr
 [eva] computing for function strchr <- main.

tests/libc/oracle/string_h.res.oracle

@@ -59,8 +59,7 @@
 [eva] Done for function test_strstr
 [eva] computing for function test_strncat <- main.
   Called from tests/libc/string_h.c:115.
-[eva] tests/libc/string_h.c:34: 
-  Semantic level unrolling superposing up to 100 states
+[eva] tests/libc/string_h.c:34: Trace partitioning superposing up to 100 states
 [eva] computing for function strncat <- test_strncat <- main.
   Called from tests/libc/string_h.c:36.
 [eva] using specification for function strncat

tests/slicing/oracle/if_many_values.res.oracle

@@ -6,7 +6,7 @@
 [eva:initial-state] Values of globals at initialization
   r ∈ {1}
 [eva] tests/slicing/if_many_values.i:8: 
-  Semantic level unrolling superposing up to 100 states
+  Trace partitioning superposing up to 100 states
 [eva] tests/slicing/if_many_values.i:8: starting to merge loop iterations
 [eva:alarm] tests/slicing/if_many_values.i:11: Warning: 
   signed overflow. assert r + 1 ≤ 2147483647;

tests/value/oracle/local_slevel.res.oracle

@@ -89,7 +89,7 @@
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {48}
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {49}
 [eva] tests/value/local_slevel.i:43: 
-  Semantic level unrolling superposing up to 100 states
+  Trace partitioning superposing up to 100 states
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {50}
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {51}
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {52}
@@ -141,7 +141,7 @@
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {98}
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {99}
 [eva] tests/value/local_slevel.i:43: 
-  Semantic level unrolling superposing up to 200 states
+  Trace partitioning superposing up to 200 states
 [eva] Recording results for main2
 [eva] Done for function main2
 [eva] Recording results for main
@@ -469,7 +469,7 @@ void main(void)
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {48}
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {49}
 [eva] tests/value/local_slevel.i:43: 
-  Semantic level unrolling superposing up to 100 states
+  Trace partitioning superposing up to 100 states
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {50}
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {51}
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {52}
@@ -521,7 +521,7 @@ void main(void)
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {98}
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {99}
 [eva] tests/value/local_slevel.i:43: 
-  Semantic level unrolling superposing up to 200 states
+  Trace partitioning superposing up to 200 states
 [eva] Recording results for main2
 [eva] Done for function main2
 [eva] Recording results for main

tests/value/oracle/no_results.res.oracle

@@ -7,65 +7,65 @@
 [eva] computing for function init <- main.
   Called from tests/value/no_results.c:19.
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 100 states
+  Trace partitioning superposing up to 100 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 200 states
+  Trace partitioning superposing up to 200 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 300 states
+  Trace partitioning superposing up to 300 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 400 states
+  Trace partitioning superposing up to 400 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 500 states
+  Trace partitioning superposing up to 500 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 600 states
+  Trace partitioning superposing up to 600 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 700 states
+  Trace partitioning superposing up to 700 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 800 states
+  Trace partitioning superposing up to 800 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 900 states
+  Trace partitioning superposing up to 900 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 1000 states
+  Trace partitioning superposing up to 1000 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 1100 states
+  Trace partitioning superposing up to 1100 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 1200 states
+  Trace partitioning superposing up to 1200 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 1300 states
+  Trace partitioning superposing up to 1300 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 1400 states
+  Trace partitioning superposing up to 1400 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 1500 states
+  Trace partitioning superposing up to 1500 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 1600 states
+  Trace partitioning superposing up to 1600 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 1700 states
+  Trace partitioning superposing up to 1700 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 1800 states
+  Trace partitioning superposing up to 1800 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 1900 states
+  Trace partitioning superposing up to 1900 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 2000 states
+  Trace partitioning superposing up to 2000 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 2100 states
+  Trace partitioning superposing up to 2100 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 2200 states
+  Trace partitioning superposing up to 2200 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 2300 states
+  Trace partitioning superposing up to 2300 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 2400 states
+  Trace partitioning superposing up to 2400 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 2500 states
+  Trace partitioning superposing up to 2500 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 2600 states
+  Trace partitioning superposing up to 2600 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 2700 states
+  Trace partitioning superposing up to 2700 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 2800 states
+  Trace partitioning superposing up to 2800 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 2900 states
+  Trace partitioning superposing up to 2900 states
 [eva] tests/value/no_results.c:10: 
-  Semantic level unrolling superposing up to 3000 states
+  Trace partitioning superposing up to 3000 states
 [eva] Recording results for init
 [eva] Done for function init
 [eva] computing for function f <- main.