- PPL-devel - BUGSENG Mailman

[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

Re: [PPL-devel] Problems installing PPL on Mac OS X Lion
by Roberto Bagnara 25 Feb '12

25 Feb '12

On 02/25/12 08:05, Jan Gustafsson wrote: > Hi! > > We had contact a few weeks ago when I (in vain) tried to install PPL > on Mac OS X 10.5.8. You recommended me to move to Lion which I have > done. Now installation of PPL comes a bit longer, but not all the > way. I get the following error message during linking in make: > > ld: illegal text-relocation to ___gmp_binvert_limb_table in > /usr/local/lib/libgmp.a(mp_minv_tab.o) from ___gmpn_divexact_1 in > /usr/local/lib/libgmp.a(dive_1.o) for architecture x86_64 > > Any advice? > > Kind regards > > Jan G [CC to the ppl-devel mailing list so as to reach other Mac OS X users.] Hi Jan, it looks like a problem with /usr/local/lib/libgmp.a that is unrelated to the PPL. Is /usr/local/lib/libgmp.a something you have compiled yourself with the same toolchain you are using for the PPL? Can it be the result of some previous experiment that now gets in the way? Otherwise I don't know: perhaps Mac OS X users on the ppl-devel list can provide advice. All the best, 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

3 2

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

25 Feb '12

Module: ppl/ppl Branch: master Commit: 4ddf6ce187e9217e560fb3e8d18b315fa28d6d92 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4ddf6ce187e9… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Feb 25 12:18:10 2012 +0100 Prefer explicit tests against zero. Detected by ECLAIR service utypflag. --- src/c_streambuf.cc | 2 +- src/stdiobuf.cc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/c_streambuf.cc b/src/c_streambuf.cc index c76ca44..fdd630f 100644 --- a/src/c_streambuf.cc +++ b/src/c_streambuf.cc @@ -89,7 +89,7 @@ c_streambuf::int_type c_streambuf::overflow(int_type c) { const int_type eof = traits_type::eof(); if (traits_type::eq_int_type(c, eof)) - return sync() ? eof : traits_type::not_eof(c); + return (sync() != 0) ? eof : traits_type::not_eof(c); else { char buf = static_cast<char>(c); if (cb_write(&buf, 1) == 1) diff --git a/src/stdiobuf.cc b/src/stdiobuf.cc index 8a5fe95..a10a7ed 100644 --- a/src/stdiobuf.cc +++ b/src/stdiobuf.cc @@ -71,7 +71,7 @@ stdiobuf::int_type stdiobuf::overflow(int_type c) { const int_type eof = traits_type::eof(); if (traits_type::eq_int_type(c, eof)) - return fflush(fp) ? eof : traits_type::not_eof(c); + return (fflush(fp) != 0) ? eof : traits_type::not_eof(c); else return putc(c, fp); }

1 0

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

25 Feb '12

Module: ppl/ppl Branch: master Commit: 1ea98773b74de31caebd07558ec8b215d8298c6b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1ea98773b74d… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Feb 25 11:33:08 2012 +0100 Prefer explicit tests against zero. Detected by ECLAIR service utypflag. --- src/PIP_Problem.cc | 4 ++-- src/PIP_Tree.cc | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/PIP_Problem.cc b/src/PIP_Problem.cc index 9c82202..6c52d69 100644 --- a/src/PIP_Problem.cc +++ b/src/PIP_Problem.cc @@ -232,10 +232,10 @@ PPL::PIP_Problem::solve() const { external_space_dim, /*indent_level=*/ 0); // Update problem status. - x.status = (x.current_solution) ? OPTIMIZED : UNSATISFIABLE; + x.status = (x.current_solution != 0) ? OPTIMIZED : UNSATISFIABLE; PPL_ASSERT(OK()); - return (x.current_solution) + return (x.current_solution != 0) ? OPTIMIZED_PIP_PROBLEM : UNFEASIBLE_PIP_PROBLEM; } // End of handler for PARTIALLY_SATISFIABLE case. diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 76b5a0d..4f2e82e 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -3574,7 +3574,7 @@ PIP_Solution_Node::print_tree(std::ostream& s, const int indent, const Linear_Expression& PIP_Solution_Node::parametric_values(const Variable var) const { const PIP_Problem* pip = get_owner(); - PPL_ASSERT(pip); + PPL_ASSERT(pip != 0); const dimension_type space_dim = pip->space_dimension(); if (var.space_dimension() > space_dim) { @@ -3613,7 +3613,7 @@ PIP_Solution_Node::update_solution() const { return; const PIP_Problem* pip = get_owner(); - PPL_ASSERT(pip); + PPL_ASSERT(pip != 0); std::vector<bool> pip_dim_is_param(pip->space_dimension()); const Variables_Set& params = pip->parameter_space_dimensions(); for (Variables_Set::const_iterator p = params.begin(),

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: 7b7ae1196e04b62461a77d98086479fad8712bc7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7b7ae1196e04… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Feb 25 11:17:06 2012 +0100 Prefer explicit test against zero. Detected by ECLAIR service utypflag. --- src/checked_mpz.inlines.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/checked_mpz.inlines.hh b/src/checked_mpz.inlines.hh index 9b2c324..9b795d4 100644 --- a/src/checked_mpz.inlines.hh +++ b/src/checked_mpz.inlines.hh @@ -499,7 +499,7 @@ div_2exp_mpz(mpz_class& to, const mpz_class& x, unsigned int exp, PPL_ASSERT(round_up(dir)); mpz_cdiv_q_2exp(to.get_mpz_t(), n, exp); if (round_strict_relation(dir)) - return mpz_divisible_2exp_p(n, exp) ? V_EQ : V_LT; + return (mpz_divisible_2exp_p(n, exp) != 0) ? V_EQ : V_LT; return V_LE; } }

1 0

[GIT] ppl/ppl(master): Fixed a few misuses of assignment ( instead of comparison) in assertions.
by Enea Zaffanella 25 Feb '12

25 Feb '12

Module: ppl/ppl Branch: master Commit: 5e705a68649d84a32490ae8692158d19706cad2c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5e705a68649d… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Feb 25 11:10:45 2012 +0100 Fixed a few misuses of assignment (instead of comparison) in assertions. Detected by ECLAIR service utypflag. --- src/Dense_Row.inlines.hh | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Dense_Row.inlines.hh b/src/Dense_Row.inlines.hh index 00d78d2..17b808f 100644 --- a/src/Dense_Row.inlines.hh +++ b/src/Dense_Row.inlines.hh @@ -100,7 +100,7 @@ Dense_Row::Dense_Row(const dimension_type sz, resize(sz, capacity); PPL_ASSERT(size() == sz); - PPL_ASSERT(impl.capacity = capacity); + PPL_ASSERT(impl.capacity == capacity); PPL_ASSERT(OK()); } @@ -155,7 +155,7 @@ Dense_Row::Dense_Row(const Dense_Row& y, } PPL_ASSERT(size() == y.size()); - PPL_ASSERT(impl.capacity = capacity); + PPL_ASSERT(impl.capacity == capacity); PPL_ASSERT(OK()); } @@ -185,7 +185,7 @@ Dense_Row::Dense_Row(const Dense_Row& y, } PPL_ASSERT(size() == sz); - PPL_ASSERT(impl.capacity = capacity); + PPL_ASSERT(impl.capacity == capacity); PPL_ASSERT(OK()); }

1 0