[PPL-devel] [GIT] ppl/ppl(floating_point): Always assert that all variables in the abstract store are bounded.

[Fabio Bossi]

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

Author: Fabio Bossi <bossi at cs.unipr.it>
Date:   Thu Sep 24 11:09:02 2009 +0200

Always assert that all variables in the abstract store are bounded.
Corrected the documentation accordingly.

---

 src/Polyhedron.defs.hh      |    7 +++++--
 src/Polyhedron.templates.hh |    3 +++
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh
index f2854b4..41c8ae6 100644
--- a/src/Polyhedron.defs.hh
+++ b/src/Polyhedron.defs.hh
@@ -995,7 +995,7 @@ public:
     \param store
     The interval abstract store in which the test defining the filter is
     performed. All variables that occur in \p left or \p right MUST have
-    an associated value in it.
+    an associated interval in it, and all of these intervals MUST be bounded.
 
     \exception std::invalid_argument
     Thrown if \p left (or \p right) is dimension-incompatible with \p *this.
@@ -1201,7 +1201,8 @@ public:
 
     \param store
     The interval abstract store in which the variable assignment is performed.
-    All variables that occur in \p lf MUST have an associated value in it.
+    All variables that occur in \p lf MUST have an associated interval in it,
+    and all of these intervals MUST be bounded.
 
     \exception std::invalid_argument
     Thrown if \p lf and \p *this are dimension-incompatible or if \p var is
@@ -2647,6 +2648,8 @@ protected:
 
     \param store
     The interval abstract store in which the approximation is performed.
+    All variables that occur in \p lf MUST have an associated interval in it,
+    and all of these intervals MUST be bounded.
 
     \param result
     Used to store the result.
diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh
index 0ef06d2..491bb20 100644
--- a/src/Polyhedron.templates.hh
+++ b/src/Polyhedron.templates.hh
@@ -307,6 +307,7 @@ Polyhedron::refine_with_linear_form_inequality(
                          "Polyhedron::refine_with_linear_form_inequality:"
                          " FP_Format not a floating point type.");
 
+  PPL_ASSERT(store.is_bounded());
   // Dimension compatibility checks.
   // The dimensions of left and right should not be greater than the
   // dimension of *this.
@@ -352,6 +353,7 @@ const Box< Interval<FP_Format, Interval_Info> >& store) {
                          "Polyhedron::affine_image:"
                          " FP_Format not a floating point type.");
 
+  PPL_ASSERT(store.is_bounded());
   // Dimension compatibility checks.
   // The dimension of lf should not be greater than the dimension of *this.
   const dimension_type lf_space_dim = lf.space_dimension();
@@ -398,6 +400,7 @@ Polyhedron::overapproximate_linear_form(
                          " FP_Format not a floating point type.");
 
   PPL_ASSERT(lf_dimension <= store.space_dimension());
+  PPL_ASSERT(store.is_bounded());
 
   typedef Interval<FP_Format, Interval_Info> FP_Interval_Type;
   typedef Linear_Form<FP_Interval_Type> FP_Linear_Form;