- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(ppl-0_12-branch): Merge branch 'master' into ppl-0_12-branch
by Roberto Bagnara 01 Apr '12

01 Apr '12

Module: ppl/ppl Branch: ppl-0_12-branch Commit: 5825555c3c7b681d2e881e7494b7c14a830f6235 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5825555c3c7b… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Apr 1 07:54:02 2012 +0200 Merge branch 'master' into ppl-0_12-branch ---

1 0

[GIT] ppl/ppl(ppl-0_12-branch): Updated for Doxygen 1.8.0.
by Roberto Bagnara 01 Apr '12

01 Apr '12

Module: ppl/ppl Branch: ppl-0_12-branch Commit: ab71409476eee8f3c120b0a481eb767819eb935a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ab71409476ee… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Apr 1 07:53:29 2012 +0200 Updated for Doxygen 1.8.0. --- doc/devref-language-interface.doxyconf.in | 14 ++++++++++++-- doc/devref.doxyconf-html.in | 14 ++++++++++++-- doc/devref.doxyconf-latex.in | 14 ++++++++++++-- doc/user-language-interface.doxyconf.in | 14 ++++++++++++-- doc/user.doxyconf-html.in | 14 ++++++++++++-- doc/user.doxyconf-latex.in | 14 ++++++++++++-- 6 files changed, 72 insertions(+), 12 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=ab714094…

1 0

[GIT] ppl/ppl(master): Updated for Doxygen 1.8.0.
by Roberto Bagnara 01 Apr '12

01 Apr '12

Module: ppl/ppl Branch: master Commit: ab71409476eee8f3c120b0a481eb767819eb935a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ab71409476ee… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Apr 1 07:53:29 2012 +0200 Updated for Doxygen 1.8.0. --- doc/devref-language-interface.doxyconf.in | 14 ++++++++++++-- doc/devref.doxyconf-html.in | 14 ++++++++++++-- doc/devref.doxyconf-latex.in | 14 ++++++++++++-- doc/user-language-interface.doxyconf.in | 14 ++++++++++++-- doc/user.doxyconf-html.in | 14 ++++++++++++-- doc/user.doxyconf-latex.in | 14 ++++++++++++-- 6 files changed, 72 insertions(+), 12 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=ab714094…

1 0

[GIT] ppl/ppl(ppl-0_12-branch): New commits
by Roberto Bagnara 31 Mar '12

31 Mar '12

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c58ed0768af4… Merge: 0a17ebd902c02367b7bf686d5e0f5a008e0290a2 7cac8985192bd1b37ce930feb1c60a47e4f5a144 Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Mar 31 21:25:10 2012 +0200 Merge branch 'master' into ppl-0_12-branch URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7cac8985192b… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Mar 31 21:06:51 2012 +0200 Indentation fixed. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9c0584c35178… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 31 13:58:31 2012 +0200 Simplified INPUT tag values in devref manuals' Doxygen configuration files. Avoid most of the explicit listing of source files, favouring a much smaller number of file name patterns. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b495379843cd… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 31 13:57:10 2012 +0200 Doxygen \relates command can not be used with enumerated types. Replace it with \name grouping. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=daeeb3466009… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 31 10:39:18 2012 +0200 No longer using the installdox command (deprecated and subject to removal). Fixed Doxygen configuration paths for license files. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=992e9dc81a58… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 31 10:20:08 2012 +0200 Further improvements to documentation of helper functions. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1d37ea40c807… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 31 10:08:05 2012 +0200 Use Doxygen command \class for declared-but-undefined class templates. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ad78ee45b1a5… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 31 10:06:55 2012 +0200 Improved documentation formatting using Doxygen command \tparam. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e99a61bf4826… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 31 09:57:42 2012 +0200 Fixed typo in documentation (causing a Doxygen warning). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7925c6720856… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 31 08:46:58 2012 +0200 Corrected name of Doxygen documentation group. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fdf149dd64f6… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Mar 30 18:14:55 2012 +0200 On machines where float is supported and double is not supported, test01() can yield results that are significantly less precise. (Thanks to Sean McGovern.)

1 0

[GIT] ppl/ppl(master): Indentation fixed.
by Roberto Bagnara 31 Mar '12

31 Mar '12

Module: ppl/ppl Branch: master Commit: 7cac8985192bd1b37ce930feb1c60a47e4f5a144 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7cac8985192b… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Mar 31 21:06:51 2012 +0200 Indentation fixed. --- src/Octagonal_Shape.defs.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index 622c546..199bfbe 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -1399,7 +1399,7 @@ public: \leq \mathrm{var}' \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}\f$. - \param var + \param var The variable updated by the affine relation; \param lb_expr

1 0

[GIT] ppl/ppl(ppl-0_12-branch): New commits
by Roberto Bagnara 31 Mar '12

31 Mar '12

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0a17ebd902c0… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 31 13:58:31 2012 +0200 Simplified INPUT tag values in devref manuals' Doxygen configuration files. Avoid most of the explicit listing of source files, favouring a much smaller number of file name patterns. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8d4bbf8168ee… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 31 13:57:10 2012 +0200 Doxygen \relates command can not be used with enumerated types. Replace it with \name grouping. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=052bd0288227… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 31 10:39:18 2012 +0200 No longer using the installdox command (deprecated and subject to removal). Fixed Doxygen configuration paths for license files. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c001b60d38da… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 31 10:20:08 2012 +0200 Further improvements to documentation of helper functions. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c84ea3af8b24… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 31 10:08:05 2012 +0200 Use Doxygen command \class for declared-but-undefined class templates. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4c27bdb4393b… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 31 10:06:55 2012 +0200 Improved documentation formatting using Doxygen command \tparam. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=50e97568b488… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 31 09:57:42 2012 +0200 Fixed typo in documentation (causing a Doxygen warning). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e3d6db5783e4… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 31 08:46:58 2012 +0200 Corrected name of Doxygen documentation group.

1 0

[GIT] ppl/ppl(master): Simplified INPUT tag values in devref manuals' Doxygen configuration files.
by Enea Zaffanella 31 Mar '12

31 Mar '12

Module: ppl/ppl Branch: master Commit: 9c0584c351784f395a16b240546fc5316b1413f6 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9c0584c35178… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 31 13:58:31 2012 +0200 Simplified INPUT tag values in devref manuals' Doxygen configuration files. Avoid most of the explicit listing of source files, favouring a much smaller number of file name patterns. --- doc/devref.doxyconf-html.in | 357 +++--------------------------------------- doc/devref.doxyconf-latex.in | 352 +++-------------------------------------- 2 files changed, 50 insertions(+), 659 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=9c0584c3…

1 0

[GIT] ppl/ppl(master): Doxygen \relates command can not be used with enumerated types.
by Enea Zaffanella 31 Mar '12

31 Mar '12

Module: ppl/ppl Branch: master Commit: b495379843cdc1ba429cef608e79a09757c9a6e7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b495379843cd… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 31 13:57:10 2012 +0200 Doxygen \relates command can not be used with enumerated types. Replace it with \name grouping. --- src/Result.defs.hh | 22 ++++++++++++++++++++-- src/Result.inlines.hh | 12 ++++++------ src/Rounding_Dir.defs.hh | 27 ++++++++++++++++++++++++++- src/Rounding_Dir.inlines.hh | 26 +++++++++++++------------- 4 files changed, 65 insertions(+), 22 deletions(-) diff --git a/src/Result.defs.hh b/src/Result.defs.hh index 35eac7a..fa2fc2f 100644 --- a/src/Result.defs.hh +++ b/src/Result.defs.hh @@ -160,16 +160,34 @@ enum Result { }; +//! \name Functions Inspecting and/or Combining Result Values +//@{ + +/*! \ingroup PPL_CXX_interface */ Result operator&(Result x, Result y); + +/*! \ingroup PPL_CXX_interface */ Result operator|(Result x, Result y); + +/*! \ingroup PPL_CXX_interface */ Result operator-(Result x, Result y); -//! Extracts the value class part of \p r (representable number, unrepresentable minus/plus infinity or nan). +/*! \brief \ingroup PPL_CXX_interface + Extracts the value class part of \p r (representable number, + unrepresentable minus/plus infinity or nan). +*/ Result_Class result_class(Result r); -//! Extracts the relation part of \p r. +/*! \brief \ingroup PPL_CXX_interface + Extracts the relation part of \p r. +*/ Result_Relation result_relation(Result r); +/*! \ingroup PPL_CXX_interface */ +Result result_relation_class(Result r); + +//@} // Functions Inspecting and/or Combining Result Values + } // namespace Parma_Polyhedra_Library #include "Result.inlines.hh" diff --git a/src/Result.inlines.hh b/src/Result.inlines.hh index 5141347..2f22082 100644 --- a/src/Result.inlines.hh +++ b/src/Result.inlines.hh @@ -28,42 +28,42 @@ site: http://bugseng.com/products/ppl/ . */ namespace Parma_Polyhedra_Library { -/*! \relates Parma_Polyhedra_Library::Result */ +/*! \ingroup PPL_CXX_interface */ inline Result operator&(Result x, Result y) { unsigned res = static_cast<unsigned>(x) & static_cast<unsigned>(y); return static_cast<Result>(res); } -/*! \relates Parma_Polyhedra_Library::Result */ +/*! \ingroup PPL_CXX_interface */ inline Result operator|(Result x, Result y) { unsigned res = static_cast<unsigned>(x) | static_cast<unsigned>(y); return static_cast<Result>(res); } -/*! \relates Parma_Polyhedra_Library::Result */ +/*! \ingroup PPL_CXX_interface */ inline Result operator-(Result x, Result y) { Result y_neg = static_cast<Result>(~static_cast<unsigned>(y)); return x & y_neg; } -/*! \relates Parma_Polyhedra_Library::Result */ +/*! \ingroup PPL_CXX_interface */ inline Result_Class result_class(Result r) { Result rc = r & static_cast<Result>(VC_MASK); return static_cast<Result_Class>(rc); } -/*! \relates Parma_Polyhedra_Library::Result */ +/*! \ingroup PPL_CXX_interface */ inline Result_Relation result_relation(Result r) { Result rc = r & static_cast<Result>(VR_MASK); return static_cast<Result_Relation>(rc); } -/*! \relates Parma_Polyhedra_Library::Result */ +/*! \ingroup PPL_CXX_interface */ inline Result result_relation_class(Result r) { return r & (static_cast<Result>(VR_MASK) | static_cast<Result>(VC_MASK)); diff --git a/src/Rounding_Dir.defs.hh b/src/Rounding_Dir.defs.hh index 15c7d63..f9161f0 100644 --- a/src/Rounding_Dir.defs.hh +++ b/src/Rounding_Dir.defs.hh @@ -69,28 +69,53 @@ enum Rounding_Dir { ROUND_CHECK = ROUND_DIRECT | ROUND_STRICT_RELATION }; +//! \name Functions Inspecting and/or Combining Rounding_Dir Values +//@{ + +/*! \ingroup PPL_CXX_interface */ Rounding_Dir operator&(Rounding_Dir x, Rounding_Dir y); + +/*! \ingroup PPL_CXX_interface */ Rounding_Dir operator|(Rounding_Dir x, Rounding_Dir y); -/*! \brief +/*! \brief \ingroup PPL_CXX_interface Returns the inverse rounding mode of \p dir, <CODE>ROUND_IGNORE</CODE> being the inverse of itself. */ Rounding_Dir inverse(Rounding_Dir dir); +/*! \ingroup PPL_CXX_interface */ Rounding_Dir round_dir(Rounding_Dir dir); + +/*! \ingroup PPL_CXX_interface */ bool round_down(Rounding_Dir dir); + +/*! \ingroup PPL_CXX_interface */ bool round_up(Rounding_Dir dir); + +/*! \ingroup PPL_CXX_interface */ bool round_ignore(Rounding_Dir dir); + +/*! \ingroup PPL_CXX_interface */ bool round_not_needed(Rounding_Dir dir); + +/*! \ingroup PPL_CXX_interface */ bool round_not_requested(Rounding_Dir dir); + +/*! \ingroup PPL_CXX_interface */ bool round_direct(Rounding_Dir dir); + +/*! \ingroup PPL_CXX_interface */ bool round_inverse(Rounding_Dir dir); +/*! \ingroup PPL_CXX_interface */ bool round_strict_relation(Rounding_Dir dir); +/*! \ingroup PPL_CXX_interface */ fpu_rounding_direction_type round_fpu_dir(Rounding_Dir dir); +//@} // Functions Inspecting and/or Combining Rounding_Dir Values + } // namespace Parma_Polyhedra_Library #include "Rounding_Dir.inlines.hh" diff --git a/src/Rounding_Dir.inlines.hh b/src/Rounding_Dir.inlines.hh index 12b9823..8b50802 100644 --- a/src/Rounding_Dir.inlines.hh +++ b/src/Rounding_Dir.inlines.hh @@ -28,69 +28,69 @@ site: http://bugseng.com/products/ppl/ . */ namespace Parma_Polyhedra_Library { -/*! \relates Parma_Polyhedra_Library::Rounding_Dir */ +/*! \ingroup PPL_CXX_interface */ inline Rounding_Dir operator&(Rounding_Dir x, Rounding_Dir y) { unsigned res = static_cast<unsigned>(x) & static_cast<unsigned>(y); return static_cast<Rounding_Dir>(res); } -/*! \relates Parma_Polyhedra_Library::Rounding_Dir */ +/*! \ingroup PPL_CXX_interface */ inline Rounding_Dir operator|(Rounding_Dir x, Rounding_Dir y) { unsigned res = static_cast<unsigned>(x) | static_cast<unsigned>(y); return static_cast<Rounding_Dir>(res); } -/*! \relates Parma_Polyhedra_Library::Rounding_Dir */ +/*! \ingroup PPL_CXX_interface */ inline Rounding_Dir round_dir(Rounding_Dir dir) { return dir & ROUND_DIR_MASK; } -/*! \relates Parma_Polyhedra_Library::Rounding_Dir */ +/*! \ingroup PPL_CXX_interface */ inline bool round_down(Rounding_Dir dir) { return round_dir(dir) == ROUND_DOWN; } -/*! \relates Parma_Polyhedra_Library::Rounding_Dir */ +/*! \ingroup PPL_CXX_interface */ inline bool round_up(Rounding_Dir dir) { return round_dir(dir) == ROUND_UP; } -/*! \relates Parma_Polyhedra_Library::Rounding_Dir */ +/*! \ingroup PPL_CXX_interface */ inline bool round_ignore(Rounding_Dir dir) { return round_dir(dir) == ROUND_IGNORE; } -/*! \relates Parma_Polyhedra_Library::Rounding_Dir */ +/*! \ingroup PPL_CXX_interface */ inline bool round_not_needed(Rounding_Dir dir) { return round_dir(dir) == ROUND_NOT_NEEDED; } -/*! \relates Parma_Polyhedra_Library::Rounding_Dir */ +/*! \ingroup PPL_CXX_interface */ inline bool round_not_requested(Rounding_Dir dir) { return round_dir(dir) == ROUND_IGNORE || round_dir(dir) == ROUND_NOT_NEEDED; } -/*! \relates Parma_Polyhedra_Library::Rounding_Dir */ +/*! \ingroup PPL_CXX_interface */ inline bool round_direct(Rounding_Dir dir) { return round_dir(dir) == ROUND_DIRECT; } -/*! \relates Parma_Polyhedra_Library::Rounding_Dir */ +/*! \ingroup PPL_CXX_interface */ inline bool round_inverse(Rounding_Dir dir) { return round_dir(dir) == ROUND_INVERSE; } -/*! \relates Parma_Polyhedra_Library::Rounding_Dir */ +/*! \ingroup PPL_CXX_interface */ inline bool round_strict_relation(Rounding_Dir dir) { return (dir & ROUND_STRICT_RELATION) == ROUND_STRICT_RELATION; @@ -98,7 +98,7 @@ round_strict_relation(Rounding_Dir dir) { #if PPL_CAN_CONTROL_FPU -/*! \relates Parma_Polyhedra_Library::Rounding_Dir */ +/*! \ingroup PPL_CXX_interface */ inline fpu_rounding_direction_type round_fpu_dir(Rounding_Dir dir) { switch (round_dir(dir)) { @@ -120,7 +120,7 @@ round_fpu_dir(Rounding_Dir dir) { #endif -/*! \relates Parma_Polyhedra_Library::Rounding_Dir */ +/*! \ingroup PPL_CXX_interface */ inline Rounding_Dir inverse(Rounding_Dir dir) { switch (round_dir(dir)) {

1 0

[GIT] ppl/ppl(master): No longer using the installdox command ( deprecated and subject to removal).
by Enea Zaffanella 31 Mar '12

31 Mar '12

Module: ppl/ppl Branch: master Commit: daeeb34660099b742150e96df970e3b1a6a882da URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=daeeb3466009… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 31 10:39:18 2012 +0200 No longer using the installdox command (deprecated and subject to removal). Fixed Doxygen configuration paths for license files. --- doc/Makefile.am | 74 ++++++++++++++++++------------------------------------ 1 files changed, 25 insertions(+), 49 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=daeeb346…

1 0

[GIT] ppl/ppl(master): Further improvements to documentation of helper functions.
by Enea Zaffanella 31 Mar '12

31 Mar '12

Module: ppl/ppl Branch: master Commit: 992e9dc81a58f65429e7650ca2077fd95f1efda1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=992e9dc81a58… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 31 10:20:08 2012 +0200 Further improvements to documentation of helper functions. --- src/linearize.hh | 190 ++++++++++++++++++++++++++++++++--------------------- 1 files changed, 115 insertions(+), 75 deletions(-) diff --git a/src/linearize.hh b/src/linearize.hh index 6bd75d8..1a074ae 100644 --- a/src/linearize.hh +++ b/src/linearize.hh @@ -32,30 +32,38 @@ site: http://bugseng.com/products/ppl/ . */ namespace Parma_Polyhedra_Library { -/*! \brief +/*! \brief \relates Parma_Polyhedra_Library::Concrete_Expression Helper function used by <CODE>linearize</CODE> to linearize a sum of floating point expressions. - \par Template type parameters - - - The class template parameter \p Target specifies the implementation - of Concrete_Expression to be used. - - 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. - Makes \p result become the linearization of \p *this in the given composite abstract store. - \param bop_expr The binary operator concrete expression to linearize. - Its binary operator type must be <CODE>ADD</CODE>. - \param oracle The FP_Oracle to be queried. - \param lf_store The linear form abstract store. - \param result The modified linear form. + \tparam Target + A type template parameter specifying the instantiation of + Concrete_Expression to be used. + + \tparam FP_Interval_Type + A type template parameter for the intervals used in the abstract domain. + The interval bounds should have a floating point type. - \return <CODE>true</CODE> if the linearization succeeded, + \return + <CODE>true</CODE> if the linearization succeeded, <CODE>false</CODE> otherwise. + \param bop_expr + The binary operator concrete expression to linearize. + Its binary operator type must be <CODE>ADD</CODE>. + + \param oracle + The FP_Oracle to be queried. + + \param lf_store + The linear form abstract store. + + \param result + The modified linear form. + \par Linearization of sum floating-point expressions Let \f$i + \sum_{v \in \cV}i_{v}v \f$ and @@ -132,30 +140,38 @@ add_linearize(const Binary_Operator<Target>& bop_expr, return !result.overflows(); } -/*! \brief +/*! \brief \relates Parma_Polyhedra_Library::Concrete_Expression Helper function used by <CODE>linearize</CODE> to linearize a difference of floating point expressions. - \par Template type parameters - - - The class template parameter \p Target specifies the implementation - of Concrete_Expression to be used. - - 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. - Makes \p result become the linearization of \p *this in the given composite abstract store. - \param bop_expr The binary operator concrete expression to linearize. - Its binary operator type must be <CODE>SUB</CODE>. - \param oracle The FP_Oracle to be queried. - \param lf_store The linear form abstract store. - \param result The modified linear form. + \tparam Target + A type template parameter specifying the instantiation of + Concrete_Expression to be used. - \return <CODE>true</CODE> if the linearization succeeded, + \tparam FP_Interval_Type + A type template parameter for the intervals used in the abstract domain. + The interval bounds should have a floating point type. + + \return + <CODE>true</CODE> if the linearization succeeded, <CODE>false</CODE> otherwise. + \param bop_expr + The binary operator concrete expression to linearize. + Its binary operator type must be <CODE>SUB</CODE>. + + \param oracle + The FP_Oracle to be queried. + + \param lf_store + The linear form abstract store. + + \param result + The modified linear form. + \par Linearization of difference floating-point expressions Let \f$i + \sum_{v \in \cV}i_{v}v \f$ and @@ -238,30 +254,38 @@ sub_linearize(const Binary_Operator<Target>& bop_expr, return !result.overflows(); } -/*! \brief +/*! \brief \relates Parma_Polyhedra_Library::Concrete_Expression Helper function used by <CODE>linearize</CODE> to linearize a product of floating point expressions. - \par Template type parameters - - - The class template parameter \p Target specifies the implementation - of Concrete_Expression to be used. - - 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. - Makes \p result become the linearization of \p *this in the given composite abstract store. - \param bop_expr The binary operator concrete expression to linearize. - Its binary operator type must be <CODE>MUL</CODE>. - \param oracle The FP_Oracle to be queried. - \param lf_store The linear form abstract store. - \param result The modified linear form. + \tparam Target + A type template parameter specifying the instantiation of + Concrete_Expression to be used. + + \tparam FP_Interval_Type + A type template parameter for the intervals used in the abstract domain. + The interval bounds should have a floating point type. - \return <CODE>true</CODE> if the linearization succeeded, + \return + <CODE>true</CODE> if the linearization succeeded, <CODE>false</CODE> otherwise. + \param bop_expr + The binary operator concrete expression to linearize. + Its binary operator type must be <CODE>MUL</CODE>. + + \param oracle + The FP_Oracle to be queried. + + \param lf_store + The linear form abstract store. + + \param result + The modified linear form. + \par Linearization of multiplication floating-point expressions Let \f$i + \sum_{v \in \cV}i_{v}v \f$ and @@ -428,30 +452,38 @@ mul_linearize(const Binary_Operator<Target>& bop_expr, return !result.overflows(); } -/*! \brief +/*! \brief \relates Parma_Polyhedra_Library::Concrete_Expression Helper function used by <CODE>linearize</CODE> to linearize a division of floating point expressions. - \par Template type parameters - - - The class template parameter \p Target specifies the implementation - of Concrete_Expression to be used. - - 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. - Makes \p result become the linearization of \p *this in the given composite abstract store. - \param bop_expr The binary operator concrete expression to linearize. - Its binary operator type must be <CODE>DIV</CODE>. - \param oracle The FP_Oracle to be queried. - \param lf_store The linear form abstract store. - \param result The modified linear form. + \tparam Target + A type template parameter specifying the instantiation of + Concrete_Expression to be used. - \return <CODE>true</CODE> if the linearization succeeded, + \tparam FP_Interval_Type + A type template parameter for the intervals used in the abstract domain. + The interval bounds should have a floating point type. + + \return + <CODE>true</CODE> if the linearization succeeded, <CODE>false</CODE> otherwise. + \param bop_expr + The binary operator concrete expression to linearize. + Its binary operator type must be <CODE>DIV</CODE>. + + \param oracle + The FP_Oracle to be queried. + + \param lf_store + The linear form abstract store. + + \param result + The modified linear form. + \par Linearization of division floating-point expressions Let \f$i + \sum_{v \in \cV}i_{v}v \f$ and @@ -561,28 +593,36 @@ div_linearize(const Binary_Operator<Target>& bop_expr, return !result.overflows(); } -/*! \brief +/*! \brief \relates Parma_Polyhedra_Library::Concrete_Expression Helper function used by <CODE>linearize</CODE> to linearize a cast floating point expression. - \par Template type parameters - - - The class template parameter \p Target specifies the implementation - of Concrete_Expression to be used. - - 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. - Makes \p result become the linearization of \p *this in the given composite abstract store. - \param cast_expr The cast operator concrete expression to linearize. - \param oracle The FP_Oracle to be queried. - \param lf_store The linear form abstract store. - \param result The modified linear form. + \tparam Target + A type template parameter specifying the instantiation of + Concrete_Expression to be used. - \return <CODE>true</CODE> if the linearization succeeded, + \tparam FP_Interval_Type + A type template parameter for the intervals used in the abstract domain. + The interval bounds should have a floating point type. + + \return + <CODE>true</CODE> if the linearization succeeded, <CODE>false</CODE> otherwise. + + \param cast_expr + The cast operator concrete expression to linearize. + + \param oracle + The FP_Oracle to be queried. + + \param lf_store + The linear form abstract store. + + \param result + The modified linear form. */ template <typename Target, typename FP_Interval_Type> static bool @@ -644,7 +684,7 @@ cast_linearize(const Cast_Operator<Target>& cast_expr, } //! Linearizes a floating point expression. -/*! \relates Concrete_Expression +/*! \relates Parma_Polyhedra_Library::Concrete_Expression Makes \p result become a linear form that correctly approximates the value of \p expr in the given composite abstract store.

1 0