Module: ppl/ppl Branch: floating_point Commit: f6b9896513010c79ce173a2226b833477690f5ab URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f6b9896513010...
Author: Fabio Bossi bossi@cs.unipr.it Date: Sat Jul 24 18:45:38 2010 +0200
Added some documentation.
---
src/Float.defs.hh | 16 +++++++++++++ src/Linear_Form.defs.hh | 55 +++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 71 insertions(+), 0 deletions(-)
diff --git a/src/Float.defs.hh b/src/Float.defs.hh index e68c3bd..e484458 100644 --- a/src/Float.defs.hh +++ b/src/Float.defs.hh @@ -360,6 +360,22 @@ public: }; #endif
+/*! \brief + Computes the absolute error of floating point computations. + + \par Template type parameters + + - The class template parameter \p FP_Interval_Type represents the type + of the intervals used in the abstract domain. The interval bounds + should have a floating point type. + + \param analyzed_format The floating point format used by the analyzed + program. + + \return The interval \f$[-\omega; \omega]\f$ where \f$\omega\f$ is the + smallest non-zero positive number in the less precise floating point + format between the analyzer format and the analyzed format. +*/ template <typename FP_Interval_Type> const FP_Interval_Type& compute_absolute_error( Floating_Point_Format analyzed_format); diff --git a/src/Linear_Form.defs.hh b/src/Linear_Form.defs.hh index ccb4e0f..c8c07ae 100644 --- a/src/Linear_Form.defs.hh +++ b/src/Linear_Form.defs.hh @@ -325,11 +325,66 @@ public:
// Floating point analysis related methods.
+ /*! \brief + Verifies if the linear form overflows. + + \return + Returns <CODE>false</CODE> if all coefficients in \p lf are bounded, + <CODE>true</CODE> otherwise. + + \p T must be the type of possibly unbounded quantities. + */ bool overflows() const;
+ /*! \brief + Computes the relative error associated to floating point computations + that operate on a quantity that is overapproximated by \p *this. + + \param analyzed_format The floating point format used by the analyzed + program. + \param result Becomes the linear form corresponding to the relative + error committed. + + This method makes <CODE>result</CODE> become a linear form + obtained by evaluating the function \f$\varepsilon_{\mathbf{f}}(l)\f$ + on the linear form. This function is defined as: + \f[ + \varepsilon_{\mathbf{f}}\left([a;b]+\sum_{v \in \cV}[a_{v};b_{v}]v\right) + \defeq + (\textrm{max}(|a|,|b|) \amifp [-\beta^{-\textrm{p}};\beta^{-\textrm{p}}]) + + + \sum_{v \in \cV}(\textrm{max}(|a_{v}|,|b_{v}|) + \amifp + [-\beta^{-\textrm{p}};\beta^{-\textrm{p}}])v + \f] + where p is the fraction size in bits for the format \f$\mathbf{f}\f$ and + \f$\beta\f$ the base. + + The result is undefined if \p T is not the type of an interval with + floating point boundaries. + */ void relative_error(Floating_Point_Format analyzed_format, Linear_Form& result) const;
+ /*! \brief + Makes \p result become an interval that overapproximates all the + possible values of \p *this in the interval abstract store \p store. + + \param store The abstract store. + \param result The linear form that will store the result. + + This method makes <CODE>result</CODE> become + \f$\iota(lf)\rho^{#}\f$, that is an interval defined as: + \f[ + \iota\left(i + \sum_{v \in \cV}i_{v}v\right)\rho^{#} + \defeq + i \asifp \left(\bigoplus_{v \in \cV}{}^{#}i_{v} \amifp + \rho^{#}(v)\right) + \f] + + The result is undefined if \p T is not the type of an interval with + floating point boundaries. + */ void intervalize(const Box<C>& store, C& result) const;
private: