[Dive] Add some tests

src/plugins/dive/tests/dive/callstack_strategy.i

+/* 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);
+}
+

src/plugins/dive/tests/dive/oracle/callstack_strategy.dot

+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

src/plugins/dive/tests/dive/oracle/callstack_strategy.res.oracle

+[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

src/plugins/dive/tests/dive/oracle/per_callstack.dot

+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

src/plugins/dive/tests/dive/oracle/per_callstack.res.oracle

+[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

src/plugins/dive/tests/dive/per_callstack.i

+/* 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;
+}
+