Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
80677e96
Commit
80677e96
authored
Jun 19, 2019
by
Valentin Perrelle
Committed by
David Bühler
Jun 21, 2019
Browse files
[Eva] Update examples
parent
0b3353b7
Changes
14
Hide whitespace changes
Inline
Side-by-side
doc/value/examples/parametrizing/context-depth.1.log
View file @
80677e96
...
...
@@ -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.
----------------------------------------------------------------------------
doc/value/examples/parametrizing/context-depth.2.log
View file @
80677e96
...
...
@@ -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.
----------------------------------------------------------------------------
doc/value/examples/parametrizing/context-depth.3.log
View file @
80677e96
...
...
@@ -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.
----------------------------------------------------------------------------
doc/value/examples/parametrizing/context-width.log
View file @
80677e96
...
...
@@ -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.
----------------------------------------------------------------------------
doc/value/examples/parametrizing/global-initial-values.log
View file @
80677e96
...
...
@@ -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.
----------------------------------------------------------------------------
doc/value/examples/parametrizing/ilevel.1.log
View file @
80677e96
...
...
@@ -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.
----------------------------------------------------------------------------
doc/value/examples/parametrizing/ilevel.2.log
View file @
80677e96
...
...
@@ -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.
----------------------------------------------------------------------------
doc/value/examples/parametrizing/nor.1.log
View file @
80677e96
...
...
@@ -5,26 +5,26 @@
[eva:initial-state] Values of globals at initialization
t[0..1999] ∈ {0}
i ∈ {0}
[eva]
Semantic level unroll
ing superposing up to 100 states
[eva]
Semantic level unroll
ing superposing up to 200 states
[eva]
Semantic level unroll
ing superposing up to 300 states
[eva]
Semantic level unroll
ing superposing up to 400 states
[eva]
Semantic level unroll
ing superposing up to 500 states
[eva]
Semantic level unroll
ing superposing up to 600 states
[eva]
Semantic level unroll
ing superposing up to 700 states
[eva]
Semantic level unroll
ing superposing up to 800 states
[eva]
Semantic level unroll
ing superposing up to 900 states
[eva]
Semantic level unroll
ing superposing up to 1000 states
[eva]
Semantic level unroll
ing superposing up to 1100 states
[eva]
Semantic level unroll
ing superposing up to 1200 states
[eva]
Semantic level unroll
ing superposing up to 1300 states
[eva]
Semantic level unroll
ing superposing up to 1400 states
[eva]
Semantic level unroll
ing superposing up to 1500 states
[eva]
Semantic level unroll
ing superposing up to 1600 states
[eva]
Semantic level unroll
ing superposing up to 1700 states
[eva]
Semantic level unroll
ing superposing up to 1800 states
[eva]
Semantic level unroll
ing superposing up to 1900 states
[eva]
Semantic level unroll
ing superposing up to 2000 states
[eva]
nor.c:5: Trace partition
ing superposing up to 100 states
[eva]
nor.c:5: Trace partition
ing superposing up to 200 states
[eva]
nor.c:5: Trace partition
ing superposing up to 300 states
[eva]
nor.c:5: Trace partition
ing superposing up to 400 states
[eva]
nor.c:5: Trace partition
ing superposing up to 500 states
[eva]
nor.c:5: Trace partition
ing superposing up to 600 states
[eva]
nor.c:5: Trace partition
ing superposing up to 700 states
[eva]
nor.c:5: Trace partition
ing superposing up to 800 states
[eva]
nor.c:5: Trace partition
ing superposing up to 900 states
[eva]
nor.c:5: Trace partition
ing superposing up to 1000 states
[eva]
nor.c:5: Trace partition
ing superposing up to 1100 states
[eva]
nor.c:5: Trace partition
ing superposing up to 1200 states
[eva]
nor.c:5: Trace partition
ing superposing up to 1300 states
[eva]
nor.c:5: Trace partition
ing superposing up to 1400 states
[eva]
nor.c:5: Trace partition
ing superposing up to 1500 states
[eva]
nor.c:5: Trace partition
ing superposing up to 1600 states
[eva]
nor.c:5: Trace partition
ing superposing up to 1700 states
[eva]
nor.c:5: Trace partition
ing superposing up to 1800 states
[eva]
nor.c:5: Trace partition
ing superposing up to 1900 states
[eva]
nor.c:5: Trace partition
ing 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
.6
1
s
user time:
7
.6
7
s
doc/value/examples/parametrizing/nor.2.log
View file @
80677e96
...
...
@@ -5,26 +5,26 @@
[eva:initial-state] Values of globals at initialization
t[0..1999] ∈ {0}
i ∈ {0}
[eva]
Semantic level unroll
ing superposing up to 100 states
[eva]
Semantic level unroll
ing superposing up to 200 states
[eva]
Semantic level unroll
ing superposing up to 300 states
[eva]
Semantic level unroll
ing superposing up to 400 states
[eva]
Semantic level unroll
ing superposing up to 500 states
[eva]
Semantic level unroll
ing superposing up to 600 states
[eva]
Semantic level unroll
ing superposing up to 700 states
[eva]
Semantic level unroll
ing superposing up to 800 states
[eva]
Semantic level unroll
ing superposing up to 900 states
[eva]
Semantic level unroll
ing superposing up to 1000 states
[eva]
Semantic level unroll
ing superposing up to 1100 states
[eva]
Semantic level unroll
ing superposing up to 1200 states
[eva]
Semantic level unroll
ing superposing up to 1300 states
[eva]
Semantic level unroll
ing superposing up to 1400 states
[eva]
Semantic level unroll
ing superposing up to 1500 states
[eva]
Semantic level unroll
ing superposing up to 1600 states
[eva]
Semantic level unroll
ing superposing up to 1700 states
[eva]
Semantic level unroll
ing superposing up to 1800 states
[eva]
Semantic level unroll
ing superposing up to 1900 states
[eva]
Semantic level unroll
ing superposing up to 2000 states
[eva]
nor.c:5: Trace partition
ing superposing up to 100 states
[eva]
nor.c:5: Trace partition
ing superposing up to 200 states
[eva]
nor.c:5: Trace partition
ing superposing up to 300 states
[eva]
nor.c:5: Trace partition
ing superposing up to 400 states
[eva]
nor.c:5: Trace partition
ing superposing up to 500 states
[eva]
nor.c:5: Trace partition
ing superposing up to 600 states
[eva]
nor.c:5: Trace partition
ing superposing up to 700 states
[eva]
nor.c:5: Trace partition
ing superposing up to 800 states
[eva]
nor.c:5: Trace partition
ing superposing up to 900 states
[eva]
nor.c:5: Trace partition
ing superposing up to 1000 states
[eva]
nor.c:5: Trace partition
ing superposing up to 1100 states
[eva]
nor.c:5: Trace partition
ing superposing up to 1200 states
[eva]
nor.c:5: Trace partition
ing superposing up to 1300 states
[eva]
nor.c:5: Trace partition
ing superposing up to 1400 states
[eva]
nor.c:5: Trace partition
ing superposing up to 1500 states
[eva]
nor.c:5: Trace partition
ing superposing up to 1600 states
[eva]
nor.c:5: Trace partition
ing superposing up to 1700 states
[eva]
nor.c:5: Trace partition
ing superposing up to 1800 states
[eva]
nor.c:5: Trace partition
ing superposing up to 1900 states
[eva]
nor.c:5: Trace partition
ing 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.26
s
user time:
3.11
s
doc/value/examples/parametrizing/out-of-bound.log
View file @
80677e96
...
...
@@ -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.
----------------------------------------------------------------------------
doc/value/examples/parametrizing/simple-main.log
View file @
80677e96
...
...
@@ -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.
----------------------------------------------------------------------------
doc/value/examples/parametrizing/slevel.1.log
View file @
80677e96
...
...
@@ -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.
----------------------------------------------------------------------------
doc/value/examples/parametrizing/slevel.2.log
View file @
80677e96
...
...
@@ -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.
----------------------------------------------------------------------------
doc/value/examples/parametrizing/widen-hints.log
View file @
80677e96
...
...
@@ -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.
----------------------------------------------------------------------------
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment