From 80677e9617d0c28c65efbb784277d968b9d59ad5 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Wed, 19 Jun 2019 16:42:32 +0200
Subject: [PATCH] [Eva] Update examples
---
.../parametrizing/context-depth.1.log | 11 ++++
.../parametrizing/context-depth.2.log | 11 ++++
.../parametrizing/context-depth.3.log | 11 ++++
.../examples/parametrizing/context-width.log | 11 ++++
.../parametrizing/global-initial-values.log | 11 ++++
doc/value/examples/parametrizing/ilevel.1.log | 14 +++++
doc/value/examples/parametrizing/ilevel.2.log | 14 +++++
doc/value/examples/parametrizing/nor.1.log | 53 +++++++++++--------
doc/value/examples/parametrizing/nor.2.log | 53 +++++++++++--------
.../examples/parametrizing/out-of-bound.log | 13 +++++
.../examples/parametrizing/simple-main.log | 11 ++++
doc/value/examples/parametrizing/slevel.1.log | 11 ++++
doc/value/examples/parametrizing/slevel.2.log | 11 ++++
.../examples/parametrizing/widen-hints.log | 11 ++++
14 files changed, 204 insertions(+), 42 deletions(-)
diff --git a/doc/value/examples/parametrizing/context-depth.1.log b/doc/value/examples/parametrizing/context-depth.1.log
index 3f4497589cb..add271dee91 100644
--- a/doc/value/examples/parametrizing/context-depth.1.log
+++ b/doc/value/examples/parametrizing/context-depth.1.log
@@ -77,3 +77,14 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 1 statements reached (out of 1): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/context-depth.2.log b/doc/value/examples/parametrizing/context-depth.2.log
index aa40ac4e166..872bda66319 100644
--- a/doc/value/examples/parametrizing/context-depth.2.log
+++ b/doc/value/examples/parametrizing/context-depth.2.log
@@ -18,3 +18,14 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 1 statements reached (out of 1): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/context-depth.3.log b/doc/value/examples/parametrizing/context-depth.3.log
index 796a0b6e08f..b907017b295 100644
--- a/doc/value/examples/parametrizing/context-depth.3.log
+++ b/doc/value/examples/parametrizing/context-depth.3.log
@@ -13,3 +13,14 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 1 statements reached (out of 1): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/context-width.log b/doc/value/examples/parametrizing/context-width.log
index 9edcb21f155..c586ab0c3b5 100644
--- a/doc/value/examples/parametrizing/context-width.log
+++ b/doc/value/examples/parametrizing/context-width.log
@@ -18,3 +18,14 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 2 statements reached (out of 2): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/global-initial-values.log b/doc/value/examples/parametrizing/global-initial-values.log
index f8a0ada3b0e..105b797c406 100644
--- a/doc/value/examples/parametrizing/global-initial-values.log
+++ b/doc/value/examples/parametrizing/global-initial-values.log
@@ -11,3 +11,14 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 1 statements reached (out of 1): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/ilevel.1.log b/doc/value/examples/parametrizing/ilevel.1.log
index c24bbec5ea5..de93eb9610e 100644
--- a/doc/value/examples/parametrizing/ilevel.1.log
+++ b/doc/value/examples/parametrizing/ilevel.1.log
@@ -21,3 +21,17 @@
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
__retres ∈ [2..31]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 5 statements reached (out of 5): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 0 unknown 0 invalid 0 total
+ Preconditions 1 valid 0 unknown 0 invalid 1 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/ilevel.2.log b/doc/value/examples/parametrizing/ilevel.2.log
index 49de84286e0..8cef794e55a 100644
--- a/doc/value/examples/parametrizing/ilevel.2.log
+++ b/doc/value/examples/parametrizing/ilevel.2.log
@@ -21,3 +21,17 @@
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
__retres ∈ {2; 3; 5; 7; 11; 13; 17; 19; 23; 27; 29; 31}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 5 statements reached (out of 5): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 0 unknown 0 invalid 0 total
+ Preconditions 1 valid 0 unknown 0 invalid 1 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/nor.1.log b/doc/value/examples/parametrizing/nor.1.log
index d9202d664a9..292dfde5dd4 100644
--- a/doc/value/examples/parametrizing/nor.1.log
+++ b/doc/value/examples/parametrizing/nor.1.log
@@ -5,26 +5,26 @@
[eva:initial-state] Values of globals at initialization
t[0..1999] ∈ {0}
i ∈ {0}
-[eva] Semantic level unrolling superposing up to 100 states
-[eva] Semantic level unrolling superposing up to 200 states
-[eva] Semantic level unrolling superposing up to 300 states
-[eva] Semantic level unrolling superposing up to 400 states
-[eva] Semantic level unrolling superposing up to 500 states
-[eva] Semantic level unrolling superposing up to 600 states
-[eva] Semantic level unrolling superposing up to 700 states
-[eva] Semantic level unrolling superposing up to 800 states
-[eva] Semantic level unrolling superposing up to 900 states
-[eva] Semantic level unrolling superposing up to 1000 states
-[eva] Semantic level unrolling superposing up to 1100 states
-[eva] Semantic level unrolling superposing up to 1200 states
-[eva] Semantic level unrolling superposing up to 1300 states
-[eva] Semantic level unrolling superposing up to 1400 states
-[eva] Semantic level unrolling superposing up to 1500 states
-[eva] Semantic level unrolling superposing up to 1600 states
-[eva] Semantic level unrolling superposing up to 1700 states
-[eva] Semantic level unrolling superposing up to 1800 states
-[eva] Semantic level unrolling superposing up to 1900 states
-[eva] Semantic level unrolling superposing up to 2000 states
+[eva] nor.c:5: Trace partitioning superposing up to 100 states
+[eva] nor.c:5: Trace partitioning superposing up to 200 states
+[eva] nor.c:5: Trace partitioning superposing up to 300 states
+[eva] nor.c:5: Trace partitioning superposing up to 400 states
+[eva] nor.c:5: Trace partitioning superposing up to 500 states
+[eva] nor.c:5: Trace partitioning superposing up to 600 states
+[eva] nor.c:5: Trace partitioning superposing up to 700 states
+[eva] nor.c:5: Trace partitioning superposing up to 800 states
+[eva] nor.c:5: Trace partitioning superposing up to 900 states
+[eva] nor.c:5: Trace partitioning superposing up to 1000 states
+[eva] nor.c:5: Trace partitioning superposing up to 1100 states
+[eva] nor.c:5: Trace partitioning superposing up to 1200 states
+[eva] nor.c:5: Trace partitioning superposing up to 1300 states
+[eva] nor.c:5: Trace partitioning superposing up to 1400 states
+[eva] nor.c:5: Trace partitioning superposing up to 1500 states
+[eva] nor.c:5: Trace partitioning superposing up to 1600 states
+[eva] nor.c:5: Trace partitioning superposing up to 1700 states
+[eva] nor.c:5: Trace partitioning superposing up to 1800 states
+[eva] nor.c:5: Trace partitioning superposing up to 1900 states
+[eva] nor.c:5: Trace partitioning superposing up to 2000 states
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function irrelevant_function:
@@ -4032,5 +4032,16 @@
[1999] ∈ {1999}
i ∈ {2000}
__retres ∈ {143}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 2): 100% coverage.
+ In these functions, 10 statements reached (out of 10): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
-user time: 0.61s
+user time: 7.67s
diff --git a/doc/value/examples/parametrizing/nor.2.log b/doc/value/examples/parametrizing/nor.2.log
index d79d6ad6a29..de472ed593d 100644
--- a/doc/value/examples/parametrizing/nor.2.log
+++ b/doc/value/examples/parametrizing/nor.2.log
@@ -5,26 +5,26 @@
[eva:initial-state] Values of globals at initialization
t[0..1999] ∈ {0}
i ∈ {0}
-[eva] Semantic level unrolling superposing up to 100 states
-[eva] Semantic level unrolling superposing up to 200 states
-[eva] Semantic level unrolling superposing up to 300 states
-[eva] Semantic level unrolling superposing up to 400 states
-[eva] Semantic level unrolling superposing up to 500 states
-[eva] Semantic level unrolling superposing up to 600 states
-[eva] Semantic level unrolling superposing up to 700 states
-[eva] Semantic level unrolling superposing up to 800 states
-[eva] Semantic level unrolling superposing up to 900 states
-[eva] Semantic level unrolling superposing up to 1000 states
-[eva] Semantic level unrolling superposing up to 1100 states
-[eva] Semantic level unrolling superposing up to 1200 states
-[eva] Semantic level unrolling superposing up to 1300 states
-[eva] Semantic level unrolling superposing up to 1400 states
-[eva] Semantic level unrolling superposing up to 1500 states
-[eva] Semantic level unrolling superposing up to 1600 states
-[eva] Semantic level unrolling superposing up to 1700 states
-[eva] Semantic level unrolling superposing up to 1800 states
-[eva] Semantic level unrolling superposing up to 1900 states
-[eva] Semantic level unrolling superposing up to 2000 states
+[eva] nor.c:5: Trace partitioning superposing up to 100 states
+[eva] nor.c:5: Trace partitioning superposing up to 200 states
+[eva] nor.c:5: Trace partitioning superposing up to 300 states
+[eva] nor.c:5: Trace partitioning superposing up to 400 states
+[eva] nor.c:5: Trace partitioning superposing up to 500 states
+[eva] nor.c:5: Trace partitioning superposing up to 600 states
+[eva] nor.c:5: Trace partitioning superposing up to 700 states
+[eva] nor.c:5: Trace partitioning superposing up to 800 states
+[eva] nor.c:5: Trace partitioning superposing up to 900 states
+[eva] nor.c:5: Trace partitioning superposing up to 1000 states
+[eva] nor.c:5: Trace partitioning superposing up to 1100 states
+[eva] nor.c:5: Trace partitioning superposing up to 1200 states
+[eva] nor.c:5: Trace partitioning superposing up to 1300 states
+[eva] nor.c:5: Trace partitioning superposing up to 1400 states
+[eva] nor.c:5: Trace partitioning superposing up to 1500 states
+[eva] nor.c:5: Trace partitioning superposing up to 1600 states
+[eva] nor.c:5: Trace partitioning superposing up to 1700 states
+[eva] nor.c:5: Trace partitioning superposing up to 1800 states
+[eva] nor.c:5: Trace partitioning superposing up to 1900 states
+[eva] nor.c:5: Trace partitioning superposing up to 2000 states
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
@@ -2031,5 +2031,16 @@ Cannot filter: dumping raw memory (including unchanged variables)
[1999] ∈ {1999}
i ∈ {2000}
__retres ∈ {143}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 2): 100% coverage.
+ In these functions, 10 statements reached (out of 10): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
-user time: 0.26s
+user time: 3.11s
diff --git a/doc/value/examples/parametrizing/out-of-bound.log b/doc/value/examples/parametrizing/out-of-bound.log
index 06f21f7998e..365e3edd937 100644
--- a/doc/value/examples/parametrizing/out-of-bound.log
+++ b/doc/value/examples/parametrizing/out-of-bound.log
@@ -11,3 +11,16 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
NON TERMINATING FUNCTION
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 2): 50% coverage.
+ In this function, 1 statements reached (out of 2): 50% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 access out of bounds index
+ 1 of them is a sure alarm (invalid status).
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/simple-main.log b/doc/value/examples/parametrizing/simple-main.log
index d7defe1645a..63b112ec393 100644
--- a/doc/value/examples/parametrizing/simple-main.log
+++ b/doc/value/examples/parametrizing/simple-main.log
@@ -19,3 +19,14 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
__retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 3 statements reached (out of 3): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/slevel.1.log b/doc/value/examples/parametrizing/slevel.1.log
index ca308071d54..7fab16b9dd7 100644
--- a/doc/value/examples/parametrizing/slevel.1.log
+++ b/doc/value/examples/parametrizing/slevel.1.log
@@ -12,3 +12,14 @@
i ∈ {5}
j ∈ {10}
t[0..4][0..9] ∈ {1}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 12 statements reached (out of 12): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/slevel.2.log b/doc/value/examples/parametrizing/slevel.2.log
index 9459da3c993..cc1474f37db 100644
--- a/doc/value/examples/parametrizing/slevel.2.log
+++ b/doc/value/examples/parametrizing/slevel.2.log
@@ -14,3 +14,14 @@
j ∈ {10}
t{[0..1][0..9]; [2][0..5]} ∈ {1}
{[2][6..9]; [3..4][0..9]} ∈ {0; 1}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 12 statements reached (out of 12): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/widen-hints.log b/doc/value/examples/parametrizing/widen-hints.log
index 9e760a40d33..b02525597d9 100644
--- a/doc/value/examples/parametrizing/widen-hints.log
+++ b/doc/value/examples/parametrizing/widen-hints.log
@@ -12,3 +12,14 @@
i ∈ {13}
j ∈ [0..55]
n ∈ {13}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 9 statements reached (out of 9): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
--
GitLab