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

Author: Fabio Bossi bossi@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;