- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Fixed a bug whereby a wrong computational weight was computed due to missing parentheses around a macro argument .
by Roberto Bagnara 21 Oct '11

21 Oct '11

Module: ppl/ppl Branch: master Commit: 8014bfef880f3b3dc0be3ee29b2c7d82472ba222 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8014bfef880f… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Oct 21 17:45:17 2011 +0200 Fixed a bug whereby a wrong computational weight was computed due to missing parentheses around a macro argument. Detected by ECLAIR service macrbody. --- src/globals.defs.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/globals.defs.hh b/src/globals.defs.hh index 310f133..6c45381 100644 --- a/src/globals.defs.hh +++ b/src/globals.defs.hh @@ -158,11 +158,11 @@ extern unsigned int in_assert; #define WEIGHT_BEGIN() #define WEIGHT_ADD(delta) \ do { \ - Weightwatch_Traits::weight += delta; \ + Weightwatch_Traits::weight += (delta); \ } while(0) #define WEIGHT_ADD_MUL(delta, factor) \ do { \ - Weightwatch_Traits::weight += delta * factor; \ + Weightwatch_Traits::weight += (delta)*(factor); \ } while(0) #endif #else

1 0

[GIT] ppl/ppl(master): Very long line shortened.
by Roberto Bagnara 21 Oct '11

21 Oct '11

Module: ppl/ppl Branch: master Commit: 5295880df1fc9f3a0fee656e9390c76fbb6f0984 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5295880df1fc… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Oct 21 16:36:01 2011 +0200 Very long line shortened. --- src/Checked_Number.inlines.hh | 6 ++++-- 1 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Checked_Number.inlines.hh b/src/Checked_Number.inlines.hh index 4364900..7c8e7cc 100644 --- a/src/Checked_Number.inlines.hh +++ b/src/Checked_Number.inlines.hh @@ -115,7 +115,8 @@ template <typename T, typename Policy> \ inline \ Checked_Number<T, Policy>::Checked_Number(const type x, Rounding_Dir dir) { \ Policy::handle_result \ - (check_result(Checked::assign_ext<Policy, Checked_Number_Transparent_Policy<type> > \ + (check_result(Checked::assign_ext<Policy, \ + Checked_Number_Transparent_Policy<type> > \ (v, x, rounding_dir(dir)), \ dir)); \ } \ @@ -124,7 +125,8 @@ inline \ Checked_Number<T, Policy>::Checked_Number(const type x) { \ Rounding_Dir dir = Policy::ROUND_DEFAULT_CONSTRUCTOR; \ Policy::handle_result \ - (check_result(Checked::assign_ext<Policy, Checked_Number_Transparent_Policy<type> > \ + (check_result(Checked::assign_ext<Policy, \ + Checked_Number_Transparent_Policy<type> > \ (v, x, rounding_dir(dir)), \ dir)); \ }

1 0

Fwd: RE: Re: ppl configure error
by Roberto Bagnara 20 Oct '11

20 Oct '11

-------- Original Message -------- Subject: RE: Re: [PPL-devel] ppl configure error Date: Thu, 20 Oct 2011 12:15:43 +0000 From: Li, Hui <lihui(a)imail.iu.edu> To: Roberto Bagnara <bagnara(a)cs.unipr.it> Hello Prof. Bagnara, The problem has been fixed after set up LD_LIBRARY_PATH. We are going to rebuild gcc_trunck to run lapack code which requires PPL lib. Thank you for the time and help. Hui ________________________________________ From: Roberto Bagnara [bagnara(a)cs.unipr.it] Sent: Thursday, October 20, 2011 01:35 AM To: Li, Hui Subject: Fwd: Re: [PPL-devel] ppl configure error -------- Original Message -------- Subject: Re: [PPL-devel] ppl configure error Date: Thu, 20 Oct 2011 08:19:14 +0200 From: Roberto Bagnara <bagnara(a)cs.unipr.it> Organization: Department of Mathematics, University of Parma, Italy To: ppl-devel(a)cs.unipr.it On 10/20/2011 05:59 AM, Li, Hui wrote: > Hello Prof. Bagnara, > > Yes, the gmpxx.h exist. And after prepending CPPFLAGS=-I/N/u/lihui/Quarry/gmp_install/include, the "gmpxx.h file not find" error fixed. > But it still throw out error says "ieeefp.h: No such file or directory". Here is the new config.log in the attachment. > > There is math.h in: > /usr/include/math.h > /usr/lib/x86_64-redhat-linux3E/include/math.h > > But there is no ieeefp.h found in above system include directory. > > Should I do some other configuration? Hi Hui, I don't see any problem involving ieeefp.h in your config.log. The problem could be that you have installed GMP in a non-standard place without instructing your dynamic linker/loader about where to find it. See `man ld.so' for more details. I guess that something like export LD_LIBRARY_PATH=/N/u/lihui/Quarry/gmp_install/lib:$LD_LIBRARY_PATH or export LD_LIBRARY_PATH=/N/u/lihui/Quarry/gmp_install/lib64:$LD_LIBRARY_PATH should work. Success, Roberto -- Prof. Roberto Bagnara Applied Formal Methods Laboratory Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0

[GIT] ppl/ppl(master): Updated to reflect the removal of `--with-gmp-prefix ' in favor of `--with-gmp'.
by Roberto Bagnara 20 Oct '11

20 Oct '11

Module: ppl/ppl Branch: master Commit: b8cc90bed27ca3cc4252baa2cc1c16f296e43044 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b8cc90bed27c… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Oct 20 08:38:01 2011 +0200 Updated to reflect the removal of `--with-gmp-prefix' in favor of `--with-gmp'. --- README.configure | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/README.configure b/README.configure index d25ac3f..f96ba90 100644 --- a/README.configure +++ b/README.configure @@ -100,7 +100,7 @@ is not standard for your compiler and/or for your linker, you will have to make sure the configure script of the PPL is invoked with, among others, the option - --with-gmp-prefix=<GMP prefix> + --with-gmp=<GMP prefix> If you use shared libraries, consult the documentation of your dynamic linker/loader (`man ld.so' will do on most Un*x-like systems) to see @@ -152,7 +152,7 @@ you can configure the PPL with a command like /path/to/ppl-x.y/configure --with-cxx=icpc --with-cc=icc \ --with-cxxflags=-pch \ - --with-gmp-prefix=/opt/intel/Compiler/11.1/072 + --with-gmp=/opt/intel/Compiler/11.1/072 Notice that the `--with-cxxflags' option is not essential here and is only included to show how extra compiler options can be passed to the @@ -169,7 +169,7 @@ Then you can configure the PPL with a command like /path/to/ppl/configure --with-cc="como --c" --with-cxx="como -tused" \ --with-cxxflags="-g++ --remarks --long_long \ --display_error_number --diag_suppress 340,401,679" \ - --disable-shared --with-gmp-prefix=/opt/comeau/local + --disable-shared --with-gmp=/opt/comeau/local Notice the use of the option `--disable-shared' both in the configuration of GMP and the configuration of the PPL. This is due to the fact that

1 0

ppl configure error
by Li, Hui 20 Oct '11

20 Oct '11

Hello, I got several error in the configure stage for the ppl-0.11.2. Here is the config.log in the attachment. And the configure options: ./configure --prefix=/N/u/lihui/ppl_install --exec-prefix=/N/u/lihui/ppl_install --with-gmp=/N/u/lihui/gmp_install the gmp was compiled with enable-cxx The system information: Red Hat Enterprise Linux AS release 4 (Nahant Update 9) Linux b001 2.6.9_78.0.22.EL_lustre.1.6.7.2_custom #6 SMP Mon Nov 9 14:28:25 EST 2009 x86_64 x86_64 x86_64 GNU/Linux Could you please tell what's the problem? I've search many pages but didn't get right solution, and any suggestion will be appreciated. Thanks, Hui

2 4

[GIT] ppl/ppl(master): Avoid excessive and dangerous reliance on the C++ operator precedence rules .
by Roberto Bagnara 18 Oct '11

18 Oct '11

Module: ppl/ppl Branch: master Commit: 703cc3ccfae900375897b441b2abfe0ad6e0f210 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=703cc3ccfae9… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Oct 18 19:51:59 2011 +0200 Avoid excessive and dangerous reliance on the C++ operator precedence rules. Detected by ECLAIR service exprprns. --- src/Linear_Expression.cc | 2 +- src/checked_int.inlines.hh | 15 ++++++++------- src/globals.inlines.hh | 2 +- 3 files changed, 10 insertions(+), 9 deletions(-) diff --git a/src/Linear_Expression.cc b/src/Linear_Expression.cc index f586ac4..86872a2 100644 --- a/src/Linear_Expression.cc +++ b/src/Linear_Expression.cc @@ -81,7 +81,7 @@ PPL::Linear_Expression::Linear_Expression(const Congruence& cg) PPL::Linear_Expression::Linear_Expression(const Variable v) : Linear_Row((v.space_dimension() <= max_space_dimension()) - ? v.space_dimension() + 1 + ? (v.space_dimension() + 1) : (throw std::length_error("PPL::Linear_Expression::" "Linear_Expression(v):\n" "v exceeds the maximum allowed " diff --git a/src/checked_int.inlines.hh b/src/checked_int.inlines.hh index 68d811f..00a4b98 100644 --- a/src/checked_int.inlines.hh +++ b/src/checked_int.inlines.hh @@ -72,18 +72,19 @@ template <typename Policy, typename Type> struct Extended_Int { static const Type plus_infinity = C_Integer<Type>::max; static const Type minus_infinity = ((C_Integer<Type>::min >= 0) - ? C_Integer<Type>::max - 1 + ? (C_Integer<Type>::max - 1) : C_Integer<Type>::min); static const Type not_a_number = ((C_Integer<Type>::min >= 0) - ? C_Integer<Type>::max - Policy::has_infinity * 2 - : C_Integer<Type>::min + Policy::has_infinity); + ? (C_Integer<Type>::max - Policy::has_infinity * 2) + : (C_Integer<Type>::min + Policy::has_infinity)); static const Type min = (C_Integer<Type>::min - + (C_Integer<Type>::min >= 0 ? 0 + + ((C_Integer<Type>::min >= 0) + ? 0 : (Policy::has_infinity + Policy::has_nan))); static const Type max = (C_Integer<Type>::max - ((C_Integer<Type>::min >= 0) - ? (2 * Policy::has_infinity + Policy::has_nan) + ? (2*Policy::has_infinity + Policy::has_nan) : Policy::has_infinity)); }; @@ -640,7 +641,7 @@ assign_signed_int_mpz(To& to, const mpz_class& from, Rounding_Dir dir) { } } } - return ::sgn(from) < 0 + return (::sgn(from) < 0) ? set_neg_overflow_int<To_Policy>(to, dir) : set_pos_overflow_int<To_Policy>(to, dir); } @@ -1369,7 +1370,7 @@ smod_2exp_unsigned_int(Type& to, const Type x, unsigned int exp, if (exp > sizeof(Type)*CHAR_BIT) to = x; else { - Type v = exp == sizeof(Type)*CHAR_BIT ? x : (x & ((Type(1) << exp) - 1)); + Type v = (exp == sizeof(Type)*CHAR_BIT ? x : (x & ((Type(1) << exp) - 1))); if (v >= Type(1) << (exp - 1)) return set_neg_overflow_int<To_Policy>(to, dir); else diff --git a/src/globals.inlines.hh b/src/globals.inlines.hh index 196c46c..fd71d71 100644 --- a/src/globals.inlines.hh +++ b/src/globals.inlines.hh @@ -71,7 +71,7 @@ compute_capacity(const dimension_type requested_size, assert(requested_size <= maximum_size); // Speculation factor 2. return (requested_size < maximum_size/2) - ? 2*(requested_size + 1) + ? (2*(requested_size + 1)) : maximum_size; // Speculation factor 1.5. // return (maximum_size - requested_size > requested_size/2)

1 0

[GIT] ppl/ppl(master): Avoid #include directives after code (except for "*. idefs.hh", "*.inlines.hh" and "*.templates.hh").
by Roberto Bagnara 18 Oct '11

18 Oct '11

Module: ppl/ppl Branch: master Commit: 615033adbfb7fbc0ec72cf5c35ef64d6c8935590 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=615033adbfb7… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Oct 18 16:14:35 2011 +0200 Avoid #include directives after code (except for "*.idefs.hh", "*.inlines.hh" and "*.templates.hh"). Detected by ECLAIR service inclmixd. --- src/Checked_Number.defs.hh | 1 - src/Coefficient.types.hh | 8 ++++---- src/Sparse_Row.defs.hh | 2 +- src/globals.defs.hh | 8 ++++---- 4 files changed, 9 insertions(+), 10 deletions(-) diff --git a/src/Checked_Number.defs.hh b/src/Checked_Number.defs.hh index 2f5578c..ba35243 100644 --- a/src/Checked_Number.defs.hh +++ b/src/Checked_Number.defs.hh @@ -1048,7 +1048,6 @@ int maybe_check_fpu_inexact(); } // namespace Parma_Polyhedra_Library #include "Checked_Number.inlines.hh" -#include "checked_numeric_limits.hh" #include "Checked_Number.templates.hh" #endif // !defined(PPL_Checked_Number_defs_hh) diff --git a/src/Coefficient.types.hh b/src/Coefficient.types.hh index 7e4d6b5..d090aab 100644 --- a/src/Coefficient.types.hh +++ b/src/Coefficient.types.hh @@ -15,6 +15,10 @@ PURPOSE. */ #include "Checked_Number.defs.hh" +#ifdef PPL_GMP_INTEGERS +#include "GMP_Integer.types.hh" +#endif + #if defined(PPL_CHECKED_INTEGERS) || defined(PPL_NATIVE_INTEGERS) namespace Parma_Polyhedra_Library { @@ -145,10 +149,6 @@ struct Coefficient_traits_template<Checked_Number<int64_t, Policy> > { #endif // defined(PPL_CHECKED_INTEGERS) || defined(PPL_NATIVE_INTEGERS) -#ifdef PPL_GMP_INTEGERS -#include "GMP_Integer.types.hh" -#endif - namespace Parma_Polyhedra_Library { //! An alias for easily naming the type of PPL coefficients. diff --git a/src/Sparse_Row.defs.hh b/src/Sparse_Row.defs.hh index ecc997b..7c14a29 100644 --- a/src/Sparse_Row.defs.hh +++ b/src/Sparse_Row.defs.hh @@ -836,7 +836,7 @@ bool operator!=(const Sparse_Row& x, const Sparse_Row& y); } // namespace Parma_Polyhedra_Library -#include "Sparse_Row.templates.hh" #include "Sparse_Row.inlines.hh" +#include "Sparse_Row.templates.hh" #endif // !defined(PPL_Sparse_Row_defs_hh) diff --git a/src/globals.defs.hh b/src/globals.defs.hh index 3be28b6..310f133 100644 --- a/src/globals.defs.hh +++ b/src/globals.defs.hh @@ -32,6 +32,10 @@ site: http://www.cs.unipr.it/ppl/ . */ #include <exception> #include <gmpxx.h> +#if defined(NDEBUG) && PPL_PROFILE_ADD_WEIGHT +#include "Weight_Profiler.defs.hh" +#endif + namespace Parma_Polyhedra_Library { //! Returns a value that does not designate a valid dimension. @@ -467,10 +471,6 @@ FOK(mpq_class) } // namespace Parma_Polyhedra_Library -#if defined(NDEBUG) && PPL_PROFILE_ADD_WEIGHT -#include "Weight_Profiler.defs.hh" -#endif - // By default, use sparse matrices both for MIP_Problem and PIP_Problem. #ifndef USE_PPL_SPARSE_MATRIX #define USE_PPL_SPARSE_MATRIX 1

1 0

[GIT] ppl/ppl(master): Avoid excessive and dangerous reliance on the C++ operator precedence rules .
by Roberto Bagnara 18 Oct '11

18 Oct '11

Module: ppl/ppl Branch: master Commit: 571c07fd424a775127467eecfc527c420c98ea2d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=571c07fd424a… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Oct 18 14:26:06 2011 +0200 Avoid excessive and dangerous reliance on the C++ operator precedence rules. Detected by ECLAIR service exprprns. --- src/Grid.inlines.hh | 16 ++++++++-------- src/Linear_Expression.cc | 2 +- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/Grid.inlines.hh b/src/Grid.inlines.hh index b04657c..006ba2f 100644 --- a/src/Grid.inlines.hh +++ b/src/Grid.inlines.hh @@ -187,10 +187,10 @@ inline Grid::Grid(const BD_Shape<U>& bd, Complexity_Class) : con_sys((bd.space_dimension() > max_space_dimension()) - ? throw_space_dimension_overflow("Grid(bd)", - "the space dimension of bd " - "exceeds the maximum allowed " - "space dimension"), 0 + ? (throw_space_dimension_overflow("Grid(bd)", + "the space dimension of bd " + "exceeds the maximum allowed " + "space dimension"), 0) : bd.space_dimension()), gen_sys(bd.space_dimension()) { Congruence_System cgs = bd.congruences(); @@ -202,10 +202,10 @@ inline Grid::Grid(const Octagonal_Shape<U>& os, Complexity_Class) : con_sys((os.space_dimension() > max_space_dimension()) - ? throw_space_dimension_overflow("Grid(os)", - "the space dimension of os " - "exceeds the maximum allowed " - "space dimension"), 0 + ? (throw_space_dimension_overflow("Grid(os)", + "the space dimension of os " + "exceeds the maximum allowed " + "space dimension"), 0) : os.space_dimension()), gen_sys(os.space_dimension()) { Congruence_System cgs = os.congruences(); diff --git a/src/Linear_Expression.cc b/src/Linear_Expression.cc index d7c997c..f586ac4 100644 --- a/src/Linear_Expression.cc +++ b/src/Linear_Expression.cc @@ -86,7 +86,7 @@ PPL::Linear_Expression::Linear_Expression(const Variable v) "Linear_Expression(v):\n" "v exceeds the maximum allowed " "space dimension."), - v.space_dimension() + 1), + (v.space_dimension() + 1)), Linear_Row::Flags()) { ++((*this)[v.space_dimension()]); }

1 0

[GIT] ppl/ppl(master): Avoid excessive and dangerous reliance on the C++ operator precedence rules .
by Roberto Bagnara 18 Oct '11

18 Oct '11

1 0

[GIT] ppl/ppl(master): Fixed MIP_Problem bug shown by tests/MIP_Problem/ mipproblem4.cc.
by Enea Zaffanella 17 Oct '11

17 Oct '11

Module: ppl/ppl Branch: master Commit: 09144610d98413a390afed2c0f5b189e7a9e5f30 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=09144610d984… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon Oct 17 09:52:30 2011 +0200 Fixed MIP_Problem bug shown by tests/MIP_Problem/mipproblem4.cc. --- src/MIP_Problem.cc | 11 ++++++++++- 1 files changed, 10 insertions(+), 1 deletions(-) diff --git a/src/MIP_Problem.cc b/src/MIP_Problem.cc index ed19471..9224ceb 100644 --- a/src/MIP_Problem.cc +++ b/src/MIP_Problem.cc @@ -1701,6 +1701,13 @@ PPL::MIP_Problem::erase_artificials(const dimension_type begin_artificials, // See page 55 of [PapadimitriouS98]. void PPL::MIP_Problem::compute_generator() const { + // Early exit for 0-dimensional problems. + if (external_space_dim == 0) { + MIP_Problem& x = const_cast<MIP_Problem&>(*this); + x.last_generator = point(); + return; + } + // We will store in num[] and in den[] the numerators and // the denominators of every variable of the original problem. std::vector<Coefficient> num(external_space_dim); @@ -1772,6 +1779,7 @@ PPL::MIP_Problem::compute_generator() const { } // Compute the lcm of all denominators. + PPL_ASSERT(external_space_dim > 0); lcm = den[0]; for (dimension_type i = 1; i < external_space_dim; ++i) lcm_assign(lcm, lcm, den[i]); @@ -1794,7 +1802,8 @@ PPL::MIP_Problem::compute_generator() const { void PPL::MIP_Problem::second_phase() { // Second_phase requires that *this is satisfiable. - PPL_ASSERT(status == SATISFIABLE || status == UNBOUNDED + PPL_ASSERT(status == SATISFIABLE + || status == UNBOUNDED || status == OPTIMIZED); // In the following cases the problem is already solved. if (status == UNBOUNDED || status == OPTIMIZED)

1 0