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

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