February 2012 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Wrong guard fixed.
by Roberto Bagnara 25 Feb '12

25 Feb '12

Module: ppl/ppl Branch: master Commit: 637df0294f81d71e4f00d55063be06cf34adf4c4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=637df0294f81… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Feb 25 18:22:24 2012 +0100 Wrong guard fixed. --- demos/ppl_lpsol/ppl_lpsol.c | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/demos/ppl_lpsol/ppl_lpsol.c b/demos/ppl_lpsol/ppl_lpsol.c index 9a72e40..8c62b94 100644 --- a/demos/ppl_lpsol/ppl_lpsol.c +++ b/demos/ppl_lpsol/ppl_lpsol.c @@ -326,7 +326,7 @@ process_options(int argc, char* argv[]) { my_exit(0); break; -#ifdef PPL_LPSOL_SUPPORTS_TIMINGS +#ifdef PPL_LPSOL_SUPPORTS_LIMIT_ON_CPU_TIME case 'C': l = strtol(optarg, &endptr, 10);

1 0

[GIT] ppl/ppl(master): Updated.
by Roberto Bagnara 25 Feb '12

25 Feb '12

Module: ppl/ppl Branch: master Commit: e87943772e7901e7b5c0e550d89742423b7fe225 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e87943772e79… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Feb 25 18:16:44 2012 +0100 Updated. --- CREDITS | 28 +++++++++++++++------------- NEWS | 2 +- README | 17 ++++++++++++----- ppl.lsm.in | 36 +++++++++++++++++++++++++----------- 4 files changed, 53 insertions(+), 30 deletions(-) diff --git a/CREDITS b/CREDITS index a34375e..99aa556 100644 --- a/CREDITS +++ b/CREDITS @@ -88,9 +88,9 @@ Past Contributors: algorithms for rational grids and products of grids and polyhedra. - Giordano Fracasso (University of Parma) wrote the initial version - of the support for native and checked integer - coefficients. + Giordano Fracasso (former student of the University of Parma) wrote + the initial version of the support for native + and checked integer coefficients. Francois Galea [5] (University of Versailles) worked at the implementation of the Parametric Integer @@ -100,11 +100,12 @@ Past Contributors: helped a little to improve the documentation for bounded differences. - Elena Mazzi (University of Parma) worked on our implementation - of bounded differences and octagons. She also - participated in the theoretical and practical - work concerning widening operators for weakly - relational domains. + Elena Mazzi (former student of the University of Parma) worked + on our implementation of bounded differences + and octagons. She also participated in the + theoretical and practical work concerning + widening operators for weakly relational + domains. David Merchat (formerly at the University of Parma) helped us with the generation of the library's documentation @@ -129,11 +130,12 @@ Past Contributors: Angela Stazzone (former student of the University of Parma) worked on the library's documentation. - Fabio Trabucchi (University of Parma) worked on a development - branch where he added serializers for all the - objects of the PPL. Support for serialization - based on Fabio's work will be available in a - future release of the library. + Fabio Trabucchi (former student of the University of Parma) worked + on a development branch where he added + serializers for all the objects of the PPL. + Support for serialization based on Fabio's + work will be available in a future release of + the library. Claudio Trento (former student of the University of Pisa) did a small amount of work on an experimental OCaml diff --git a/NEWS b/NEWS index 5807807..7de2386 100644 --- a/NEWS +++ b/NEWS @@ -10,7 +10,7 @@ Parma Polyhedra Library NEWS -- history of user-visible changes -------------------------------------------------------------------------- -NEWS for version 0.12 (release date to be decided) +NEWS for version 0.12 (released on February 27, 2012) -------------------------------------------------------------------------- New and Changed Features diff --git a/README b/README index 785214b..079e65a 100644 --- a/README +++ b/README @@ -17,17 +17,24 @@ To be more precise, the Parma Polyhedra Library (PPL) can handle: by an equality or a (strict or non-strict) inequality with rational coefficients; - + convex polyhedra defined by systems of bounded differences with - a wide choice of integer, rational or floating point coefficients; + + some special classes of polyhedra shapes that offer interesting + complexity/precision tradeoffs: boxes, bounded difference shapes + and octagonal shapes defined over a wide choice of integer, + rational or floating point coefficients; - + all grids (or, equivalently, lattices); a grid is defined by a set + + all grids (or, equivalently, lattices): a grid is defined by a set of congruence relations with rational coefficients and consists of the set of all points that satisfy these relations; - + finite powersets of the above; + + finite powersets and products of the above; + linear programming problems, solved with an implementation of the - primal simplex algorithm using exact arithmetic. + primal simplex algorithm using exact arithmetic; + + + parametric integer programming problems; + + + termination analysis problems, via the automatic synthesis of + linear ranking functions. The Parma Polyhedra Library is: diff --git a/ppl.lsm.in b/ppl.lsm.in index 6f20d00..0e01b58 100644 --- a/ppl.lsm.in +++ b/ppl.lsm.in @@ -4,24 +4,38 @@ Version: @VERSION@ Entered-date: @ISODATE@ Description: The Parma Polyhedra Library (PPL) is a C++ library for the manipulation of numerical abstractions. -Keywords: C++ library convex polyhedra -Author: Roberto Bagnara (bagnara(a)cs.unipr.it) - Patricia M. Hill (hill(a)comp.leeds.ac.uk) - Enea Zaffanella (zaffanella(a)cs.unipr.it) - Abramo Bagnara (Opera Unica) - Andrea Cimino (University of Parma) - Giordano Fracasso (University of Parma) - Elena Mazzi (University of Parma) - Matthew Mundell (University of Leeds) - Barbara Quartieri (University of Parma) +Keywords: C++ library convex polyhedra verification +Author: Roberto Bagnara (BUGSENG srl and University of Parma) + Patricia M. Hill (BUGSENG srl and University of Leeds) + Enea Zaffanella (BUGSENG srl and University of Parma) + Abramo Bagnara (BUGSENG srl) Elisa Ricci (former student of the University of Parma) + Marco Poletti (student of the University of Bologna) + Alessandro Zaccagnini (University of Parma) + Roberto Amadini (former student of the University of Parma) + Irene Bacchi (former student of the University of Parma) + Fabio Biselli (student of the University of Parma) + Fabio Bossi (former student of the University of Parma) + Danilo Bonardi (former student of the University of Parma) Sara Bonini (former student of the University of Parma) + Andrea Cimino (former student of the University of Parma) + Katy Dobson (former student of the University of Leeds) + Giordano Fracasso (former student of the University of Parma) + Francois Galea (University of Versailles) + Maximiliano Marchesi (former student of the University of Parma) + Elena Mazzi (former student of the University of Parma) + David Merchat (formerly at the University of Parma) + Matthew Mundell (formerly at the University of Leeds) Andrea Pescetti (former student of the University of Parma) + Barbara Quartieri (former student of the University of Parma) + Enric Rodriguez Carbonell (Technical University of Catalonia) Angela Stazzone (former student of the University of Parma) + Fabio Trabucchi (University of Parma) + Claudio Trento (former student of the University of Pisa) Tatiana Zolo (former student of the University of Parma) Maintained-by: ppl-devel(a)cs.unipr.it (PPL developers) Primary-site: metlab.unc.edu /pub/linux/libs - 5850k ppl-@VERSION@.tar.gz + 16788k ppl-@VERSION@.tar.gz 800 ppl.lsm Alternate-site: Original-site: http://bugseng.com/products/ppl/

1 0

[GIT] ppl/ppl(master): Hide enum initializers from docs.
by Enea Zaffanella 25 Feb '12

25 Feb '12

Module: ppl/ppl Branch: master Commit: bbc3deda4d9ee21af4609396779e4ab1bde16d5b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=bbc3deda4d9e… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Feb 25 18:09:09 2012 +0100 Hide enum initializers from docs. Remove I_Result enumeration form user manual. --- src/intervals.defs.hh | 45 ++++++++++++++++++++++++++++----------------- 1 files changed, 28 insertions(+), 17 deletions(-) diff --git a/src/intervals.defs.hh b/src/intervals.defs.hh index a4f3754..92b7693 100644 --- a/src/intervals.defs.hh +++ b/src/intervals.defs.hh @@ -31,46 +31,55 @@ site: http://bugseng.com/products/ppl/ . */ namespace Parma_Polyhedra_Library { +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS +//! The result of an operation on intervals. +/*! \ingroup PPL_CXX_interface */ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) enum I_Result { - //! The resulting set may be empty + //! \hideinitializer Result may be empty I_EMPTY = 1U, - //! The resulting set may have only one value + //! \hideinitializer Result may have only one value I_SINGLETON = 2U, - //! The resulting set may have more than one value and to be not the domain universe + /*! \brief \hideinitializer + Result may have more than one value, but it is not the domain universe + */ I_SOME = 4U, - //! The resulting set may be the domain universe + //! \hideinitializer Result may be the domain universe I_UNIVERSE = 8U, - //! The resulting set is not empty + //! \hideinitializer Result is not empty I_NOT_EMPTY = I_SINGLETON | I_SOME | I_UNIVERSE, - //! The resulting set may be empty or not empty + //! \hideinitializer Result may be empty or not empty I_ANY = I_EMPTY | I_NOT_EMPTY, - //! The resulting set may be empty or not empty + //! \hideinitializer Result may be empty or not empty I_NOT_UNIVERSE = I_EMPTY | I_SINGLETON | I_SOME, - //! The resulting set can'be empty or the domain universe + //! \hideinitializer Result is neither empty nor the domain universe I_NOT_DEGENERATE = I_SINGLETON | I_SOME, - //! The resulting set is definitely exact + //! \hideinitializer Result is definitely exact I_EXACT = 16, - //! The resulting set is definitely inexact + //! \hideinitializer Result is definitely inexact I_INEXACT = 32, - //! The operation has definitely changed the set + //! \hideinitializer Operation has definitely changed the set I_CHANGED = 64, - //! The operation has left the set definitely unchanged + //! \hideinitializer Operation has left the set definitely unchanged I_UNCHANGED = 128, - //! The operation is undefined for some combination of values + //! \hideinitializer Operation is undefined for some combination of values I_SINGULARITIES = 256 }; -inline I_Result operator|(I_Result a, I_Result b) { +inline I_Result +operator|(I_Result a, I_Result b) { return static_cast<I_Result>(static_cast<unsigned>(a) | static_cast<unsigned>(b)); } -inline I_Result operator&(I_Result a, I_Result b) { +inline I_Result +operator&(I_Result a, I_Result b) { return static_cast<I_Result>(static_cast<unsigned>(a) & static_cast<unsigned>(b)); } -inline I_Result operator-(I_Result a, I_Result b) { +inline I_Result +operator-(I_Result a, I_Result b) { return static_cast<I_Result>(static_cast<unsigned>(a) & ~static_cast<unsigned>(b)); } @@ -352,7 +361,9 @@ struct I_Constraint_Rel { template <typename T, typename Val_Or_Ref_Criteria = Use_Slow_Copy, bool extended = false> -class I_Constraint : public I_Constraint_Common<I_Constraint<T, Val_Or_Ref_Criteria, extended> > { +class I_Constraint + : public I_Constraint_Common<I_Constraint<T, Val_Or_Ref_Criteria, + extended> > { typedef Val_Or_Ref<T, Val_Or_Ref_Criteria> Val_Ref; typedef typename Val_Ref::Arg_Type Arg_Type; typedef typename Val_Ref::Return_Type Return_Type;

1 0

[GIT] ppl/ppl(master): Updated.
by Roberto Bagnara 25 Feb '12

25 Feb '12

Module: ppl/ppl Branch: master Commit: fcbdfeab44225f1b03243f11bd32e999828c0b4c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fcbdfeab4422… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Feb 25 17:06:00 2012 +0100 Updated. --- CREDITS | 60 +++++++++++++++++++++++++++--------------------------------- 1 files changed, 27 insertions(+), 33 deletions(-) diff --git a/CREDITS b/CREDITS index 7c799d7..a34375e 100644 --- a/CREDITS +++ b/CREDITS @@ -10,9 +10,10 @@ people: Core Development Team: ---------------------- - Roberto Bagnara [1] (University of Parma) - Patricia M. Hill [2] (University of Leeds) - Enea Zaffanella [3] (University of Parma) + Roberto Bagnara [1] (BUGSENG srl and University of Parma) + Patricia M. Hill [2] (BUGSENG srl and University of Leeds) + Enea Zaffanella [3] (BUGSENG srl and University of Parma) + Abramo Bagnara (BUGSENG srl) Former Members of the Core Development Team: @@ -28,21 +29,6 @@ Former Members of the Core Development Team: Current Contributors: --------------------- - Abramo Bagnara (Opera Unica) rewrote and generalized the - support for checked coefficients. He also - wrote the support for extended numbers and is - currently writing a new implementation of - intervals. He also helps on several other - design and implementation issues. - - Fabio Bossi (student of the University of Parma) - is working on the PPL support for the approximation - of floating point computations. - - Francois Galea [*] (University of Versailles) is working - at the implementation of the Parametric Integer - Programming solver. - Marco Poletti (student of the University of Bologna) implemented the sparse matrices that are used in the MIP and PIP solvers of the PPL; he also @@ -51,10 +37,7 @@ Current Contributors: on improving the PPL's memory footprint and on other improvements to the library. - Enric Rodriguez Carbonell [4] (Technical University of Catalonia) is - working on the implementation of polynomial spaces. - - Alessandro Zaccagnini [5] (University of Parma) has helped with + Alessandro Zaccagnini [4] (University of Parma) has helped with the efficient implementation of GCD and LCM for checked numbers. He is now working on the definitions of interval arithmetic operations. @@ -65,7 +48,7 @@ Current Contributors: Past Contributors: ------------------ - Roberto Amadini (student of the University of Parma) + Roberto Amadini (former student of the University of Parma) did some work on the PPL support for the approximation of floating point computations. @@ -79,6 +62,10 @@ Past Contributors: did some work on the PPL support for the approximation of floating point computations. + Fabio Bossi (former student of the University of Parma) + worked on the PPL support for the approximation + of floating point computations. + Danilo Bonardi (former student of the University of Parma) worked on a development branch where he experimented with the use of metaprogramming techniques @@ -96,7 +83,7 @@ Past Contributors: solver, and also most of the Java and OCaml interfaces. - Katy Dobson [6] (former student of the University of Leeds) + Katy Dobson (former student of the University of Leeds) worked on the formalization and definition of algorithms for rational grids and products of grids and polyhedra. @@ -105,6 +92,10 @@ Past Contributors: of the support for native and checked integer coefficients. + Francois Galea [5] (University of Versailles) worked + at the implementation of the Parametric Integer + Programming solver. + Maximiliano Marchesi (former student of the University of Parma) helped a little to improve the documentation for bounded differences. @@ -119,18 +110,22 @@ Past Contributors: with the generation of the library's documentation using Doxygen. - Matthew Mundell [7] (formerly at the University of Leeds) worked + Matthew Mundell [6] (formerly at the University of Leeds) worked on the implementation of rational grids. He has also helped on other implementation issues. - Andrea Pescetti (University of Parma) was one of the four students - with which the PPL project started. Later, he - helped a little with the library's documentation. + Andrea Pescetti (former student of the University of Parma) was one + of the four students with which the PPL + project started. Later, he helped a little + with the library's documentation. Barbara Quartieri (former student of the University of Parma) worked on our implementation of bounded differences and octagons. + Enric Rodriguez Carbonell [7] (Technical University of Catalonia) + worked at the implementation of polynomial spaces. + Angela Stazzone (former student of the University of Parma) worked on the library's documentation. @@ -369,11 +364,10 @@ projects and organizations: [1] http://www.cs.unipr.it/~bagnara/ [2] http://www.comp.leeds.ac.uk/hill/ [3] http://www.cs.unipr.it/~zaffanella/ - [*] http://www.prism.uvsq.fr/~fgalea/ - [4] http://www.lsi.upc.edu/~erodri/ - [5] http://www.math.unipr.it/~zaccagni/ - [6] http://www.comp.leeds.ac.uk/katyd/ - [7] http://www.mundell.ukfsn.org/ + [4] http://www.math.unipr.it/~zaccagni/ + [5] http://www.prism.uvsq.fr/~fgalea/ + [6] http://www.mundell.ukfsn.org/ + [7] http://www.lsi.upc.edu/~erodri/ [8] http://www.irisa.fr/lande/fbesson/fbesson.html [9] http://www.cs.ucsb.edu/~bultan/ [10] http://www.clip.dia.fi.upm.es/~boris/

1 0

[GIT] ppl/ppl(master): For code clarity purposes, better distinguish signed /unsigned operations.
by Enea Zaffanella 25 Feb '12

25 Feb '12

Module: ppl/ppl Branch: master Commit: 5ac71293891dbc160c066a80738a4bd27b93a450 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5ac71293891d… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Feb 25 16:12:58 2012 +0100 For code clarity purposes, better distinguish signed/unsigned operations. Detected by ECLAIR service utypflag. --- src/Bit_Row.cc | 6 ++++-- src/CO_Tree.cc | 9 +++++---- src/checked_float.inlines.hh | 19 +++++++++++-------- 3 files changed, 20 insertions(+), 14 deletions(-) diff --git a/src/Bit_Row.cc b/src/Bit_Row.cc index c303fae..d250197 100644 --- a/src/Bit_Row.cc +++ b/src/Bit_Row.cc @@ -55,7 +55,8 @@ PPL::Bit_Row::next(unsigned long position) const { // return (r == C_Integer<unsigned long>::max) ? -1 : r; // </CODE> - mp_size_t li = static_cast<mp_size_t>(position / PPL_BITS_PER_GMP_LIMB); + const unsigned long uli = position / PPL_BITS_PER_GMP_LIMB; + mp_size_t li = static_cast<mp_size_t>(uli); const mp_size_t vec_size = vec->_mp_size; PPL_ASSERT(vec_size >= 0); if (li >= vec_size) @@ -104,7 +105,8 @@ PPL::Bit_Row::prev(unsigned long position) const { const mp_size_t vec_size = vec->_mp_size; PPL_ASSERT(vec_size > 0); - mp_size_t li = static_cast<mp_size_t>(position / PPL_BITS_PER_GMP_LIMB); + const unsigned long uli = position / PPL_BITS_PER_GMP_LIMB; + mp_size_t li = static_cast<mp_size_t>(uli); mp_limb_t limb; mp_srcptr p = vec->_mp_d; diff --git a/src/CO_Tree.cc b/src/CO_Tree.cc index 4a70f04..0b388a1 100644 --- a/src/CO_Tree.cc +++ b/src/CO_Tree.cc @@ -893,8 +893,9 @@ PPL::CO_Tree --subtree_size; } - PPL_ASSERT(first_unused_index >= indexes); - return static_cast<dimension_type>(first_unused_index - indexes); + ptrdiff_t distance = first_unused_index - indexes; + PPL_ASSERT(distance >= 0); + return static_cast<dimension_type>(distance); } void @@ -907,8 +908,8 @@ PPL::CO_Tree::redistribute_elements_in_subtree( bool add_element) { // This is static and with static allocation, to improve performance. - // sizeof_to_bits(sizeof(dimension_type)) is the maximum k such that 2^k-1 is a - // dimension_type, so it is the maximum tree height. + // sizeof_to_bits(sizeof(dimension_type)) is the maximum k such that + // 2^k-1 is a dimension_type, so it is the maximum tree height. // For each node level, the stack may contain up to two element (one for the // subtree rooted at the right son of a node of that level, and one for the // node itself). An additional element can be at the top of the tree. diff --git a/src/checked_float.inlines.hh b/src/checked_float.inlines.hh index 79166c0..08b7251 100644 --- a/src/checked_float.inlines.hh +++ b/src/checked_float.inlines.hh @@ -885,14 +885,17 @@ assign_float_mpq(T& to, const mpq_class& from, Rounding_Dir dir) { - exponent); mpz_t mantissa; mpz_init(mantissa); - long shift = static_cast<long>(needed_bits) - exponent; - if (shift > 0) { - mpz_mul_2exp(mantissa, numer_z, static_cast<unsigned long>(shift)); - numer_z = mantissa; - } - else if (shift < 0) { - mpz_mul_2exp(mantissa, denom_z, static_cast<unsigned long>(-shift)); - denom_z = mantissa; + { + long shift = static_cast<long>(needed_bits) - exponent; + if (shift > 0) { + mpz_mul_2exp(mantissa, numer_z, static_cast<unsigned long>(shift)); + numer_z = mantissa; + } + else if (shift < 0) { + shift = -shift; + mpz_mul_2exp(mantissa, denom_z, static_cast<unsigned long>(shift)); + denom_z = mantissa; + } } mpz_t r; mpz_init(r);

1 0

[GIT] ppl/ppl(master): Exploit new helper function least_significant_one_mask(),
by Enea Zaffanella 25 Feb '12

25 Feb '12

Module: ppl/ppl Branch: master Commit: 73aee8ff7b811416d25b4c54344fbaa214ea7804 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=73aee8ff7b81… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Feb 25 16:11:07 2012 +0100 Exploit new helper function least_significant_one_mask(), thereby avoiding unary minus on unsigned integer values. Detected by ECLAIR service utypflag. --- src/CO_Tree.inlines.hh | 19 ++++++++++--------- 1 files changed, 10 insertions(+), 9 deletions(-) diff --git a/src/CO_Tree.inlines.hh b/src/CO_Tree.inlines.hh index ece7ab0..0032029 100644 --- a/src/CO_Tree.inlines.hh +++ b/src/CO_Tree.inlines.hh @@ -679,7 +679,7 @@ CO_Tree::tree_iterator::tree_iterator(CO_Tree& tree1, dimension_type i1) PPL_ASSERT(tree.reserved_size != 0); PPL_ASSERT(i1 <= tree.reserved_size + 1); i = i1; - offset = i & -i; + offset = least_significant_one_mask(i); PPL_ASSERT(OK()); } @@ -703,9 +703,7 @@ inline CO_Tree::tree_iterator& CO_Tree::tree_iterator::operator=(const iterator& itr) { PPL_ASSERT(itr != tree.end()); i = tree.dfs_index(itr); - offset = i; - // This assumes two's complement encoding. - offset &= -i; + offset = least_significant_one_mask(i); return *this; } @@ -762,9 +760,10 @@ CO_Tree::tree_iterator::follow_left_children_with_value() { p -= (offset - 1); while (*p == unused_index) ++p; - PPL_ASSERT(p >= tree.indexes); - i = static_cast<dimension_type>(p - tree.indexes); - offset = i & -i; + ptrdiff_t distance = p - tree.indexes; + PPL_ASSERT(distance >= 0); + i = static_cast<dimension_type>(distance); + offset = least_significant_one_mask(i); PPL_ASSERT(OK()); } @@ -776,8 +775,10 @@ CO_Tree::tree_iterator::follow_right_children_with_value() { p += (offset - 1); while (*p == unused_index) --p; - i = static_cast<dimension_type>(p - tree.indexes); - offset = i & -i; + ptrdiff_t distance = p - tree.indexes; + PPL_ASSERT(distance >= 0); + i = static_cast<dimension_type>(distance); + offset = least_significant_one_mask(i); PPL_ASSERT(OK()); }

1 0

[GIT] ppl/ppl(master): Added helper function least_significant_one_mask().
by Enea Zaffanella 25 Feb '12

25 Feb '12

Module: ppl/ppl Branch: master Commit: 015e50d0dfee5724c26b989121c15e79b92b8059 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=015e50d0dfee… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Feb 25 16:08:48 2012 +0100 Added helper function least_significant_one_mask(). --- src/globals.defs.hh | 3 +++ src/globals.inlines.hh | 8 +++++++- 2 files changed, 10 insertions(+), 1 deletions(-) diff --git a/src/globals.defs.hh b/src/globals.defs.hh index 2c54772..a7e46a3 100644 --- a/src/globals.defs.hh +++ b/src/globals.defs.hh @@ -497,6 +497,9 @@ template <typename RA_Container> typename RA_Container::const_iterator nth_iter(const RA_Container& cont, dimension_type n); +dimension_type +least_significant_one_mask(dimension_type i); + } // namespace Parma_Polyhedra_Library // By default, use sparse matrices both for MIP_Problem and PIP_Problem. diff --git a/src/globals.inlines.hh b/src/globals.inlines.hh index d176bb0..0d27ddb 100644 --- a/src/globals.inlines.hh +++ b/src/globals.inlines.hh @@ -39,7 +39,8 @@ not_a_dimension() { inline int32_t hash_code_from_dimension(dimension_type dim) { const dimension_type divisor = 1U << (32 - 1); - return static_cast<int32_t>(dim % divisor); + dim = dim % divisor; + return static_cast<int32_t>(dim); } inline const Weightwatch_Traits::Threshold& @@ -142,6 +143,11 @@ nth_iter(const RA_Container& cont, dimension_type n) { return cont.begin() + static_cast<diff_t>(n); } +inline dimension_type +least_significant_one_mask(const dimension_type i) { + return i & (~i + 1U); +} + } // namespace Parma_Polyhedra_Library #endif // !defined(PPL_globals_inlines_hh)

1 0

[GIT] ppl/ppl(master): Prefer explicit test against zero.
by Enea Zaffanella 25 Feb '12

25 Feb '12

Module: ppl/ppl Branch: master Commit: 02eb888f14e01881c56274ed8009d6c5aa3d8e41 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=02eb888f14e0… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Feb 25 13:34:55 2012 +0100 Prefer explicit test against zero. Detected by ECLAIR service utypflag. --- interfaces/C/ppl_interface_generator_c_cc_code.m4 | 3 ++- 1 files changed, 2 insertions(+), 1 deletions(-) diff --git a/interfaces/C/ppl_interface_generator_c_cc_code.m4 b/interfaces/C/ppl_interface_generator_c_cc_code.m4 index 43d971e..87d446d 100644 --- a/interfaces/C/ppl_interface_generator_c_cc_code.m4 +++ b/interfaces/C/ppl_interface_generator_c_cc_code.m4 @@ -41,7 +41,8 @@ ppl_new_@TOPOLOGY@@CLASS@_from_space_dimension (ppl_@CLASS@_t* pph, ppl_dimension_type d, int empty) try { - *pph = to_nonconst(new @TOPOLOGY@@CPP_CLASS@(d, empty ? EMPTY : UNIVERSE)); + Degenerate_Element e = (empty != 0) ? EMPTY : UNIVERSE; + *pph = to_nonconst(new @TOPOLOGY@@CPP_CLASS@(d, e)); return 0; } CATCH_ALL

1 0

[GIT] ppl/ppl(master): Prefer explicit test against zero.
by Enea Zaffanella 25 Feb '12

25 Feb '12

Module: ppl/ppl Branch: master Commit: ce56ec42203672a969d24b819854e48a8ec60985 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ce56ec422036… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Feb 25 12:54:34 2012 +0100 Prefer explicit test against zero. Detected by ECLAIR service utypflag. --- demos/ppl_lcdd/ppl_lcdd.cc | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/demos/ppl_lcdd/ppl_lcdd.cc b/demos/ppl_lcdd/ppl_lcdd.cc index d6f1b8e..e30de0e 100644 --- a/demos/ppl_lcdd/ppl_lcdd.cc +++ b/demos/ppl_lcdd/ppl_lcdd.cc @@ -241,7 +241,7 @@ set_input(const char* file_name) { std::istream& input() { - assert(input_stream_p); + assert(input_stream_p != 0); return *input_stream_p; } @@ -269,7 +269,7 @@ set_output(const char* file_name) { std::ostream& output() { - assert(output_stream_p); + assert(output_stream_p != 0); return *output_stream_p; }

1 0

[GIT] ppl/ppl(master): Reduced the scope of variable declarations.
by Roberto Bagnara 25 Feb '12

25 Feb '12

Module: ppl/ppl Branch: master Commit: b52dea04e8d347087359c175ed5c7d963ed3c8e2 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b52dea04e8d3… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Feb 25 12:37:53 2012 +0100 Reduced the scope of variable declarations. Detected by ECLAIR service minscope. --- ...lication_Floating_Point_Expression.templates.hh | 11 ++++++----- src/linearize.hh | 11 ++++++----- 2 files changed, 12 insertions(+), 10 deletions(-) diff --git a/src/Multiplication_Floating_Point_Expression.templates.hh b/src/Multiplication_Floating_Point_Expression.templates.hh index b9c84bd..e182317 100644 --- a/src/Multiplication_Floating_Point_Expression.templates.hh +++ b/src/Multiplication_Floating_Point_Expression.templates.hh @@ -60,15 +60,16 @@ bool Multiplication_Floating_Point_Expression<FP_Interval_Type, FP_Format> FP_Interval_Type intervalized_second_operand; this->intervalize(linearized_second_operand, int_store, intervalized_second_operand); - boundary_type first_interval_size, second_interval_size; // FIXME: we are not sure that what we do here is policy-proof. if (intervalized_first_operand.is_bounded()) { if (intervalized_second_operand.is_bounded()) { - first_interval_size = intervalized_first_operand.upper() - - intervalized_first_operand.lower(); - second_interval_size = intervalized_second_operand.upper() - - intervalized_second_operand.lower(); + boundary_type first_interval_size + = intervalized_first_operand.upper() + - intervalized_first_operand.lower(); + boundary_type second_interval_size + = intervalized_second_operand.upper() + - intervalized_second_operand.lower(); if (first_interval_size <= second_interval_size) intervalize_first = true; else diff --git a/src/linearize.hh b/src/linearize.hh index fff09d3..e5ac48a 100644 --- a/src/linearize.hh +++ b/src/linearize.hh @@ -380,15 +380,16 @@ mul_linearize(const Binary_Operator<Target>& bop_expr, if (!linearized_second_operand.intervalize(oracle, intervalized_second_operand)) return false; - analyzer_format first_interval_size, second_interval_size; // FIXME: we are not sure that what we do here is policy-proof. if (intervalized_first_operand.is_bounded()) { if (intervalized_second_operand.is_bounded()) { - first_interval_size = intervalized_first_operand.upper() - - intervalized_first_operand.lower(); - second_interval_size = intervalized_second_operand.upper() - - intervalized_second_operand.lower(); + analyzer_format first_interval_size + = intervalized_first_operand.upper() + - intervalized_first_operand.lower(); + analyzer_format second_interval_size + = intervalized_second_operand.upper() + - intervalized_second_operand.lower(); if (first_interval_size <= second_interval_size) intervalize_first = true; else

1 0