- PPL-devel - BUGSENG Mailman

To represent z->Empty and w->Universe.
by Zell 24 Aug '12

24 Aug '12

Hello, I still have a superficial question. Consider the domain D:= Var-> Interval, where "Interval" contains two special intervals, " Empty " and " Universe " . I am now using Int_64 from PPL to model this domain. However I feel confused when I need to represent elements that " mixes the 'Empty' and 'Universe' " . One such element is, { x->[3,5], y->[4,7], z->empty, w->universe}. I find that, whenever a constraint like "z->empty" is added to a constraints_system, the constraints_system becomes "false". This seems reasonable because the constraint_system in PPL models a conjunction of constraints and thus one constraint is false make the whole constraint system unsatisfiable. However, I do not see how to represent elements like the one given above that mixes 'z->Empty' and 'w->Universe' . ( I would like to use 'z->empty' to mean 'z is not yet initialized', and 'w->universe' to mean that 'w is unknown' .) I probably misunderstand something basic here. What do you think? Thanks. Zell. p.s Due to the help of Enea and Roberto, I am not able to use PPL in my analysis. I really appreciate your help!!! By the way, I have been using the pseudo name "Zell" because I used to write my name as "Zell". For information, my passport name is "Zhoulai", which can be more or less pronounced as "zell".

2 4

[GIT] ppl/ppl(master): Avoided some "magic constants".
by Roberto Bagnara 22 Aug '12

22 Aug '12

Module: ppl/ppl Branch: master Commit: 55575dcac0fa329b196684941eded7123e3c34ff URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=55575dcac0fa… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 22 16:30:51 2012 +0200 Avoided some "magic constants". Detected by ECLAIR service nomagicc. --- src/Float.cc | 1 + src/Float_defs.hh | 6 ++++++ src/Float_inlines.hh | 18 +++++++++--------- 3 files changed, 16 insertions(+), 9 deletions(-) diff --git a/src/Float.cc b/src/Float.cc index e79c04f..d20d5da 100644 --- a/src/Float.cc +++ b/src/Float.cc @@ -38,6 +38,7 @@ const uint64_t float_ieee754_quad::MSP_POS_ZERO; const uint64_t float_ieee754_quad::MSP_NEG_ZERO; const uint64_t float_ieee754_quad::LSP_INF; const uint64_t float_ieee754_quad::LSP_ZERO; +const uint64_t float_ieee754_quad::MSP_MAX; const uint64_t float_ieee754_quad::LSP_MAX; } // Parma_Polyhedra_Library diff --git a/src/Float_defs.hh b/src/Float_defs.hh index 1def00d..3b1060e 100644 --- a/src/Float_defs.hh +++ b/src/Float_defs.hh @@ -51,6 +51,7 @@ struct float_ieee754_half { uint16_t word; static const uint16_t SGN_MASK = 0x8000U; static const uint16_t EXP_MASK = 0xfc00U; + static const uint16_t WRD_MAX = 0x7bffU; static const uint16_t POS_INF = 0x7c00U; static const uint16_t NEG_INF = 0xfc00U; static const uint16_t POS_ZERO = 0x0000U; @@ -83,6 +84,7 @@ struct float_ieee754_single { uint32_t word; static const uint32_t SGN_MASK = 0x80000000U; static const uint32_t EXP_MASK = 0x7f800000U; + static const uint32_t WRD_MAX = 0x7f7fffffU; static const uint32_t POS_INF = 0x7f800000U; static const uint32_t NEG_INF = 0xff800000U; static const uint32_t POS_ZERO = 0x00000000U; @@ -131,6 +133,7 @@ struct float_ieee754_double { static const uint32_t MSP_NEG_ZERO = 0x80000000U; static const uint32_t LSP_INF = 0; static const uint32_t LSP_ZERO = 0; + static const uint32_t MSP_MAX = 0x7fefffffU; static const uint32_t LSP_MAX = 0xffffffffU; static const unsigned int BASE = 2; static const unsigned int EXPONENT_BITS = 11; @@ -159,6 +162,7 @@ struct float_ibm_single { uint32_t word; static const uint32_t SGN_MASK = 0x80000000U; static const uint32_t EXP_MASK = 0x7f000000U; + static const uint32_t WRD_MAX = 0x7fffffffU; static const uint32_t POS_INF = 0x7f000000U; static const uint32_t NEG_INF = 0xff000000U; static const uint32_t POS_ZERO = 0x00000000U; @@ -211,6 +215,7 @@ struct float_intel_double_extended { static const uint32_t MSP_NEG_ZERO = 0x00008000U; static const uint64_t LSP_INF = static_cast<uint64_t>(0x8000000000000000ULL); static const uint64_t LSP_ZERO = 0; + static const uint32_t MSP_MAX = 0x00007ffeU; static const uint64_t LSP_DMAX = static_cast<uint64_t>(0x7fffffffffffffffULL); static const uint64_t LSP_NMAX = static_cast<uint64_t>(0xffffffffffffffffULL); static const unsigned int BASE = 2; @@ -252,6 +257,7 @@ struct float_ieee754_quad { static const uint64_t MSP_NEG_ZERO = static_cast<uint64_t>(0x8000000000000000ULL); static const uint64_t LSP_INF = 0; static const uint64_t LSP_ZERO = 0; + static const uint64_t MSP_MAX = static_cast<uint64_t>(0x7ffeffffffffffffULL); static const uint64_t LSP_MAX = static_cast<uint64_t>(0xffffffffffffffffULL); static const unsigned int BASE = 2; static const unsigned int EXPONENT_BITS = 15; diff --git a/src/Float_inlines.hh b/src/Float_inlines.hh index 50670de..47ae609 100644 --- a/src/Float_inlines.hh +++ b/src/Float_inlines.hh @@ -75,7 +75,7 @@ float_ieee754_half::inc() { inline void float_ieee754_half::set_max(bool negative) { - word = 0x7bffU; + word = WRD_MAX; if (negative) word |= SGN_MASK; } @@ -136,7 +136,7 @@ float_ieee754_single::inc() { inline void float_ieee754_single::set_max(bool negative) { - word = 0x7f7fffffU; + word = WRD_MAX; if (negative) word |= SGN_MASK; } @@ -212,8 +212,8 @@ float_ieee754_double::inc() { inline void float_ieee754_double::set_max(bool negative) { - msp = 0x7fefffffU; - lsp = 0xffffffffU; + msp = MSP_MAX; + lsp = LSP_MAX; if (negative) msp |= MSP_SGN_MASK; } @@ -283,7 +283,7 @@ float_ibm_single::inc() { inline void float_ibm_single::set_max(bool negative) { - word = 0x7f000000U; + word = WRD_MAX; if (negative) word |= SGN_MASK; } @@ -361,8 +361,8 @@ float_intel_double_extended::inc() { inline void float_intel_double_extended::set_max(bool negative) { - msp = 0x00007ffeU; - lsp = static_cast<uint64_t>(0xffffffffffffffffULL); + msp = MSP_MAX; + lsp = LSP_NMAX; if (negative) msp |= MSP_SGN_MASK; } @@ -441,8 +441,8 @@ float_ieee754_quad::inc() { inline void float_ieee754_quad::set_max(bool negative) { - msp = static_cast<uint64_t>(0x7ffeffffffffffffULL); - lsp = static_cast<uint64_t>(0xffffffffffffffffULL); + msp = MSP_MAX; + lsp = LSP_MAX; if (negative) msp |= MSP_SGN_MASK; }

1 0

[GIT] ppl/ppl(master): Fixed float_ieee754_half:: POS_INF and float_ieee754_half::NEG_INF.
by Roberto Bagnara 22 Aug '12

22 Aug '12

Module: ppl/ppl Branch: master Commit: 004c134532a33753997d6a2a5a4b9f8a09ff4622 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=004c134532a3… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 22 15:45:11 2012 +0200 Fixed float_ieee754_half::POS_INF and float_ieee754_half::NEG_INF. They were swapped. --- src/Float_defs.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Float_defs.hh b/src/Float_defs.hh index 3a4188f..1def00d 100644 --- a/src/Float_defs.hh +++ b/src/Float_defs.hh @@ -51,8 +51,8 @@ struct float_ieee754_half { uint16_t word; static const uint16_t SGN_MASK = 0x8000U; static const uint16_t EXP_MASK = 0xfc00U; - static const uint16_t POS_INF = 0xfc00U; - static const uint16_t NEG_INF = 0x7c00U; + static const uint16_t POS_INF = 0x7c00U; + static const uint16_t NEG_INF = 0xfc00U; static const uint16_t POS_ZERO = 0x0000U; static const uint16_t NEG_ZERO = 0x8000U; static const unsigned int BASE = 2;

1 0

[GIT] ppl/ppl(ppl-1_0-branch): New commits
by Roberto Bagnara 22 Aug '12

22 Aug '12

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=da09734808a5… Merge: 1c2978601db3e2701a4de1da80986c3ed84bad3e 490e191f4f9d54f21ff080a52ff61e7bbb4383fe Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 22 08:37:11 2012 +0200 Merge branch 'master' into ppl-1_0-branch URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=490e191f4f9d… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 22 08:36:18 2012 +0200 Revert "Two comments turned into assertions." This reverts commit e4ced22bfaf9e410719d47154dcc942ceffbeea0. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=364dfbeafba1… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Aug 21 21:05:46 2012 +0200 Avoided a couple of "magic constants". Detected by ECLAIR service nomagicc. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=88fdc38a0e2e… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Aug 21 17:16:24 2012 +0200 Comments should never be used for "commenting out" code. Detected by ECLAIR service cmntdout. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=56f7bba205d5… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Aug 21 17:15:06 2012 +0200 Unusual and difficult-to-maintain comment removed. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e4ced22bfaf9… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Aug 20 22:29:26 2012 +0200 Two comments turned into assertions. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=82085ae7fc21… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Aug 20 21:33:27 2012 +0200 Do not declare more than one variable per declaration. Detected by ECLAIR service declgrup_srceline. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d75793538dc6… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Aug 20 16:51:41 2012 +0200 Avoided non-constant pointers to function. Detected by ECLAIR service funpntr. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=eb5a736c101e… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Aug 20 16:27:50 2012 +0200 Avoided non-constant pointers to function. Detected by ECLAIR service funpntr. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b23873fe14a7… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Aug 20 15:49:20 2012 +0200 Avoided non-constant pointers to function. Detected by ECLAIR service funpntr.

1 0

[GIT] ppl/ppl(master): Revert "Two comments turned into assertions."
by Roberto Bagnara 22 Aug '12

22 Aug '12

Module: ppl/ppl Branch: master Commit: 490e191f4f9d54f21ff080a52ff61e7bbb4383fe URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=490e191f4f9d… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 22 08:36:18 2012 +0200 Revert "Two comments turned into assertions." This reverts commit e4ced22bfaf9e410719d47154dcc942ceffbeea0. --- src/wrap_assign.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/wrap_assign.hh b/src/wrap_assign.hh index acc6b5e..fb8b2c1 100644 --- a/src/wrap_assign.hh +++ b/src/wrap_assign.hh @@ -153,11 +153,11 @@ wrap_assign(PSET& pointset, const unsigned complexity_threshold, const bool wrap_individually, const char* class_name) { - PPL_ASSERT(vars.space_dimension() <= pointset.space_dimension()); + // We must have cs_p->space_dimension() <= vars.space_dimension() + // and vars.space_dimension() <= pointset.space_dimension(). // Dimension-compatibility check of `*cs_p', if any. if (cs_p != 0) { - PPL_ASSERT(cs_p->space_dimension() <= vars.space_dimension()); const dimension_type vars_space_dim = vars.space_dimension(); if (cs_p->space_dimension() > vars_space_dim) { std::ostringstream s;

1 0

[GIT] ppl/ppl(master): Avoided a couple of "magic constants".
by Roberto Bagnara 21 Aug '12

21 Aug '12

Module: ppl/ppl Branch: master Commit: 364dfbeafba14774884ce7d84373785d01f43d46 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=364dfbeafba1… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Aug 21 21:05:46 2012 +0200 Avoided a couple of "magic constants". Detected by ECLAIR service nomagicc. --- src/Float_inlines.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Float_inlines.hh b/src/Float_inlines.hh index 9c0f735..50670de 100644 --- a/src/Float_inlines.hh +++ b/src/Float_inlines.hh @@ -371,7 +371,7 @@ inline void float_intel_double_extended::build(bool negative, mpz_t mantissa, int exponent) { #if ULONG_MAX == 0xffffffffUL - mpz_export(&lsp, 0, -1, 8, 0, 0, mantissa); + mpz_export(&lsp, 0, -1, sizeof(lsp), 0, 0, mantissa); #else lsp = mpz_get_ui(mantissa); #endif @@ -450,7 +450,7 @@ float_ieee754_quad::set_max(bool negative) { inline void float_ieee754_quad::build(bool negative, mpz_t mantissa, int exponent) { uint64_t parts[2]; - mpz_export(parts, 0, -1, 8, 0, 0, mantissa); + mpz_export(parts, 0, -1, sizeof(parts[0]), 0, 0, mantissa); lsp = parts[0]; msp = parts[1]; msp &= ((static_cast<uint64_t>(1) << (MANTISSA_BITS - 64)) - 1);

1 0

[GIT] ppl/ppl(master): Comments should never be used for "commenting out" code.
by Roberto Bagnara 21 Aug '12

21 Aug '12

Module: ppl/ppl Branch: master Commit: 88fdc38a0e2e9d49fc8c1940705302d22cb790ee URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=88fdc38a0e2e… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Aug 21 17:16:24 2012 +0200 Comments should never be used for "commenting out" code. Detected by ECLAIR service cmntdout. --- src/Boundary_defs.hh | 10 ---------- 1 files changed, 0 insertions(+), 10 deletions(-) diff --git a/src/Boundary_defs.hh b/src/Boundary_defs.hh index 894abf2..6d4c023 100644 --- a/src/Boundary_defs.hh +++ b/src/Boundary_defs.hh @@ -116,11 +116,6 @@ set_unbounded(Boundary_Type type, T& x, Info& info) { template <typename T, typename Info> inline Result set_minus_infinity(Boundary_Type type, T& x, Info& info, bool open = false) { - /* - PPL_COMPILE_TIME_CHECK(Info::store_special - || std::numeric_limits<T>::has_infinity, - "minus infinity is not representable"); - */ if (open) { PPL_ASSERT(type == LOWER); } @@ -144,11 +139,6 @@ set_minus_infinity(Boundary_Type type, T& x, Info& info, bool open = false) { template <typename T, typename Info> inline Result set_plus_infinity(Boundary_Type type, T& x, Info& info, bool open = false) { - /* - PPL_COMPILE_TIME_CHECK(Info::store_special - || std::numeric_limits<T>::has_infinity, - "minus infinity is not representable"); - */ if (open) { PPL_ASSERT(type == UPPER); }

1 0

[GIT] ppl/ppl(master): Unusual and difficult-to-maintain comment removed.
by Roberto Bagnara 21 Aug '12

21 Aug '12

Module: ppl/ppl Branch: master Commit: 56f7bba205d5941ac03bdf0d5fb211d3db334419 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=56f7bba205d5… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Aug 21 17:15:06 2012 +0200 Unusual and difficult-to-maintain comment removed. --- src/Grid_simplify.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/Grid_simplify.cc b/src/Grid_simplify.cc index a7e20c7..4a0a515 100644 --- a/src/Grid_simplify.cc +++ b/src/Grid_simplify.cc @@ -467,7 +467,7 @@ Grid::simplify(Congruence_System& cgs, Dimension_Kinds& dim_kinds) { ++pivot_index; } - } // end for (dimension_type dim = num_columns; dim-- > 0; ) + } if (pivot_index > 0) { // If the last row is false then make it the equality 1 = 0, and

1 0

[GIT] ppl/ppl(master): Two comments turned into assertions.
by Roberto Bagnara 20 Aug '12

20 Aug '12

Module: ppl/ppl Branch: master Commit: e4ced22bfaf9e410719d47154dcc942ceffbeea0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e4ced22bfaf9… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Aug 20 22:29:26 2012 +0200 Two comments turned into assertions. --- src/wrap_assign.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/wrap_assign.hh b/src/wrap_assign.hh index fb8b2c1..acc6b5e 100644 --- a/src/wrap_assign.hh +++ b/src/wrap_assign.hh @@ -153,11 +153,11 @@ wrap_assign(PSET& pointset, const unsigned complexity_threshold, const bool wrap_individually, const char* class_name) { - // We must have cs_p->space_dimension() <= vars.space_dimension() - // and vars.space_dimension() <= pointset.space_dimension(). + PPL_ASSERT(vars.space_dimension() <= pointset.space_dimension()); // Dimension-compatibility check of `*cs_p', if any. if (cs_p != 0) { + PPL_ASSERT(cs_p->space_dimension() <= vars.space_dimension()); const dimension_type vars_space_dim = vars.space_dimension(); if (cs_p->space_dimension() > vars_space_dim) { std::ostringstream s;

1 0

[GIT] ppl/ppl(master): Do not declare more than one variable per declaration.
by Roberto Bagnara 20 Aug '12

20 Aug '12

Module: ppl/ppl Branch: master Commit: 82085ae7fc2115e6218ce723cbc93ec4f07361b9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=82085ae7fc21… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Aug 20 21:33:27 2012 +0200 Do not declare more than one variable per declaration. Detected by ECLAIR service declgrup_srceline. --- src/Box_templates.hh | 8 ++++++-- src/Grid_conversion.cc | 3 ++- src/Interval_defs.hh | 3 ++- src/Interval_inlines.hh | 27 ++++++++++++++++++--------- src/Pointset_Powerset_templates.hh | 9 ++++----- 5 files changed, 32 insertions(+), 18 deletions(-) diff --git a/src/Box_templates.hh b/src/Box_templates.hh index ad1e8e0..b1061b9 100644 --- a/src/Box_templates.hh +++ b/src/Box_templates.hh @@ -2801,7 +2801,9 @@ Box<ITV>::affine_image(const Variable var, if (is_empty()) return; - Tmp_Interval_Type expr_value, temp0, temp1; + Tmp_Interval_Type expr_value; + Tmp_Interval_Type temp0; + Tmp_Interval_Type temp1; expr_value.assign(expr.inhomogeneous_term()); for (Linear_Expression::const_iterator i = expr.begin(), i_end = expr.end(); i != i_end; ++i) { @@ -2881,7 +2883,9 @@ Box<ITV>::affine_preimage(const Variable var, const Coefficient& expr_v = expr.coefficient(var); const bool invertible = (expr_v != 0); if (!invertible) { - Tmp_Interval_Type expr_value, temp0, temp1; + Tmp_Interval_Type expr_value; + Tmp_Interval_Type temp0; + Tmp_Interval_Type temp1; expr_value.assign(expr.inhomogeneous_term()); for (Linear_Expression::const_iterator i = expr.begin(), i_end = expr.end(); i != i_end; ++i) { diff --git a/src/Grid_conversion.cc b/src/Grid_conversion.cc index df033c6..7495825 100644 --- a/src/Grid_conversion.cc +++ b/src/Grid_conversion.cc @@ -323,7 +323,8 @@ Grid::conversion(Congruence_System& source, Grid_Generator_System& dest, // Initialize matrix row number counters and compute the LCM of the // diagonal entries of the proper congruences in `source'. - dimension_type source_num_rows = 0, dest_num_rows = 0; + dimension_type source_num_rows = 0; + dimension_type dest_num_rows = 0; PPL_DIRTY_TEMP_COEFFICIENT(diagonal_lcm); diagonal_lcm = 1; dimension_type dims = source.space_dimension() + 1; diff --git a/src/Interval_defs.hh b/src/Interval_defs.hh index 08378a4..c07f74d 100644 --- a/src/Interval_defs.hh +++ b/src/Interval_defs.hh @@ -332,7 +332,8 @@ public: typename Enable_If<Is_Special<From>::value, I_Result>::type assign(const From&) { info().clear(); - Result rl, ru; + Result rl; + Result ru; switch (From::vclass) { case VC_MINUS_INFINITY: rl = Boundary_NS::set_minus_infinity(LOWER, lower(), info()); diff --git a/src/Interval_inlines.hh b/src/Interval_inlines.hh index 19aedd9..e986771 100644 --- a/src/Interval_inlines.hh +++ b/src/Interval_inlines.hh @@ -257,7 +257,8 @@ Interval<To_Boundary, To_Info>::join_assign(const From& x) { return assign(x); if (check_empty_arg(x)) return combine(V_EQ, V_EQ); - Result rl, ru; + Result rl; + Result ru; rl = min_assign(LOWER, lower(), info(), LOWER, f_lower(x), f_info(x)); ru = max_assign(UPPER, upper(), info(), UPPER, f_upper(x), f_info(x)); PPL_ASSERT(OK()); @@ -279,7 +280,8 @@ Interval<To_Boundary, To_Info>::join_assign(const From1& x, const From2& y) { return assign(x); PPL_DIRTY_TEMP(To_Info, to_info); to_info.clear(); - Result rl, ru; + Result rl; + Result ru; rl = min_assign(LOWER, lower(), to_info, LOWER, f_lower(x), f_info(x), LOWER, f_lower(y), f_info(y)); @@ -355,7 +357,8 @@ Interval<To_Boundary, To_Info>::difference_assign(const From& x) { return combine(V_EQ, V_EQ); bool nl = ge(LOWER, lower(), info(), LOWER, f_lower(x), f_info(x)); bool nu = le(UPPER, upper(), info(), UPPER, f_upper(x), f_info(x)); - Result rl = V_EQ, ru = V_EQ; + Result rl = V_EQ; + Result ru = V_EQ; if (nl) { if (nu) return assign(EMPTY); @@ -389,7 +392,8 @@ Interval<To_Boundary, To_Info>::difference_assign(const From1& x, return assign(x); bool nl = ge(LOWER, f_lower(x), f_info(x), LOWER, f_lower(y), f_info(y)); bool nu = le(UPPER, f_upper(x), f_info(x), UPPER, f_upper(y), f_info(y)); - Result rl = V_EQ, ru = V_EQ; + Result rl = V_EQ; + Result ru = V_EQ; if (nl) { if (nu) return assign(EMPTY); @@ -558,7 +562,8 @@ Interval<To_Boundary, To_Info>::neg_assign(const From& x) { return assign(EMPTY); PPL_DIRTY_TEMP(To_Info, to_info); to_info.clear(); - Result rl, ru; + Result rl; + Result ru; PPL_DIRTY_TEMP(To_Boundary, to_lower); rl = Boundary_NS::neg_assign(LOWER, to_lower, to_info, UPPER, f_upper(x), f_info(x)); ru = Boundary_NS::neg_assign(UPPER, upper(), to_info, LOWER, f_lower(x), f_info(x)); @@ -628,7 +633,8 @@ Interval<To_Boundary, To_Info>::sub_assign(const From1& x, const From2& y) { PPL_DIRTY_TEMP(To_Info, to_info); to_info.clear(); - Result rl, ru; + Result rl; + Result ru; PPL_DIRTY_TEMP(To_Boundary, to_lower); rl = Boundary_NS::sub_assign(LOWER, to_lower, to_info, LOWER, f_lower(x), f_info(x), @@ -670,7 +676,8 @@ Interval<To_Boundary, To_Info>::mul_assign(const From1& x, const From2& y) { int yls = sgn_b(LOWER, f_lower(y), f_info(y)); int yus = (yls > 0) ? 1 : sgn_b(UPPER, f_upper(y), f_info(y)); int inf_sign = Parma_Polyhedra_Library::infinity_sign(x); - int ls, us; + int ls; + int us; if (inf_sign != 0) { ls = yls; us = yus; @@ -697,7 +704,8 @@ Interval<To_Boundary, To_Info>::mul_assign(const From1& x, const From2& y) { PPL_DIRTY_TEMP(To_Info, to_info); to_info.clear(); - Result rl, ru; + Result rl; + Result ru; PPL_DIRTY_TEMP(To_Boundary, to_lower); if (xls >= 0) { @@ -854,7 +862,8 @@ Interval<To_Boundary, To_Info>::div_assign(const From1& x, const From2& y) { PPL_DIRTY_TEMP(To_Info, to_info); to_info.clear(); - Result rl, ru; + Result rl; + Result ru; PPL_DIRTY_TEMP(To_Boundary, to_lower); if (yls >= 0) { if (xls >= 0) { diff --git a/src/Pointset_Powerset_templates.hh b/src/Pointset_Powerset_templates.hh index 34fffcc..00d1a19 100644 --- a/src/Pointset_Powerset_templates.hh +++ b/src/Pointset_Powerset_templates.hh @@ -1329,11 +1329,10 @@ is_cert_multiset_stabilizing(const std::map<Cert, size_type, typedef std::map<Cert, size_type, typename Cert::Compare> Cert_Multiset; Cert_Multiset x_cert_ms; collect_certificates(x_cert_ms); - typename Cert_Multiset::const_iterator - xi = x_cert_ms.begin(), - x_cert_ms_end = x_cert_ms.end(), - yi = y_cert_ms.begin(), - y_cert_ms_end = y_cert_ms.end(); + typename Cert_Multiset::const_iterator xi = x_cert_ms.begin(); + typename Cert_Multiset::const_iterator x_cert_ms_end = x_cert_ms.end(); + typename Cert_Multiset::const_iterator yi = y_cert_ms.begin(); + typename Cert_Multiset::const_iterator y_cert_ms_end = y_cert_ms.end(); while (xi != x_cert_ms_end && yi != y_cert_ms_end) { const Cert& xi_cert = xi->first; const Cert& yi_cert = yi->first;

1 0