diff --git a/src/plugins/value/engine/trace_partitioning.ml b/src/plugins/value/engine/trace_partitioning.ml index 71cb5fab948d7fd0e823931a7983d50fbb5499aa..2a63927373bb51f90a120cc3eac6e04e7466e887 100644 --- a/src/plugins/value/engine/trace_partitioning.ml +++ b/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 diff --git a/tests/builtins/oracle/alloc_weak.res.oracle b/tests/builtins/oracle/alloc_weak.res.oracle index 14c99ac21dce40ed9e7ac58e24aa5776d23bcb9c..5a584e372684c98e4aa9b566bf7ddcda96c4ca45 100644 --- a/tests/builtins/oracle/alloc_weak.res.oracle +++ b/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. diff --git a/tests/builtins/oracle/allocated.1.res.oracle b/tests/builtins/oracle/allocated.1.res.oracle index 1d1a14a2671438875798c21c4c233aae76eff722..0a5410846375e6424c9544508acbe145bab980e4 100644 --- a/tests/builtins/oracle/allocated.1.res.oracle +++ b/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} diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle index 6976af91e177e1561a61388b9e0d12e64314e244..fffd2495d1d6ab651db22788f76adb4ca2104a70 100644 --- a/tests/builtins/oracle/memcpy.res.oracle +++ b/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 diff --git a/tests/float/oracle/some.0.res.oracle b/tests/float/oracle/some.0.res.oracle index 919ce1d7a0f9da2fd337a9de6c61e08f2693397d..adf1550160eae6b7e5449a33e2e6e585520ee2be 100644 --- a/tests/float/oracle/some.0.res.oracle +++ b/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: diff --git a/tests/libc/oracle/string_c_strchr.res.oracle b/tests/libc/oracle/string_c_strchr.res.oracle index cd933cfd49fed6dc7715135b255f735021193df9..965af4a3862fe7990d7ca5c2fa9ece0a8c3fc0f8 100644 --- a/tests/libc/oracle/string_c_strchr.res.oracle +++ b/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. diff --git a/tests/libc/oracle/string_h.res.oracle b/tests/libc/oracle/string_h.res.oracle index 731e3e522c0941ee99099b17fb0e2ccfe22a7e53..66a8414bd903b0993bdbd8dba5989da6b0294e31 100644 --- a/tests/libc/oracle/string_h.res.oracle +++ b/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 diff --git a/tests/slicing/oracle/if_many_values.res.oracle b/tests/slicing/oracle/if_many_values.res.oracle index b9a574da2ca5015672235bcfc41d788a86eb8d2c..51574c7a555960703c9aed99d4b3a247375189a4 100644 --- a/tests/slicing/oracle/if_many_values.res.oracle +++ b/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; diff --git a/tests/value/oracle/local_slevel.res.oracle b/tests/value/oracle/local_slevel.res.oracle index ecb1201e61c7d2bad6588c6b28a35d3c0bb612e2..5c81a0b88089bac314eae4f6c35d4d239a4d1938 100644 --- a/tests/value/oracle/local_slevel.res.oracle +++ b/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 diff --git a/tests/value/oracle/no_results.res.oracle b/tests/value/oracle/no_results.res.oracle index b1bab125fb03891dc033443817eabe909a5dd537..83759c6e7fe0117d61dcfaac1a19f5f388f46d51 100644 --- a/tests/value/oracle/no_results.res.oracle +++ b/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.