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

Author: Roberto Amadini r.amadini@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