From 86e4c302a7324e6d54434d63a83155cb9f1f3089 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Mon, 16 Sep 2019 16:18:00 +0200
Subject: [PATCH] [Dive] Add some tests
---
.../dive/tests/dive/callstack_strategy.i | 31 ++++++++++++
.../tests/dive/oracle/callstack_strategy.dot | 42 +++++++++++++++++
.../dive/oracle/callstack_strategy.res.oracle | 20 ++++++++
.../dive/tests/dive/oracle/per_callstack.dot | 47 +++++++++++++++++++
.../dive/oracle/per_callstack.res.oracle | 22 +++++++++
src/plugins/dive/tests/dive/per_callstack.i | 18 +++++++
6 files changed, 180 insertions(+)
create mode 100644 src/plugins/dive/tests/dive/callstack_strategy.i
create mode 100644 src/plugins/dive/tests/dive/oracle/callstack_strategy.dot
create mode 100644 src/plugins/dive/tests/dive/oracle/callstack_strategy.res.oracle
create mode 100644 src/plugins/dive/tests/dive/oracle/per_callstack.dot
create mode 100644 src/plugins/dive/tests/dive/oracle/per_callstack.res.oracle
create mode 100644 src/plugins/dive/tests/dive/per_callstack.i
diff --git a/src/plugins/dive/tests/dive/callstack_strategy.i b/src/plugins/dive/tests/dive/callstack_strategy.i
new file mode 100644
index 00000000000..72d1f5a832c
--- /dev/null
+++ b/src/plugins/dive/tests/dive/callstack_strategy.i
@@ -0,0 +1,31 @@
+/* run.config
+STDOPT: +"-dive-from g::r -dive-depth-limit 20"
+*/
+
+float f(float z) {
+ return z;
+}
+
+float g(float y) {
+ float z = f(y);
+ float r = y + z;
+ return r;
+}
+
+float h(float x) {
+ float y = f(x);
+ float r = g(y);
+ return r;
+}
+
+float i(float x) {
+ return g(x);
+}
+
+
+void main(float a)
+{
+ h(a);
+ i(a);
+}
+
diff --git a/src/plugins/dive/tests/dive/oracle/callstack_strategy.dot b/src/plugins/dive/tests/dive/oracle/callstack_strategy.dot
new file mode 100644
index 00000000000..0712d3f1771
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/callstack_strategy.dot
@@ -0,0 +1,42 @@
+digraph G {
+ cp0 [label=<r>, shape=box, ];
+ cp1 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp3 [label=<z>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp5 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp7 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp9 [label=<z>, shape=box, ];
+ cp11 [label=<a>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp13 [label=<z>, shape=box, ];
+ cp16 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+
+ subgraph cluster_cs_1 { label=<g>; cp3;cp1;cp0;
+ subgraph cluster_cs_4 { label=<f>; cp9;
+ };
+ };
+ subgraph cluster_cs_2 { label=<i>; cp5;
+ };
+ subgraph cluster_cs_3 { label=<h>; cp16;cp7;
+ subgraph cluster_cs_6 { label=<f>; cp13;
+ };
+ };
+ subgraph cluster_cs_5 { label=<main>; cp11;
+ };
+
+ cp1 -> cp0;
+ cp1 -> cp9;
+ cp3 -> cp0;
+ cp5 -> cp1;
+ cp7 -> cp1;
+ cp9 -> cp3;
+ cp11 -> cp5;
+ cp11 -> cp16;
+ cp13 -> cp7;
+ cp16 -> cp13;
+
+ }
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/callstack_strategy.res.oracle b/src/plugins/dive/tests/dive/oracle/callstack_strategy.res.oracle
new file mode 100644
index 00000000000..db657295bfd
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/callstack_strategy.res.oracle
@@ -0,0 +1,20 @@
+[kernel] Parsing tests/dive/callstack_strategy.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:alarm] tests/dive/callstack_strategy.i:11: Warning:
+ non-finite float value. assert \is_finite((float)(y + z));
+[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 5 functions analyzed (out of 5): 100% coverage.
+ In these functions, 12 statements reached (out of 12): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 nan or infinite floating-point value
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+[dive] output to tests/dive/result/callstack_strategy.dot
diff --git a/src/plugins/dive/tests/dive/oracle/per_callstack.dot b/src/plugins/dive/tests/dive/oracle/per_callstack.dot
new file mode 100644
index 00000000000..c9dd70c166a
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/per_callstack.dot
@@ -0,0 +1,47 @@
+digraph G {
+ cp0 [label=<w>, shape=box, ];
+ cp1 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp3 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp5 [label=<z>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp7 [label=<y>, shape=box, ];
+ cp9 [label=<y>, shape=box, ];
+ cp11 [label=<y>, shape=box, ];
+ cp13 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp15 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp17 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp19 [label=<a>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp21 [label=<b>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp23 [label=<c>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+
+ subgraph cluster_cs_1 { label=<main>; cp23;cp21;cp19;cp5;cp3;cp1;cp0;
+ subgraph cluster_cs_2 { label=<f>; cp13;cp7;
+ };
+ subgraph cluster_cs_3 { label=<f>; cp15;cp9;
+ };
+ subgraph cluster_cs_4 { label=<f>; cp17;cp11;
+ };
+ };
+
+ cp1 -> cp0;
+ cp3 -> cp0;
+ cp5 -> cp0;
+ cp7 -> cp1;
+ cp9 -> cp3;
+ cp11 -> cp5;
+ cp13 -> cp7;
+ cp15 -> cp9;
+ cp17 -> cp11;
+ cp19 -> cp13;
+ cp21 -> cp15;
+ cp23 -> cp17;
+
+ }
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/per_callstack.res.oracle b/src/plugins/dive/tests/dive/oracle/per_callstack.res.oracle
new file mode 100644
index 00000000000..b306565b38e
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/per_callstack.res.oracle
@@ -0,0 +1,22 @@
+[kernel] Parsing tests/dive/per_callstack.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:alarm] tests/dive/per_callstack.i:15: Warning:
+ non-finite float value. assert \is_finite((float)(x + y));
+[eva:alarm] tests/dive/per_callstack.i:15: Warning:
+ non-finite float value. assert \is_finite((float)((float)(x + y) + z));
+[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 2): 100% coverage.
+ In these functions, 7 statements reached (out of 7): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 2 alarms generated by the analysis:
+ 2 nan or infinite floating-point values
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+[dive] output to tests/dive/result/per_callstack.dot
diff --git a/src/plugins/dive/tests/dive/per_callstack.i b/src/plugins/dive/tests/dive/per_callstack.i
new file mode 100644
index 00000000000..a264d1a6844
--- /dev/null
+++ b/src/plugins/dive/tests/dive/per_callstack.i
@@ -0,0 +1,18 @@
+/* run.config
+STDOPT: +"-dive-from main::w -dive-depth-limit 20"
+*/
+
+float f(float x) {
+ float y = x + 1;
+ return y;
+}
+
+float main(float a, float b, float c)
+{
+ float x = f(a);
+ float y = f(b);
+ float z = f(c);
+ float w = x + y + z;
+ return w;
+}
+
--
GitLab