From 6a700dd42e90da34269aaa586bd7dbbafdc8fcc8 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 5 Oct 2021 16:39:12 +0200
Subject: [PATCH] [Eva] Add a test for interprocedural splits

---
 .../partitioning-interproc.2.res.oracle       | 36 +++++++++++++++++++
 tests/value/partitioning-interproc.c          | 23 +++++++++++-
 2 files changed, 58 insertions(+), 1 deletion(-)
 create mode 100644 tests/value/oracle/partitioning-interproc.2.res.oracle

diff --git a/tests/value/oracle/partitioning-interproc.2.res.oracle b/tests/value/oracle/partitioning-interproc.2.res.oracle
new file mode 100644
index 00000000000..25cdbcbd620
--- /dev/null
+++ b/tests/value/oracle/partitioning-interproc.2.res.oracle
@@ -0,0 +1,36 @@
+[kernel] Parsing tests/value/partitioning-interproc.c (with preprocessing)
+[eva] Analyzing a complete application starting at fabs_splits_test
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  
+[eva] computing for function fabs_splits <- fabs_splits_test.
+  Called from tests/value/partitioning-interproc.c:71.
+[eva] Recording results for fabs_splits
+[eva] Done for function fabs_splits
+[eva] Recording results for fabs_splits_test
+[eva] done for function fabs_splits_test
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function fabs_splits:
+  __retres ∈ [0. .. 1.79769313486e+308]
+[eva:final-states] Values at end of function fabs_splits_test:
+  x ∈ [-1. .. 1.]
+[from] Computing for function fabs_splits
+[from] Done for function fabs_splits
+[from] Computing for function fabs_splits_test
+[from] Done for function fabs_splits_test
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function fabs_splits:
+  \result FROM x
+[from] Function fabs_splits_test:
+  NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function fabs_splits:
+    __retres
+[inout] Inputs for function fabs_splits:
+    \nothing
+[inout] Out (internal) for function fabs_splits_test:
+    x; tmp
+[inout] Inputs for function fabs_splits_test:
+    \nothing
diff --git a/tests/value/partitioning-interproc.c b/tests/value/partitioning-interproc.c
index 7cb9dc220aa..5e6882b7dd9 100644
--- a/tests/value/partitioning-interproc.c
+++ b/tests/value/partitioning-interproc.c
@@ -2,8 +2,8 @@
    GCC:
    STDOPT: #"-main cassign_test -eva-partition-history 1 -eva-interprocedural-partitioning-keep-history"
    STDOPT: #"-main fabs_test -eva-partition-history 1 -eva-domains equality -eva-interprocedural-partitioning-keep-history"
+   STDOPT: #"-main fabs_splits_test -eva-partition-history 1 -eva-domains equality -eva-interprocedural-partitioning-keep-splits"
    */
-
 #include "__fc_builtin.h"
 
 int cassign(int *p)
@@ -51,3 +51,24 @@ void fabs_test(double x)
     x = x < 0 ? -1.0 : 1.0;
   }
 }
+
+
+double fabs_splits(double x)
+{
+  //@ split x > 0.0;
+  //@ split x < 0.0;
+  if (x == 0.0) {
+    return 0.0;
+  } else if (x > 0.0) {
+    return x;
+  } else {
+    return -x;
+  } 
+}
+
+void fabs_splits_test(double x)
+{
+  if (fabs_splits(x) > 1.0) {
+    x = x < 0 ? -1.0 : 1.0;
+  }
+}
-- 
GitLab