[PPL-devel] [GIT] ppl/ppl(floating_point): Added some (and corrected some of the) documentation.

[Fabio Bossi]

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

Author: Fabio Bossi <bossi at cs.unipr.it>
Date:   Mon Sep 21 15:00:49 2009 +0200

Added some (and corrected some of the) documentation.

---

 src/Octagonal_Shape.defs.hh |   18 ++++++++++-----
 src/Polyhedron.defs.hh      |   51 +++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 63 insertions(+), 6 deletions(-)

diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh
index b5a6055..60f7f58 100644
--- a/src/Octagonal_Shape.defs.hh
+++ b/src/Octagonal_Shape.defs.hh
@@ -993,17 +993,19 @@ public:
     the constraint expressed by \p left \f$\leq\f$ \p right.
 
     \param left
-    The linear form on intervals with floating point coefficients that
-    is on the left of the comparison operator. All of its coefficients
+    The linear form on intervals with floating point boundaries that
+    is at the left of the comparison operator. All of its coefficients
     MUST be bounded.
 
     \param right
-    The linear form on intervals with floating point coefficients that
-    is on the right of the comparison operator. All of its coefficients
+    The linear form on intervals with floating point boundaries that
+    is at the right of the comparison operator. All of its coefficients
     MUST be bounded.
 
     \exception std::invalid_argument
     Thrown if \p left (or \p right) is dimension-incompatible with \p *this.
+
+    
   */
   template <typename Interval_Info>
   void refine_with_linear_form_inequality(
@@ -1139,12 +1141,16 @@ public:
     The variable to which the affine expression is assigned.
 
     \param lf
-    The linear form on intervals with floating point coefficients that
-    defines the affine expression. ALL of its coefficients MUST be boundend.
+    The linear form on intervals with floating point boundaries that
+    defines the affine expression(s). ALL of its coefficients MUST be bounded.
 
     \exception std::invalid_argument
     Thrown if \p lf and \p *this are dimension-incompatible or if \p var
     is not a dimension of \p *this.
+
+    This function is used in abstract interpretation to model an assignment
+    of a value that is correctly overapproximated by \p lf to the
+    floating point variable represented by \p var.
   */
   template <typename Interval_Info>
   void affine_image(const Variable& var,
diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh
index 0ef020c..3c3a9d5 100644
--- a/src/Polyhedron.defs.hh
+++ b/src/Polyhedron.defs.hh
@@ -979,6 +979,32 @@ public:
   */
   void refine_with_congruences(const Congruence_System& cgs);
 
+  /*!
+    Refines \p *this with the constraint expressed by \p left \f$\leq\f$
+    \p right.
+
+    \param left
+    The linear form on intervals with floating point boundaries that
+    is on the left of the comparison operator. All of its coefficients
+    MUST be bounded.
+
+    \param right
+    The linear form on intervals with floating point boundaries that
+    is on the right of the comparison operator. All of its coefficients
+    MUST be bounded.
+
+    \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.
+
+    \exception std::invalid_argument
+    Thrown if \p left (or \p right) is dimension-incompatible with \p *this.
+
+    This function is used in abstract interpretation to model a filter
+    that is generated by a comparison of two expressions that are correctly
+    approximated by \p left and \p right respectively.
+  */
   template <typename FP_Format, typename Interval_Info>
   void refine_with_linear_form_inequality(
   const Linear_Form< Interval<FP_Format, Interval_Info> >& left,
@@ -1151,6 +1177,31 @@ public:
 		    Coefficient_traits::const_reference denominator
 		      = Coefficient_one());
 
+  /*!
+    Assigns to \p *this the
+    \ref Single_Update_Affine_Functions "affine image"
+    of \p *this under the function mapping variable \p var into the
+    affine expression(s) specified by \p lf.
+
+    \param var
+    The variable to which the affine expression is assigned.
+
+    \param lf
+    The linear form on intervals with floating point boundaries that
+    defines the affine expression(s). ALL of its coefficients MUST be bounded.
+
+    \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.
+
+    \exception std::invalid_argument
+    Thrown if \p lf and \p *this are dimension-incompatible or if \p var is
+    not a space dimension of \p *this.
+
+    This function is used in abstract interpretation to model an assignment
+    of a value that is correctly overapproximated by \p lf to the
+    floating point variable represented by \p var.
+  */
   template <typename FP_Format, typename Interval_Info>
   void affine_image(const Variable& var,
   const Linear_Form<Interval <FP_Format, Interval_Info> >& lf,