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 0000000000000000000000000000000000000000..25cdbcbd6200484db29211b2522b308cd086c023 --- /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 7cb9dc220aa9c4b3ac751b632251ca2cd4edecee..5e6882b7dd9e77aa263eaff689ed424a37117585 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; + } +}