From 6cfa0e9e528f7fb3e5e0d06a93c22b0a037ebe08 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 15 Apr 2019 14:26:54 +0200
Subject: [PATCH] [Eva] Changes "semantic level unrolling" into "trace
partitioning" in a feedback.
---
.../value/engine/trace_partitioning.ml | 2 +-
tests/builtins/oracle/alloc_weak.res.oracle | 16 ++---
tests/builtins/oracle/allocated.1.res.oracle | 8 +--
tests/builtins/oracle/memcpy.res.oracle | 2 +-
tests/float/oracle/some.0.res.oracle | 15 ++---
tests/libc/oracle/string_c_strchr.res.oracle | 10 ++--
tests/libc/oracle/string_h.res.oracle | 3 +-
.../slicing/oracle/if_many_values.res.oracle | 2 +-
tests/value/oracle/local_slevel.res.oracle | 8 +--
tests/value/oracle/no_results.res.oracle | 60 +++++++++----------
10 files changed, 59 insertions(+), 67 deletions(-)
diff --git a/src/plugins/value/engine/trace_partitioning.ml b/src/plugins/value/engine/trace_partitioning.ml
index 71cb5fab948..2a63927373b 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 14c99ac21dc..5a584e37268 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 1d1a14a2671..0a541084637 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 6976af91e17..fffd2495d1d 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 919ce1d7a0f..adf1550160e 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 cd933cfd49f..965af4a3862 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 731e3e522c0..66a8414bd90 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 b9a574da2ca..51574c7a555 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 ecb1201e61c..5c81a0b8808 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 b1bab125fb0..83759c6e7fe 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.
--
GitLab