From 8db1e8cfdf42569bae3530c1431275113d495d78 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 7 Apr 2023 17:02:48 +0200
Subject: [PATCH] [Eva] statistics: add a test
---
tests/value/oracle/statistics.res.oracle | 76 +++++++++++++++++++
tests/value/oracle/statistics.stats | 7 ++
.../value/oracle_apron/statistics.res.oracle | 17 +++++
tests/value/oracle_apron/statistics.stats | 6 ++
tests/value/oracle_bitwise/statistics.stats | 7 ++
tests/value/oracle_equality/statistics.stats | 7 ++
tests/value/oracle_gauges/statistics.stats | 7 ++
tests/value/oracle_multidim/statistics.stats | 7 ++
tests/value/oracle_octagon/statistics.stats | 7 ++
tests/value/oracle_symblocs/statistics.stats | 7 ++
tests/value/statistics.i | 17 +++++
11 files changed, 165 insertions(+)
create mode 100644 tests/value/oracle/statistics.res.oracle
create mode 100644 tests/value/oracle/statistics.stats
create mode 100644 tests/value/oracle_apron/statistics.res.oracle
create mode 100644 tests/value/oracle_apron/statistics.stats
create mode 100644 tests/value/oracle_bitwise/statistics.stats
create mode 100644 tests/value/oracle_equality/statistics.stats
create mode 100644 tests/value/oracle_gauges/statistics.stats
create mode 100644 tests/value/oracle_multidim/statistics.stats
create mode 100644 tests/value/oracle_octagon/statistics.stats
create mode 100644 tests/value/oracle_symblocs/statistics.stats
create mode 100644 tests/value/statistics.i
diff --git a/tests/value/oracle/statistics.res.oracle b/tests/value/oracle/statistics.res.oracle
new file mode 100644
index 00000000000..525a88abd35
--- /dev/null
+++ b/tests/value/oracle/statistics.res.oracle
@@ -0,0 +1,76 @@
+[kernel] Parsing statistics.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] computing for function f <- main.
+ Called from statistics.i:15.
+[eva] computing for function g <- f <- main.
+ Called from statistics.i:10.
+[eva] Recording results for g
+[eva] Done for function g
+[eva] statistics.i:9: starting to merge loop iterations
+[eva] computing for function g <- f <- main.
+ Called from statistics.i:10.
+[eva] Recording results for g
+[eva] Done for function g
+[eva] computing for function g <- f <- main.
+ Called from statistics.i:10.
+[eva] Recording results for g
+[eva] Done for function g
+[eva] computing for function g <- f <- main.
+ Called from statistics.i:10.
+[eva] Recording results for g
+[eva] Done for function g
+[eva] Recording results for f
+[eva] Done for function f
+[eva:alarm] statistics.i:16: Warning:
+ signed overflow. assert -2147483648 ≤ n - 1;
+[eva] computing for function f <- main.
+ Called from statistics.i:16.
+[eva] statistics.i:10: Reusing old results for call to g
+[eva] statistics.i:10: Reusing old results for call to g
+[eva] statistics.i:10: Reusing old results for call to g
+[eva] computing for function g <- f <- main.
+ Called from statistics.i:10.
+[eva] Recording results for g
+[eva] Done for function g
+[eva] Recording results for f
+[eva] Done for function f
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function g:
+
+[eva:final-states] Values at end of function f:
+ i ∈ [0..2147483647]
+[eva:final-states] Values at end of function main:
+ __retres ∈ {0}
+[from] Computing for function g
+[from] Done for function g
+[from] Computing for function f
+[from] Done for function f
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function g:
+ NO EFFECTS
+[from] Function f:
+ NO EFFECTS
+[from] Function main:
+ \result FROM \nothing
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function g:
+ \nothing
+[inout] Inputs for function g:
+ \nothing
+[inout] Out (internal) for function f:
+ i
+[inout] Inputs for function f:
+ \nothing
+[inout] Out (internal) for function main:
+ __retres
+[inout] Inputs for function main:
+ \nothing
diff --git a/tests/value/oracle/statistics.stats b/tests/value/oracle/statistics.stats
new file mode 100644
index 00000000000..adde9af7b2f
--- /dev/null
+++ b/tests/value/oracle/statistics.stats
@@ -0,0 +1,7 @@
+memexec-hits:g 3
+memexec-misses:g 5
+memexec-misses:f 2
+memexec-misses:main 1
+partitioning-index-misses 57
+max-widenings:statistics.i:9 1
+iterations:statistics.i:9 8
diff --git a/tests/value/oracle_apron/statistics.res.oracle b/tests/value/oracle_apron/statistics.res.oracle
new file mode 100644
index 00000000000..df0e4d5911b
--- /dev/null
+++ b/tests/value/oracle_apron/statistics.res.oracle
@@ -0,0 +1,17 @@
+32,34c32,43
+< [eva] statistics.i:10: Reusing old results for call to g
+< [eva] statistics.i:10: Reusing old results for call to g
+< [eva] statistics.i:10: Reusing old results for call to g
+---
+> [eva] computing for function g <- f <- main.
+> Called from statistics.i:10.
+> [eva] Recording results for g
+> [eva] Done for function g
+> [eva] computing for function g <- f <- main.
+> Called from statistics.i:10.
+> [eva] Recording results for g
+> [eva] Done for function g
+> [eva] computing for function g <- f <- main.
+> Called from statistics.i:10.
+> [eva] Recording results for g
+> [eva] Done for function g
diff --git a/tests/value/oracle_apron/statistics.stats b/tests/value/oracle_apron/statistics.stats
new file mode 100644
index 00000000000..fbbfc57885e
--- /dev/null
+++ b/tests/value/oracle_apron/statistics.stats
@@ -0,0 +1,6 @@
+memexec-misses:g 8
+memexec-misses:f 2
+memexec-misses:main 1
+partitioning-index-misses 60
+max-widenings:statistics.i:9 1
+iterations:statistics.i:9 8
diff --git a/tests/value/oracle_bitwise/statistics.stats b/tests/value/oracle_bitwise/statistics.stats
new file mode 100644
index 00000000000..adde9af7b2f
--- /dev/null
+++ b/tests/value/oracle_bitwise/statistics.stats
@@ -0,0 +1,7 @@
+memexec-hits:g 3
+memexec-misses:g 5
+memexec-misses:f 2
+memexec-misses:main 1
+partitioning-index-misses 57
+max-widenings:statistics.i:9 1
+iterations:statistics.i:9 8
diff --git a/tests/value/oracle_equality/statistics.stats b/tests/value/oracle_equality/statistics.stats
new file mode 100644
index 00000000000..adde9af7b2f
--- /dev/null
+++ b/tests/value/oracle_equality/statistics.stats
@@ -0,0 +1,7 @@
+memexec-hits:g 3
+memexec-misses:g 5
+memexec-misses:f 2
+memexec-misses:main 1
+partitioning-index-misses 57
+max-widenings:statistics.i:9 1
+iterations:statistics.i:9 8
diff --git a/tests/value/oracle_gauges/statistics.stats b/tests/value/oracle_gauges/statistics.stats
new file mode 100644
index 00000000000..adde9af7b2f
--- /dev/null
+++ b/tests/value/oracle_gauges/statistics.stats
@@ -0,0 +1,7 @@
+memexec-hits:g 3
+memexec-misses:g 5
+memexec-misses:f 2
+memexec-misses:main 1
+partitioning-index-misses 57
+max-widenings:statistics.i:9 1
+iterations:statistics.i:9 8
diff --git a/tests/value/oracle_multidim/statistics.stats b/tests/value/oracle_multidim/statistics.stats
new file mode 100644
index 00000000000..adde9af7b2f
--- /dev/null
+++ b/tests/value/oracle_multidim/statistics.stats
@@ -0,0 +1,7 @@
+memexec-hits:g 3
+memexec-misses:g 5
+memexec-misses:f 2
+memexec-misses:main 1
+partitioning-index-misses 57
+max-widenings:statistics.i:9 1
+iterations:statistics.i:9 8
diff --git a/tests/value/oracle_octagon/statistics.stats b/tests/value/oracle_octagon/statistics.stats
new file mode 100644
index 00000000000..adde9af7b2f
--- /dev/null
+++ b/tests/value/oracle_octagon/statistics.stats
@@ -0,0 +1,7 @@
+memexec-hits:g 3
+memexec-misses:g 5
+memexec-misses:f 2
+memexec-misses:main 1
+partitioning-index-misses 57
+max-widenings:statistics.i:9 1
+iterations:statistics.i:9 8
diff --git a/tests/value/oracle_symblocs/statistics.stats b/tests/value/oracle_symblocs/statistics.stats
new file mode 100644
index 00000000000..adde9af7b2f
--- /dev/null
+++ b/tests/value/oracle_symblocs/statistics.stats
@@ -0,0 +1,7 @@
+memexec-hits:g 3
+memexec-misses:g 5
+memexec-misses:f 2
+memexec-misses:main 1
+partitioning-index-misses 57
+max-widenings:statistics.i:9 1
+iterations:statistics.i:9 8
diff --git a/tests/value/statistics.i b/tests/value/statistics.i
new file mode 100644
index 00000000000..fc219e146b9
--- /dev/null
+++ b/tests/value/statistics.i
@@ -0,0 +1,17 @@
+/* run.config*
+ LOG: @PTEST_NAME@.stats
+ STDOPT: +" -eva-statistics-file ./@PTEST_NAME@.stats"
+*/
+
+void g(int i) {}
+
+void f(int n) {
+ for (int i = 0 ; i < n ; i++) {
+ g(i);
+ }
+}
+
+int main(int n) {
+ f(n);
+ f(n-1);
+}
--
GitLab