diff --git a/tests/value/oracle/statistics.res.oracle b/tests/value/oracle/statistics.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..525a88abd350e4ecb645ac44df7401866a3a8af2 --- /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 0000000000000000000000000000000000000000..adde9af7b2fa751eb5bfa0d968132ecb64e56746 --- /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 0000000000000000000000000000000000000000..df0e4d5911b985c327b96b6ac1813ed26b2ed2d3 --- /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 0000000000000000000000000000000000000000..fbbfc57885eb02c1c80c6f8b78765832fb7c8e8b --- /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 0000000000000000000000000000000000000000..adde9af7b2fa751eb5bfa0d968132ecb64e56746 --- /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 0000000000000000000000000000000000000000..adde9af7b2fa751eb5bfa0d968132ecb64e56746 --- /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 0000000000000000000000000000000000000000..adde9af7b2fa751eb5bfa0d968132ecb64e56746 --- /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 0000000000000000000000000000000000000000..adde9af7b2fa751eb5bfa0d968132ecb64e56746 --- /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 0000000000000000000000000000000000000000..adde9af7b2fa751eb5bfa0d968132ecb64e56746 --- /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 0000000000000000000000000000000000000000..adde9af7b2fa751eb5bfa0d968132ecb64e56746 --- /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 0000000000000000000000000000000000000000..fc219e146b94ebf223c820fb1f783addcafd6ce1 --- /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); +}