[PPL-devel] [GIT] ppl/ppl(floating_point): Fixed test03.

[Roberto Amadini]

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

Author: Roberto Amadini <r.amadini at virgilio.it>
Date:   Tue Oct  6 01:22:33 2009 +0200

Fixed test03.

---

 tests/Floating_Point_Expression/digitalfilters1.cc |   15 +++++++++------
 1 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc
index 141cdff..5c3a4fd 100644
--- a/tests/Floating_Point_Expression/digitalfilters1.cc
+++ b/tests/Floating_Point_Expression/digitalfilters1.cc
@@ -216,7 +216,6 @@ test02() {
 
 // tests rate limiter using octagons abstract domain
 // and ignoring rounding errors.
-// FIXME: Not pass at the moment,
 bool
 test03() {
   // Input signal.
@@ -282,6 +281,7 @@ test03() {
     oc.upper_bound_assign(oc_begin);
     Constraint_System cs;
     PPL_DIRTY_TEMP_COEFFICIENT(M);
+    PPL_DIRTY_TEMP_COEFFICIENT(N);
     ANALYZER_FP_FORMAT max_analyzed =
     (2 - pow(2,
        -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS)))
@@ -291,10 +291,13 @@ test03() {
       std::numeric_limits<ANALYZER_FP_FORMAT>::max();
     max_analyzer = std::min(max_analyzer, max_analyzed);
     assign_r(M, max_analyzer, ROUND_DOWN);
-    cs.insert(Y <= M);
-    cs.insert(Y >= -M);
-    //Octagonal_Shape<float> oc1(cs);
-    //print_constraints(oc1, "*** oc1 ***");
+    div_2exp_assign_r(N, M, 1, ROUND_DOWN);
+    // FIXME: By inserting the constraints Y <= M and Y >= -M, we obtain
+    // Y + Y <= 2 * M = +inf and -Y - Y <= -2 * M = +inf.
+    // For a more precise analysis, it is better to insert the
+    // constraints Y <= N and Y >= -N, where N = M / 2.
+    cs.insert(Y <= N);
+    cs.insert(Y >= -N);
     oc.limited_BHMZ05_extrapolation_assign(oc_begin, cs);
     Box<FP_Interval> box(oc);
     print_constraints(box, "*** after widening ***");
@@ -638,7 +641,7 @@ test06() {
 BEGIN_MAIN
   DO_TEST(test01);
   DO_TEST(test02);
-  //DO_TEST(test03);
+  DO_TEST(test03);
   DO_TEST(test04);
   //DO_TEST(test05);
   //DO_TEST(test06);