January 2013 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(polyops): Const-qualify immutable objects.
by Roberto Bagnara 14 Jan '13

14 Jan '13

Module: ppl/ppl Branch: polyops Commit: 479fd86bc58b644f81aec0cedd6b857b693cc25a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=479fd86bc58b… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Mon Jan 14 18:12:47 2013 +0100 Const-qualify immutable objects. Detected by ECLAIR service cnstpnte. --- .../ppl_interface_generator_prolog_cc_code.m4 | 47 +++++++++++--------- 1 files changed, 26 insertions(+), 21 deletions(-) diff --git a/interfaces/Prolog/ppl_interface_generator_prolog_cc_code.m4 b/interfaces/Prolog/ppl_interface_generator_prolog_cc_code.m4 index da1cb66..a7f739c 100644 --- a/interfaces/Prolog/ppl_interface_generator_prolog_cc_code.m4 +++ b/interfaces/Prolog/ppl_interface_generator_prolog_cc_code.m4 @@ -62,18 +62,18 @@ ppl_new_@TOPOLOGY@@CLASS@_from_space_dimension(Prolog_term_ref t_nd, m4_define(`ppl_new_@TOPOLOGY@@CLASS@_from_@FRIEND@_code', `extern "C" Prolog_foreign_return_type -ppl_new_@TOPOLOGY@@CLASS@_from_@FRIEND@( - Prolog_term_ref t_ph_source, Prolog_term_ref t_ph) +ppl_new_@TOPOLOGY@@CLASS@_from_@FRIEND@ +(Prolog_term_ref t_ph_source, Prolog_term_ref t_ph) { - static const char* where = - "ppl_new_@TOPOLOGY@@CLASS@_from_@FRIEND@/2"; + static const char* where + = "ppl_new_@TOPOLOGY@@CLASS@_from_@FRIEND@/2"; try { @TOPOLOGY@@CPP_CLASS@* ph; - const @B_FRIEND@* ph_source - = static_cast<const @B_FRIEND@*> + const @B_FRIEND@* const ph_source + = static_cast<const @B_FRIEND@*> (term_to_handle<@B_FRIEND@ >(t_ph_source, where)); PPL_CHECK(ph_source); - ph = new @TOPOLOGY@@CPP_CLASS@(*ph_source); + ph = new @TOPOLOGY@@CPP_CLASS@(*ph_source); Prolog_term_ref tmp = Prolog_new_term_ref(); Prolog_put_address(tmp, ph); if (Prolog_unify(t_ph, tmp)) { @@ -217,7 +217,8 @@ m4_define(`ppl_@CLASS@_get_@CLASS_REPRESENT@s_code', Prolog_term_ref t_glist) { static const char* where = "ppl_@CLASS@_get_@CLASS_REPRESENT@s/2"; try { - const @CPP_CLASS@* ph = term_to_handle<@CPP_CLASS@ >(t_ph, where); + const @CPP_CLASS@* const ph + = term_to_handle<@CPP_CLASS@ >(t_ph, where); PPL_CHECK(ph); Prolog_term_ref tail = Prolog_new_term_ref(); @@ -241,7 +242,8 @@ m4_define(`ppl_@CLASS@_get_minimized_@CLASS_REPRESENT@s_code', Prolog_term_ref t_glist) { static const char* where = "ppl_@CLASS@_get_minimized_@CLASS_REPRESENT@s/2"; try { - const @CPP_CLASS@* ph = term_to_handle<@CPP_CLASS@ >(t_ph, where); + const @CPP_CLASS@* const ph + = term_to_handle<@CPP_CLASS@ >(t_ph, where); PPL_CHECK(ph); Prolog_term_ref tail = Prolog_new_term_ref(); @@ -703,7 +705,8 @@ m4_define(`ppl_@CLASS@_@HAS_PROPERTY@_code', ppl_@CLASS@_@HAS_PROPERTY@(Prolog_term_ref t_ph) { static const char* where = "ppl_@CLASS@_@HAS_PROPERTY@/1"; try { - const @CPP_CLASS@* ph = term_to_handle<@CPP_CLASS@ >(t_ph, where); + const @CPP_CLASS@* const ph + = term_to_handle<@CPP_CLASS@ >(t_ph, where); PPL_CHECK(ph); if (ph->@HAS_PROPERTY@()) return PROLOG_SUCCESS; @@ -793,7 +796,7 @@ m4_define(`ppl_@CLASS@_bounds_from_@ABOVEBELOW@_code', try { @CPP_CLASS@* ph = term_to_handle<@CPP_CLASS@ >(t_ph, where); PPL_CHECK(ph); - Linear_Expression l = build_linear_expression(t_expr, where); + const Linear_Expression l = build_linear_expression(t_expr, where); if (ph->bounds_from_@ABOVEBELOW@(l)) return PROLOG_SUCCESS; } @@ -838,7 +841,8 @@ m4_define(`ppl_@CLASS@_@MAXMIN@_code', Prolog_term_ref t_maxmin) { static const char* where = "ppl_@CLASS@_@MAXMIN@/5"; try { - const @CPP_CLASS@* ph = term_to_handle<@CPP_CLASS@ >(t_ph, where); + const @CPP_CLASS@* const ph + = term_to_handle<@CPP_CLASS@ >(t_ph, where); PPL_CHECK(ph); const Linear_Expression le = build_linear_expression(t_le_expr, where); PPL_DIRTY_TEMP_COEFFICIENT(n); @@ -846,7 +850,7 @@ m4_define(`ppl_@CLASS@_@MAXMIN@_code', bool maxmin; if (ph->@MAXMIN@(le, n, d, maxmin)) { Prolog_term_ref t = Prolog_new_term_ref(); - Prolog_atom a = (maxmin ? a_true : a_false); + const Prolog_atom a = (maxmin ? a_true : a_false); Prolog_put_atom(t, a); if (Prolog_unify_Coefficient(t_n, n) && Prolog_unify_Coefficient(t_d, d) @@ -860,14 +864,15 @@ m4_define(`ppl_@CLASS@_@MAXMIN@_code', ') m4_define(`ppl_@CLASS@_@MAXMIN@_with_point_code', - `extern "C" Prolog_foreign_return_type - ppl_@CLASS@_@MAXMIN@_with_point(Prolog_term_ref t_ph, - Prolog_term_ref t_le_expr, - Prolog_term_ref t_n, Prolog_term_ref t_d, - Prolog_term_ref t_maxmin, Prolog_term_ref t_g) { +`extern "C" Prolog_foreign_return_type +ppl_@CLASS@_@MAXMIN@_with_point +(Prolog_term_ref t_ph, + Prolog_term_ref t_le_expr, + Prolog_term_ref t_n, Prolog_term_ref t_d, + Prolog_term_ref t_maxmin, Prolog_term_ref t_g) { static const char* where = "ppl_@CLASS@_@MAXMIN@_with_point/6"; try { - const @CPP_CLASS@* ph = term_to_handle<@CPP_CLASS@ >(t_ph, where); + const @CPP_CLASS@* const ph = term_to_handle<@CPP_CLASS@ >(t_ph, where); PPL_CHECK(ph); const Linear_Expression le = build_linear_expression(t_le_expr, where); PPL_DIRTY_TEMP_COEFFICIENT(n); @@ -876,7 +881,7 @@ m4_define(`ppl_@CLASS@_@MAXMIN@_with_point_code', Generator g(point()); if (ph->@MAXMIN@(le, n, d, maxmin, g)) { Prolog_term_ref t = Prolog_new_term_ref(); - Prolog_atom a = (maxmin ? a_true : a_false); + const Prolog_atom a = (maxmin ? a_true : a_false); Prolog_put_atom(t, a); if (Prolog_unify_Coefficient(t_n, n) && Prolog_unify_Coefficient(t_d, d) @@ -930,7 +935,7 @@ m4_define(`ppl_@CLASS@_OK_code', ppl_@CLASS@_OK(Prolog_term_ref t_ph) { static const char* where = "ppl_@CLASS@_OK/1"; try { - const @CPP_CLASS@* ph = term_to_handle<@CPP_CLASS@ >(t_ph, where); + const @CPP_CLASS@* const ph = term_to_handle<@CPP_CLASS@ >(t_ph, where); PPL_CHECK(ph); if (ph->OK()) return PROLOG_SUCCESS;

1 0

[GIT] ppl/ppl(polyops): Links updated.
by Roberto Bagnara 14 Jan '13

14 Jan '13

Module: ppl/ppl Branch: polyops Commit: aee1d002585b6185507ad9bc1426616b3db4129d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=aee1d002585b… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Mon Jan 14 18:12:15 2013 +0100 Links updated. --- doc/ppl.bib | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/ppl.bib b/doc/ppl.bib index aa56844..0d73b78 100644 --- a/doc/ppl.bib +++ b/doc/ppl.bib @@ -1787,7 +1787,7 @@ Summarizing: The result is an efficient automatic tool for approximate, but conservative, verification of reachability properties of these systems.", - URL = "http://www-verimag.imag.fr/PEOPLE/Nicolas.Halbwachs/hybrid.html" + URL = "http://www-verimag.imag.fr/~halbwach/hybrid.html" } @Manual{HalbwachsKP95, @@ -1848,7 +1848,7 @@ Summarizing: sufficient precision is obtained. We consider the standard abstract convex-hull operator and a novel abstract extrapolation operator.", - URL = "http://www-cad.eecs.berkeley.edu/HomePages/tah/Publications/abstract-interp…" + URL = "http://pub.ist.ac.at/~tah/Publications/abstract-interpretation_strategies_f…" } @InProceedings{HenzingerPW01, @@ -1874,7 +1874,7 @@ Summarizing: to address some of the tool's shortcomings. We evaluate these extensions, and conclude with some desiderata for verification tools for hybrid systems.", - URL = "http://www-cad.eecs.berkeley.edu/HomePages/tah/Publications/some_lessons_fr…" + URL = "http://pub.ist.ac.at/~tah/Publications/some_lessons_from_the_hytech_experie…" } @TechReport{HuelsbergenHL90,

1 0

[GIT] ppl/ppl(polyops): Const-qualify immutable objects.
by Roberto Bagnara 14 Jan '13

14 Jan '13

Module: ppl/ppl Branch: polyops Commit: fd568b02214e751e909f88f33719776d37b4256b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fd568b02214e… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Wed Jan 9 18:09:28 2013 +0100 Const-qualify immutable objects. Detected by ECLAIR service cnstpnte. --- interfaces/C/ppl_interface_generator_c_cc_code.m4 | 2 +- .../OCaml/ppl_interface_generator_ocaml_cc_code.m4 | 58 ++++++++++---------- interfaces/OCaml/ppl_ocaml_common.cc | 22 ++++---- 3 files changed, 41 insertions(+), 41 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=fd568b02…

1 0

[GIT] ppl/ppl(polyops): Const-qualify immutable objects.
by Roberto Bagnara 14 Jan '13

14 Jan '13

Module: ppl/ppl Branch: polyops Commit: 3d42a8fdc6039720fdb2eb362505bc56273d8098 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3d42a8fdc603… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Jan 5 20:53:04 2013 +0100 Const-qualify immutable objects. Detected by ECLAIR service cnstpnte. --- interfaces/C/ppl_interface_generator_c_cc_code.m4 | 22 ++++++++++---------- 1 files changed, 11 insertions(+), 11 deletions(-) diff --git a/interfaces/C/ppl_interface_generator_c_cc_code.m4 b/interfaces/C/ppl_interface_generator_c_cc_code.m4 index 4f743c1..6cc8683 100644 --- a/interfaces/C/ppl_interface_generator_c_cc_code.m4 +++ b/interfaces/C/ppl_interface_generator_c_cc_code.m4 @@ -41,7 +41,7 @@ ppl_new_@TOPOLOGY@@CLASS@_from_space_dimension (ppl_@CLASS@_t* pph, ppl_dimension_type d, int empty) try { - Degenerate_Element e = (empty != 0) ? EMPTY : UNIVERSE; + const Degenerate_Element e = (empty != 0) ? EMPTY : UNIVERSE; *pph = to_nonconst(new @TOPOLOGY@@CPP_CLASS@(d, e)); return 0; } @@ -227,7 +227,7 @@ ppl_@CLASS@_@MAXMIN@ Coefficient& ssup_n = *to_nonconst(sup_n); Coefficient& ssup_d = *to_nonconst(sup_d); bool optimum; - bool ok = pph.@MAXMIN@(lle, ssup_n, ssup_d, optimum); + const bool ok = pph.@MAXMIN@(lle, ssup_n, ssup_d, optimum); if (ok) *poptimum = optimum ? 1 : 0; return ok ? 1 : 0; @@ -251,7 +251,7 @@ ppl_@CLASS@_@MAXMIN@_with_point Coefficient& ssup_d = *to_nonconst(sup_d); Generator& ppoint = *to_nonconst(point); bool optimum; - bool ok = pph.@MAXMIN@(lle, ssup_n, ssup_d, optimum, ppoint); + const bool ok = pph.@MAXMIN@(lle, ssup_n, ssup_d, optimum, ppoint); if (ok) *poptimum = optimum ? 1 : 0; return ok ? 1 : 0; @@ -386,7 +386,7 @@ ppl_@CLASS@_constrains (ppl_@CLASS@_t ph, ppl_dimension_type var ) try { - @CPP_CLASS@& pph = *to_nonconst(ph); + const @CPP_CLASS@& pph = *to_const(ph); return pph.constrains(Variable(var)) ? 1 : 0; } CATCH_ALL @@ -845,7 +845,7 @@ ppl_@CLASS@_map_space_dimensions ppl_dimension_type maps[], size_t n) try { @CPP_CLASS@& pph = *to_nonconst(ph); - Array_Partial_Function_Wrapper function(maps, n); + const Array_Partial_Function_Wrapper function(maps, n); pph.map_space_dimensions(function); return 0; } @@ -1288,7 +1288,7 @@ ppl_one_affine_ranking_function_@TERMINATION_ID@_@TOPOLOGY@@CLASS@ const @TOPOLOGY@@CPP_CLASS@& ppset = *static_cast<const @TOPOLOGY@@CPP_CLASS@*>(to_const(pset)); Generator& ppoint = *to_nonconst(point); - bool ok = one_affine_ranking_function_@TERMINATION_ID@(ppset, ppoint); + const bool ok = one_affine_ranking_function_@TERMINATION_ID@(ppset, ppoint); return ok ? 1 : 0; } CATCH_ALL @@ -1306,9 +1306,9 @@ ppl_one_affine_ranking_function_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2 const @TOPOLOGY@@CPP_CLASS@& ppset_after = *static_cast<const @TOPOLOGY@@CPP_CLASS@*>(to_const(pset_after)); Generator& ppoint = *to_nonconst(point); - bool ok = one_affine_ranking_function_@TERMINATION_ID@_2(ppset_before, - ppset_after, - ppoint); + const bool ok = one_affine_ranking_function_@TERMINATION_ID@_2(ppset_before, + ppset_after, + ppoint); return ok ? 1 : 0; } CATCH_ALL @@ -1402,8 +1402,8 @@ ppl_@CLASS@_wrap_assign Variables_Set vars; for (ppl_dimension_type i = n; i-- > 0; ) vars.insert(ds[i]); - const Constraint_System* ccs = to_const(*pcs); - bool b = (wrap_individually != 0); + const Constraint_System* const ccs = to_const(*pcs); + const bool b = (wrap_individually != 0); pph.wrap_assign(vars, bounded_integer_type_width(w), bounded_integer_type_representation(r),

1 0

[GIT] ppl/ppl(master): Const-qualify immutable objects.
by Roberto Bagnara 14 Jan '13

14 Jan '13

Module: ppl/ppl Branch: master Commit: 479fd86bc58b644f81aec0cedd6b857b693cc25a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=479fd86bc58b… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Mon Jan 14 18:12:47 2013 +0100 Const-qualify immutable objects. Detected by ECLAIR service cnstpnte. --- .../ppl_interface_generator_prolog_cc_code.m4 | 47 +++++++++++--------- 1 files changed, 26 insertions(+), 21 deletions(-) diff --git a/interfaces/Prolog/ppl_interface_generator_prolog_cc_code.m4 b/interfaces/Prolog/ppl_interface_generator_prolog_cc_code.m4 index da1cb66..a7f739c 100644 --- a/interfaces/Prolog/ppl_interface_generator_prolog_cc_code.m4 +++ b/interfaces/Prolog/ppl_interface_generator_prolog_cc_code.m4 @@ -62,18 +62,18 @@ ppl_new_@TOPOLOGY@@CLASS@_from_space_dimension(Prolog_term_ref t_nd, m4_define(`ppl_new_@TOPOLOGY@@CLASS@_from_@FRIEND@_code', `extern "C" Prolog_foreign_return_type -ppl_new_@TOPOLOGY@@CLASS@_from_@FRIEND@( - Prolog_term_ref t_ph_source, Prolog_term_ref t_ph) +ppl_new_@TOPOLOGY@@CLASS@_from_@FRIEND@ +(Prolog_term_ref t_ph_source, Prolog_term_ref t_ph) { - static const char* where = - "ppl_new_@TOPOLOGY@@CLASS@_from_@FRIEND@/2"; + static const char* where + = "ppl_new_@TOPOLOGY@@CLASS@_from_@FRIEND@/2"; try { @TOPOLOGY@@CPP_CLASS@* ph; - const @B_FRIEND@* ph_source - = static_cast<const @B_FRIEND@*> + const @B_FRIEND@* const ph_source + = static_cast<const @B_FRIEND@*> (term_to_handle<@B_FRIEND@ >(t_ph_source, where)); PPL_CHECK(ph_source); - ph = new @TOPOLOGY@@CPP_CLASS@(*ph_source); + ph = new @TOPOLOGY@@CPP_CLASS@(*ph_source); Prolog_term_ref tmp = Prolog_new_term_ref(); Prolog_put_address(tmp, ph); if (Prolog_unify(t_ph, tmp)) { @@ -217,7 +217,8 @@ m4_define(`ppl_@CLASS@_get_@CLASS_REPRESENT@s_code', Prolog_term_ref t_glist) { static const char* where = "ppl_@CLASS@_get_@CLASS_REPRESENT@s/2"; try { - const @CPP_CLASS@* ph = term_to_handle<@CPP_CLASS@ >(t_ph, where); + const @CPP_CLASS@* const ph + = term_to_handle<@CPP_CLASS@ >(t_ph, where); PPL_CHECK(ph); Prolog_term_ref tail = Prolog_new_term_ref(); @@ -241,7 +242,8 @@ m4_define(`ppl_@CLASS@_get_minimized_@CLASS_REPRESENT@s_code', Prolog_term_ref t_glist) { static const char* where = "ppl_@CLASS@_get_minimized_@CLASS_REPRESENT@s/2"; try { - const @CPP_CLASS@* ph = term_to_handle<@CPP_CLASS@ >(t_ph, where); + const @CPP_CLASS@* const ph + = term_to_handle<@CPP_CLASS@ >(t_ph, where); PPL_CHECK(ph); Prolog_term_ref tail = Prolog_new_term_ref(); @@ -703,7 +705,8 @@ m4_define(`ppl_@CLASS@_@HAS_PROPERTY@_code', ppl_@CLASS@_@HAS_PROPERTY@(Prolog_term_ref t_ph) { static const char* where = "ppl_@CLASS@_@HAS_PROPERTY@/1"; try { - const @CPP_CLASS@* ph = term_to_handle<@CPP_CLASS@ >(t_ph, where); + const @CPP_CLASS@* const ph + = term_to_handle<@CPP_CLASS@ >(t_ph, where); PPL_CHECK(ph); if (ph->@HAS_PROPERTY@()) return PROLOG_SUCCESS; @@ -793,7 +796,7 @@ m4_define(`ppl_@CLASS@_bounds_from_@ABOVEBELOW@_code', try { @CPP_CLASS@* ph = term_to_handle<@CPP_CLASS@ >(t_ph, where); PPL_CHECK(ph); - Linear_Expression l = build_linear_expression(t_expr, where); + const Linear_Expression l = build_linear_expression(t_expr, where); if (ph->bounds_from_@ABOVEBELOW@(l)) return PROLOG_SUCCESS; } @@ -838,7 +841,8 @@ m4_define(`ppl_@CLASS@_@MAXMIN@_code', Prolog_term_ref t_maxmin) { static const char* where = "ppl_@CLASS@_@MAXMIN@/5"; try { - const @CPP_CLASS@* ph = term_to_handle<@CPP_CLASS@ >(t_ph, where); + const @CPP_CLASS@* const ph + = term_to_handle<@CPP_CLASS@ >(t_ph, where); PPL_CHECK(ph); const Linear_Expression le = build_linear_expression(t_le_expr, where); PPL_DIRTY_TEMP_COEFFICIENT(n); @@ -846,7 +850,7 @@ m4_define(`ppl_@CLASS@_@MAXMIN@_code', bool maxmin; if (ph->@MAXMIN@(le, n, d, maxmin)) { Prolog_term_ref t = Prolog_new_term_ref(); - Prolog_atom a = (maxmin ? a_true : a_false); + const Prolog_atom a = (maxmin ? a_true : a_false); Prolog_put_atom(t, a); if (Prolog_unify_Coefficient(t_n, n) && Prolog_unify_Coefficient(t_d, d) @@ -860,14 +864,15 @@ m4_define(`ppl_@CLASS@_@MAXMIN@_code', ') m4_define(`ppl_@CLASS@_@MAXMIN@_with_point_code', - `extern "C" Prolog_foreign_return_type - ppl_@CLASS@_@MAXMIN@_with_point(Prolog_term_ref t_ph, - Prolog_term_ref t_le_expr, - Prolog_term_ref t_n, Prolog_term_ref t_d, - Prolog_term_ref t_maxmin, Prolog_term_ref t_g) { +`extern "C" Prolog_foreign_return_type +ppl_@CLASS@_@MAXMIN@_with_point +(Prolog_term_ref t_ph, + Prolog_term_ref t_le_expr, + Prolog_term_ref t_n, Prolog_term_ref t_d, + Prolog_term_ref t_maxmin, Prolog_term_ref t_g) { static const char* where = "ppl_@CLASS@_@MAXMIN@_with_point/6"; try { - const @CPP_CLASS@* ph = term_to_handle<@CPP_CLASS@ >(t_ph, where); + const @CPP_CLASS@* const ph = term_to_handle<@CPP_CLASS@ >(t_ph, where); PPL_CHECK(ph); const Linear_Expression le = build_linear_expression(t_le_expr, where); PPL_DIRTY_TEMP_COEFFICIENT(n); @@ -876,7 +881,7 @@ m4_define(`ppl_@CLASS@_@MAXMIN@_with_point_code', Generator g(point()); if (ph->@MAXMIN@(le, n, d, maxmin, g)) { Prolog_term_ref t = Prolog_new_term_ref(); - Prolog_atom a = (maxmin ? a_true : a_false); + const Prolog_atom a = (maxmin ? a_true : a_false); Prolog_put_atom(t, a); if (Prolog_unify_Coefficient(t_n, n) && Prolog_unify_Coefficient(t_d, d) @@ -930,7 +935,7 @@ m4_define(`ppl_@CLASS@_OK_code', ppl_@CLASS@_OK(Prolog_term_ref t_ph) { static const char* where = "ppl_@CLASS@_OK/1"; try { - const @CPP_CLASS@* ph = term_to_handle<@CPP_CLASS@ >(t_ph, where); + const @CPP_CLASS@* const ph = term_to_handle<@CPP_CLASS@ >(t_ph, where); PPL_CHECK(ph); if (ph->OK()) return PROLOG_SUCCESS;

1 0

[GIT] ppl/ppl(master): Links updated.
by Roberto Bagnara 14 Jan '13

14 Jan '13

Module: ppl/ppl Branch: master Commit: aee1d002585b6185507ad9bc1426616b3db4129d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=aee1d002585b… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Mon Jan 14 18:12:15 2013 +0100 Links updated. --- doc/ppl.bib | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/ppl.bib b/doc/ppl.bib index aa56844..0d73b78 100644 --- a/doc/ppl.bib +++ b/doc/ppl.bib @@ -1787,7 +1787,7 @@ Summarizing: The result is an efficient automatic tool for approximate, but conservative, verification of reachability properties of these systems.", - URL = "http://www-verimag.imag.fr/PEOPLE/Nicolas.Halbwachs/hybrid.html" + URL = "http://www-verimag.imag.fr/~halbwach/hybrid.html" } @Manual{HalbwachsKP95, @@ -1848,7 +1848,7 @@ Summarizing: sufficient precision is obtained. We consider the standard abstract convex-hull operator and a novel abstract extrapolation operator.", - URL = "http://www-cad.eecs.berkeley.edu/HomePages/tah/Publications/abstract-interp…" + URL = "http://pub.ist.ac.at/~tah/Publications/abstract-interpretation_strategies_f…" } @InProceedings{HenzingerPW01, @@ -1874,7 +1874,7 @@ Summarizing: to address some of the tool's shortcomings. We evaluate these extensions, and conclude with some desiderata for verification tools for hybrid systems.", - URL = "http://www-cad.eecs.berkeley.edu/HomePages/tah/Publications/some_lessons_fr…" + URL = "http://pub.ist.ac.at/~tah/Publications/some_lessons_from_the_hytech_experie…" } @TechReport{HuelsbergenHL90,

1 0

[GIT] ppl/ppl(master): Const-qualify immutable objects.
by Roberto Bagnara 09 Jan '13

09 Jan '13

Module: ppl/ppl Branch: master Commit: fd568b02214e751e909f88f33719776d37b4256b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fd568b02214e… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Wed Jan 9 18:09:28 2013 +0100 Const-qualify immutable objects. Detected by ECLAIR service cnstpnte. --- interfaces/C/ppl_interface_generator_c_cc_code.m4 | 2 +- .../OCaml/ppl_interface_generator_ocaml_cc_code.m4 | 58 ++++++++++---------- interfaces/OCaml/ppl_ocaml_common.cc | 22 ++++---- 3 files changed, 41 insertions(+), 41 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=fd568b02…

1 0

[GIT] ppl/ppl(master): Const-qualify immutable objects.
by Roberto Bagnara 05 Jan '13

05 Jan '13

Module: ppl/ppl Branch: master Commit: 3d42a8fdc6039720fdb2eb362505bc56273d8098 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3d42a8fdc603… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Jan 5 20:53:04 2013 +0100 Const-qualify immutable objects. Detected by ECLAIR service cnstpnte. --- interfaces/C/ppl_interface_generator_c_cc_code.m4 | 22 ++++++++++---------- 1 files changed, 11 insertions(+), 11 deletions(-) diff --git a/interfaces/C/ppl_interface_generator_c_cc_code.m4 b/interfaces/C/ppl_interface_generator_c_cc_code.m4 index 4f743c1..6cc8683 100644 --- a/interfaces/C/ppl_interface_generator_c_cc_code.m4 +++ b/interfaces/C/ppl_interface_generator_c_cc_code.m4 @@ -41,7 +41,7 @@ ppl_new_@TOPOLOGY@@CLASS@_from_space_dimension (ppl_@CLASS@_t* pph, ppl_dimension_type d, int empty) try { - Degenerate_Element e = (empty != 0) ? EMPTY : UNIVERSE; + const Degenerate_Element e = (empty != 0) ? EMPTY : UNIVERSE; *pph = to_nonconst(new @TOPOLOGY@@CPP_CLASS@(d, e)); return 0; } @@ -227,7 +227,7 @@ ppl_@CLASS@_@MAXMIN@ Coefficient& ssup_n = *to_nonconst(sup_n); Coefficient& ssup_d = *to_nonconst(sup_d); bool optimum; - bool ok = pph.@MAXMIN@(lle, ssup_n, ssup_d, optimum); + const bool ok = pph.@MAXMIN@(lle, ssup_n, ssup_d, optimum); if (ok) *poptimum = optimum ? 1 : 0; return ok ? 1 : 0; @@ -251,7 +251,7 @@ ppl_@CLASS@_@MAXMIN@_with_point Coefficient& ssup_d = *to_nonconst(sup_d); Generator& ppoint = *to_nonconst(point); bool optimum; - bool ok = pph.@MAXMIN@(lle, ssup_n, ssup_d, optimum, ppoint); + const bool ok = pph.@MAXMIN@(lle, ssup_n, ssup_d, optimum, ppoint); if (ok) *poptimum = optimum ? 1 : 0; return ok ? 1 : 0; @@ -386,7 +386,7 @@ ppl_@CLASS@_constrains (ppl_@CLASS@_t ph, ppl_dimension_type var ) try { - @CPP_CLASS@& pph = *to_nonconst(ph); + const @CPP_CLASS@& pph = *to_const(ph); return pph.constrains(Variable(var)) ? 1 : 0; } CATCH_ALL @@ -845,7 +845,7 @@ ppl_@CLASS@_map_space_dimensions ppl_dimension_type maps[], size_t n) try { @CPP_CLASS@& pph = *to_nonconst(ph); - Array_Partial_Function_Wrapper function(maps, n); + const Array_Partial_Function_Wrapper function(maps, n); pph.map_space_dimensions(function); return 0; } @@ -1288,7 +1288,7 @@ ppl_one_affine_ranking_function_@TERMINATION_ID@_@TOPOLOGY@@CLASS@ const @TOPOLOGY@@CPP_CLASS@& ppset = *static_cast<const @TOPOLOGY@@CPP_CLASS@*>(to_const(pset)); Generator& ppoint = *to_nonconst(point); - bool ok = one_affine_ranking_function_@TERMINATION_ID@(ppset, ppoint); + const bool ok = one_affine_ranking_function_@TERMINATION_ID@(ppset, ppoint); return ok ? 1 : 0; } CATCH_ALL @@ -1306,9 +1306,9 @@ ppl_one_affine_ranking_function_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2 const @TOPOLOGY@@CPP_CLASS@& ppset_after = *static_cast<const @TOPOLOGY@@CPP_CLASS@*>(to_const(pset_after)); Generator& ppoint = *to_nonconst(point); - bool ok = one_affine_ranking_function_@TERMINATION_ID@_2(ppset_before, - ppset_after, - ppoint); + const bool ok = one_affine_ranking_function_@TERMINATION_ID@_2(ppset_before, + ppset_after, + ppoint); return ok ? 1 : 0; } CATCH_ALL @@ -1402,8 +1402,8 @@ ppl_@CLASS@_wrap_assign Variables_Set vars; for (ppl_dimension_type i = n; i-- > 0; ) vars.insert(ds[i]); - const Constraint_System* ccs = to_const(*pcs); - bool b = (wrap_individually != 0); + const Constraint_System* const ccs = to_const(*pcs); + const bool b = (wrap_individually != 0); pph.wrap_assign(vars, bounded_integer_type_width(w), bounded_integer_type_representation(r),

1 0

Re: [PPL-devel] [Bug Report] GMP and PPL mismatches
by Chia-Hsun Cheng 05 Jan '13

05 Jan '13

Dear Roberto Bagnara, I followed the provided link and downloaded ppl-1.1pre6 version. The compilation was fine and all tests in "make check" passed. The build-up of gcc was successful as well. Thanks for the fast response and kind help! Dear Marco Bodrato, Thanks for the notification that solves my confusion! Best Regards, -- chiahsun 2013/1/4 Roberto Bagnara <bagnara(a)cs.unipr.it> > On 01/03/13 12:47, Chia-Hsun Cheng wrote: > >> 2. < Static data member name mismatches > >> ppl-1.0/src/mp_std_bits.defs.**hh:72 and >> ppl-1.0/src/mp_std_bits.defs.**hh:133 defines >> static const bool tininess_before = false; >> ^^^^^^^^^^^^^^^^^ >> However, in >> gmp-5.1.0/gmpxx.h:3302 and gmp-5.1.0/gmpxx.h:3339, there are >> static const bool tinyness_before = false; >> ^^^^^^^^^^^^^^^^^^ >> Problem: >> I am not sure if the two data member are the same. Since I commented >> out the whole block of >> numeric_limits in ppl-1.0/src/mp_std_bits.defs.**hh in the last step, >> the member `tininess_before' >> cannot be resolved. >> Fix: >> Finally, I add >> static const bool tininess_before = false; >> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^**^^^^^^^^^^^^ >> in gmp-5.1.0/gmpxx.h:3303 and gmp-5.1.0/gmpxx.h:3341 >> and add member initialization >> const bool numeric_limits<T>::tininess_**before; \ >> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^**^^^^^^^^^^^^^^^^^^ >> in gmp-5.1.0/cxx/limits.cc:47 >> and rebuild the gmp library. >> So, for PPL library, even if the code for numeric_limits is commented >> out, the declarations and object >> code can be found from GMP library. >> > > Dear Chia-Hsun, > > Marco Bodrato (thanks Marco!) made me notice I overlooked this part > of your message. Indeed this is a bug in the PPL: the right spelling > is `tinyness_before' as correctly written in GMP. I have just fixed > the Git version of the PPL and a new PPL 1.1 snapshot release will soon > be added to the location I already indicated. > > Kind regards, > > Roberto > > -- > Prof. Roberto Bagnara > > Applied Formal Methods Laboratory - University of Parma, Italy > mailto:bagnara@cs.unipr.it > BUGSENG srl - http://bugseng.com > mailto:roberto.bagnara@**bugseng.com<roberto.bagnara(a)bugseng.com> >

1 0

[GIT] ppl/ppl(polyops): Const-qualify immutable objects.
by Roberto Bagnara 04 Jan '13

04 Jan '13

Module: ppl/ppl Branch: polyops Commit: 9ddca3fbdf256f9c2457298e2947185210a4a77f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9ddca3fbdf25… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jan 4 19:08:19 2013 +0100 Const-qualify immutable objects. Detected by ECLAIR service cnstpnte. --- src/Box_templates.hh | 6 ++++-- src/CO_Tree.cc | 2 +- src/Linear_System_inlines.hh | 2 +- src/MIP_Problem.cc | 2 +- src/OR_Matrix_inlines.hh | 2 +- src/Polyhedron_inlines.hh | 2 +- src/c_streambuf.cc | 2 +- 7 files changed, 10 insertions(+), 8 deletions(-) diff --git a/src/Box_templates.hh b/src/Box_templates.hh index 6853b48..227dd65 100644 --- a/src/Box_templates.hh +++ b/src/Box_templates.hh @@ -2538,7 +2538,8 @@ Box<ITV>::propagate_constraint_no_check(const Constraint& c) { if (open == T_MAYBE && maybe_check_fpu_inexact<Temp_Boundary_Type>() == 1) open = T_YES; - Relation_Symbol rel = (open == T_YES) ? LESS_THAN : LESS_OR_EQUAL; + const Relation_Symbol rel + = (open == T_YES) ? LESS_THAN : LESS_OR_EQUAL; seq[k_var.id()].add_constraint(i_constraint(rel, t_bound)); reset_empty_up_to_date(); } @@ -2672,7 +2673,8 @@ Box<ITV>::propagate_constraint_no_check(const Constraint& c) { if (open == T_MAYBE && maybe_check_fpu_inexact<Temp_Boundary_Type>() == 1) open = T_YES; - Relation_Symbol rel = (open == T_YES) ? GREATER_THAN : GREATER_OR_EQUAL; + const Relation_Symbol rel + = (open == T_YES) ? GREATER_THAN : GREATER_OR_EQUAL; seq[k_var.id()].add_constraint(i_constraint(rel, t_bound)); reset_empty_up_to_date(); } diff --git a/src/CO_Tree.cc b/src/CO_Tree.cc index 5a67d90..a7e5ecd 100644 --- a/src/CO_Tree.cc +++ b/src/CO_Tree.cc @@ -169,7 +169,7 @@ PPL::CO_Tree::erase_element_and_shift_left(dimension_type key) { return; const dimension_type i = dfs_index(itr); dimension_type* p = indexes + i; - const dimension_type* p_end = indexes + (reserved_size + 1); + const dimension_type* const p_end = indexes + (reserved_size + 1); for ( ; p != p_end; ++p) if (*p != unused_index) --(*p); diff --git a/src/Linear_System_inlines.hh b/src/Linear_System_inlines.hh index 995043e..a2aedba 100644 --- a/src/Linear_System_inlines.hh +++ b/src/Linear_System_inlines.hh @@ -366,7 +366,7 @@ inline void Linear_System<Row>::remove_row_no_ok(const dimension_type i, const bool keep_sorted) { PPL_ASSERT(i < num_rows()); - bool was_pending = (i >= index_first_pending); + const bool was_pending = (i >= index_first_pending); if (sorted && keep_sorted && !was_pending) { for (dimension_type j = i + 1; j < rows.size(); ++j) diff --git a/src/MIP_Problem.cc b/src/MIP_Problem.cc index 8c3d12c..b5030d8 100644 --- a/src/MIP_Problem.cc +++ b/src/MIP_Problem.cc @@ -1035,7 +1035,7 @@ PPL::MIP_Problem::steepest_edge_float_entering_index() const { // this implementation and the dense implementation below. for (std::vector<std::pair<dimension_type, double> >::const_reverse_iterator i = columns.rbegin(), i_end = columns.rend(); i != i_end; ++i) { - double challenger_value = sqrt(i->second); + const double challenger_value = sqrt(i->second); if (entering_index == 0 || challenger_value > current_value) { current_value = challenger_value; entering_index = i->first; diff --git a/src/OR_Matrix_inlines.hh b/src/OR_Matrix_inlines.hh index 4dfd006..f0e8349 100644 --- a/src/OR_Matrix_inlines.hh +++ b/src/OR_Matrix_inlines.hh @@ -465,7 +465,7 @@ inline dimension_type OR_Matrix<T>::max_num_rows() { // Compute the maximum number of rows that are contained in a DB_Row // that allocates a pseudo-triangular matrix. - dimension_type k = isqrt(2*DB_Row<T>::max_size() + 1); + const dimension_type k = isqrt(2*DB_Row<T>::max_size() + 1); return (k - 1) - (k - 1) % 2; } diff --git a/src/Polyhedron_inlines.hh b/src/Polyhedron_inlines.hh index aa521e8..f543e9c 100644 --- a/src/Polyhedron_inlines.hh +++ b/src/Polyhedron_inlines.hh @@ -434,7 +434,7 @@ Polyhedron::strictly_contains(const Polyhedron& y) const { inline void Polyhedron::drop_some_non_integer_points(Complexity_Class complexity) { - const Variables_Set* p_vs = 0; + const Variables_Set* const p_vs = 0; drop_some_non_integer_points(p_vs, complexity); } diff --git a/src/c_streambuf.cc b/src/c_streambuf.cc index 3c83995..a15499a 100644 --- a/src/c_streambuf.cc +++ b/src/c_streambuf.cc @@ -30,7 +30,7 @@ namespace Parma_Polyhedra_Library { c_streambuf::int_type c_streambuf::uflow() { - int_type c = underflow(); + const int_type c = underflow(); next_char_buf = traits_type::eof(); return c; }

1 0