[PPL-devel] [GIT] ppl/ppl(floating_point): Assert that the octagon is not empty when refining, since the analyzer

[Fabio Bossi]

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

Author: Fabio Bossi <bossi at cs.unipr.it>
Date:   Thu Sep 17 17:35:34 2009 +0200

Assert that the octagon is not empty when refining, since the analyzer
should not try to apply filters in an unreachable state.

---

 src/Octagonal_Shape.templates.hh |    3 ++-
 1 files changed, 2 insertions(+), 1 deletions(-)

diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh
index 7710b61..5598b0d 100644
--- a/src/Octagonal_Shape.templates.hh
+++ b/src/Octagonal_Shape.templates.hh
@@ -490,7 +490,8 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality(
                      "Octagonal_Shape<T>::refine_with_linear_form_inequality:"
                      " T not a floating point type.");
 
-  // FIXME: what to do when empty?
+  // We assume that the analyzer will not try to apply an unreachable filter.
+  PPL_ASSERT(!marked_empty());
 
   // Dimension-compatibility checks.
   // The dimensions of `left' and `right' should not be greater than the