[PPL-devel] [GIT] ppl/ppl(floating_point): Added test for Octagonal_Shape<T>:: refine_fp_interval_abstract_store.

[Roberto Amadini]

Module: ppl/ppl
Branch: floating_point
Commit: 4a811294d3accd1cf5fbcc0470e8e70905c076dd
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4a811294d3accd1cf5fbcc0470e8e70905c076dd

Author: Roberto Amadini <r.amadini at virgilio.it>
Date:   Fri Sep 18 12:32:47 2009 +0200

Added test for Octagonal_Shape<T>::refine_fp_interval_abstract_store.

---

 .../floatingpointexpr1.cc                          |    8 ++--
 tests/Floating_Point_Expression/refinelf1.cc       |   47 ++++++++++++++++++++
 2 files changed, 51 insertions(+), 4 deletions(-)

diff --git a/tests/Floating_Point_Expression/floatingpointexpr1.cc b/tests/Floating_Point_Expression/floatingpointexpr1.cc
index 1553458..624f00f 100644
--- a/tests/Floating_Point_Expression/floatingpointexpr1.cc
+++ b/tests/Floating_Point_Expression/floatingpointexpr1.cc
@@ -60,16 +60,16 @@ typedef Opposite_Floating_Point_Expression<db_r_oc, IEEE754_Single> opp_fpeds;
 typedef Opposite_Floating_Point_Expression<db_r_oc, IEEE754_Double> opp_fpedd;
 
 typedef Floating_Point_Expression<fl_r_oc, IEEE754_Single>::FP_Interval_Abstract_Store sstr;
-typedef Constant_Floating_Point_Expression<db_r_oc, IEEE754_Single>::FP_Interval_Abstract_Store dstr;
+typedef Floating_Point_Expression<db_r_oc, IEEE754_Single>::FP_Interval_Abstract_Store dstr;
 
 typedef Floating_Point_Expression<fl_r_oc, IEEE754_Single>::FP_Linear_Form_Abstract_Store lsstr;
-typedef Constant_Floating_Point_Expression<db_r_oc, IEEE754_Single>::FP_Linear_Form_Abstract_Store ldstr;
+typedef Floating_Point_Expression<db_r_oc, IEEE754_Single>::FP_Linear_Form_Abstract_Store ldstr;
 
 typedef Floating_Point_Expression<fl_r_oc, IEEE754_Double>::FP_Interval_Abstract_Store sdtr;
-typedef Constant_Floating_Point_Expression<db_r_oc, IEEE754_Double>::FP_Interval_Abstract_Store ddtr;
+typedef Floating_Point_Expression<db_r_oc, IEEE754_Double>::FP_Interval_Abstract_Store ddtr;
 
 typedef Floating_Point_Expression<fl_r_oc, IEEE754_Double>::FP_Linear_Form_Abstract_Store lsdtr;
-typedef Constant_Floating_Point_Expression<db_r_oc, IEEE754_Double>::FP_Linear_Form_Abstract_Store lddtr;
+typedef Floating_Point_Expression<db_r_oc, IEEE754_Double>::FP_Linear_Form_Abstract_Store lddtr;
 
 namespace {
 
diff --git a/tests/Floating_Point_Expression/refinelf1.cc b/tests/Floating_Point_Expression/refinelf1.cc
index 8f25961..5d15285 100644
--- a/tests/Floating_Point_Expression/refinelf1.cc
+++ b/tests/Floating_Point_Expression/refinelf1.cc
@@ -23,6 +23,8 @@ site: http://www.cs.unipr.it/ppl/ . */
 
 #include "ppl_test.hh"
 
+typedef Floating_Point_Expression<db_r_oc, IEEE754_Double>::FP_Interval_Abstract_Store ddtr;
+
 namespace {
 
 // tests trivial cases
@@ -403,6 +405,50 @@ test10() {
   return ok;
 }
 
+// tests Octagonal_Shape<T>::refine_fp_interval_abstract_store
+// FIXME: this test should be parametric according to the floating point
+// format of analyzer and analyzed.
+bool
+test11() {
+  Variable A(0);
+  Variable B(1);
+  ddtr store;
+  db_r_oc tmp(-2.5);
+  tmp.join_assign(3.5);
+  store[0] = tmp;
+  tmp.lower() = -4;
+  tmp.upper() = 4;
+  store[1] = tmp;
+  Octagonal_Shape<double> oc1(2);
+  oc1.add_constraint(A <= 2);
+  oc1.add_constraint(B <= 2);
+  oc1.add_constraint(A >= -3);
+  oc1.add_constraint(2*B >= -3);
+  oc1.refine_fp_interval_abstract_store(store);
+
+  nout << "*** store[0] ***" << endl
+       << store[0] << endl;
+
+  db_r_oc known_result1(-2.5);
+  known_result1.join_assign(2);
+  nout << "*** known_result1 ***" << endl
+       << known_result1 << endl;
+
+  bool ok1 = (store[0] == known_result1);
+
+  nout << "*** store[1] ***" << endl
+       << store[1] << endl;
+
+  db_r_oc known_result2(-1.5);
+  known_result2.join_assign(2);
+  nout << "*** known_result2 ***" << endl
+       << known_result2 << endl;
+
+  bool ok2 = (store[1] == known_result2);
+
+  return ok1 && ok2;
+}
+
 } //namespace
 
 BEGIN_MAIN
@@ -416,4 +462,5 @@ BEGIN_MAIN
   DO_TEST(test08);
   DO_TEST(test09);
   DO_TEST(test10);
+  DO_TEST(test11);
 END_MAIN