- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Avoid a non-portable GNU Make idiom (using $< in a non-suffix rule context).
by Roberto Bagnara 17 Jul '12

17 Jul '12

Module: ppl/ppl Branch: master Commit: 64802610e73c3db4f520cedaebf73eadfc0a4611 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=64802610e73c… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Jul 17 16:49:39 2012 +0200 Avoid a non-portable GNU Make idiom (using $< in a non-suffix rule context). --- Makefile.am | 4 ++-- src/Makefile.am | 16 ++++++++-------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/Makefile.am b/Makefile.am index 1b80b3d..3cb89d5 100644 --- a/Makefile.am +++ b/Makefile.am @@ -36,10 +36,10 @@ dist_noinst_HEADERS = \ instchk.hh ppl-config.h: config.h $(srcdir)/ppl-config.sed - $(SED) -f $(srcdir)/ppl-config.sed $< >$@ + $(SED) -f $(srcdir)/ppl-config.sed config.h >$@ ppl-config.h.in: config.h.in $(srcdir)/ppl-config.sed - $(SED) -f $(srcdir)/ppl-config.sed $< >$@ + $(SED) -f $(srcdir)/ppl-config.sed config.h.in >$@ DISTCHECK_CONFIGURE_FLAGS = \ --enable-shared diff --git a/src/Makefile.am b/src/Makefile.am index 8a73add..6fb2c3f 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -628,28 +628,28 @@ ppl.hh.sed: Makefile @echo "}" >>$@ ppl.hh: ppl.hh.dist ppl.hh.sed - $(SED) -f ppl.hh.sed $< >$@ + $(SED) -f ppl.hh.sed ppl.hh.dist >$@ rm -f ppl.hh.sed BUGS.hh: BUGS.hh.dist - cp -f $< $@ + cp -f BUGS.hh.dist $@ BUGS.cc: BUGS.cc.dist - cp -f $< $@ + cp -f BUGS.cc.dist $@ COPYING.hh: COPYING.hh.dist - cp -f $< $@ + cp -f COPYING.hh.dist $@ COPYING.cc: COPYING.cc.dist - cp -f $< $@ + cp -f COPYING.cc.dist $@ CREDITS.hh: CREDITS.hh.dist - cp -f $< $@ + cp -f CREDITS.hh.dist $@ CREDITS.cc: CREDITS.cc.dist - cp -f $< $@ + cp -f CREDITS.cc.dist $@ endif !HAVE_PERL if USE_PRECOMPILED_HEADERS ppl.hh.gch: ppl.hh - $(CXXCOMPILE) -xc++-header -o $@ $< + $(CXXCOMPILE) -xc++-header -o $@ ppl.hh PRECOMPILED = ppl.hh.gch

1 0

[GIT] ppl/ppl(master): Changed test04 to print more info when noisy.
by Enea Zaffanella 13 Jul '12

13 Jul '12

Module: ppl/ppl Branch: master Commit: 8a29319f037b70bef7b59992a1f95132aa9254cc URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8a29319f037b… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Jul 13 15:40:36 2012 +0200 Changed test04 to print more info when noisy. --- tests/Concrete_Expression/polyhedron2.cc | 29 +++++++++++++++++------------ 1 files changed, 17 insertions(+), 12 deletions(-) diff --git a/tests/Concrete_Expression/polyhedron2.cc b/tests/Concrete_Expression/polyhedron2.cc index 8ac9cf3..4577b3d 100644 --- a/tests/Concrete_Expression/polyhedron2.cc +++ b/tests/Concrete_Expression/polyhedron2.cc @@ -119,27 +119,26 @@ test04() { FP_Interval_Abstract_Store store(2); store.set_interval(A, tmp0); store.set_interval(B, tmp0); - FP_Interval tmp(tmp0); - tmp = 2; - tmp /= FP_Interval(3); FP_Linear_Form la(A); FP_Linear_Form lb(B); - FP_Linear_Form lk(tmp); + + FP_Interval tmp(2); + tmp /= FP_Interval(3); C_Polyhedron ph(2); ph.generalized_refine_with_linear_form_inequality( - lk, la, GREATER_THAN); - tmp = 1; - lk -= tmp; + FP_Linear_Form(tmp), la, GREATER_THAN); + tmp = -1; + tmp /= FP_Interval(3); ph.generalized_refine_with_linear_form_inequality( - lk, -la, GREATER_OR_EQUAL); + FP_Linear_Form(tmp), -la, GREATER_OR_EQUAL); + tmp = 1; + tmp /= FP_Interval(3); ph.generalized_refine_with_linear_form_inequality( - lb, -lk, LESS_OR_EQUAL); + lb, FP_Linear_Form(tmp), LESS_OR_EQUAL); tmp = 0; - lk = FP_Linear_Form(tmp); ph.generalized_refine_with_linear_form_inequality( - -lb, lk, LESS_THAN); - print_constraints(ph, "*** ph ***"); + -lb, FP_Linear_Form(tmp), LESS_THAN); C_Polyhedron known_result1(2); known_result1.add_constraint(3*A >= 1); @@ -148,11 +147,17 @@ test04() { known_result1.add_constraint(3*B <= 1); print_constraints(known_result1, "*** known_result1 ***"); + Box<FP_Interval> box(ph); + print_constraints(ph, "*** ph ***"); + print_constraints(box, "*** box ***"); + bool ok1 = ph.contains(known_result1); ph.refine_fp_interval_abstract_store(store); nout << "*** FP_Interval_Abstract_Store ***" << endl; + nout << "tmp0 = " << tmp0 << endl; + nout << "A = " << store.get_interval(A) << endl; bool ok2 = tmp0.contains(store.get_interval(A));

1 0

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

29 Jun '12

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ae7b3951caad… Merge: 734d8127c33feaf13a2125c403dfc229c700cf09 3349ebad2d6197b22f4453e61f40ea5782bdf3e5 Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 29 14:45:34 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=3349ebad2d61… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 29 14:36:58 2012 +0200 Use std::floor() and std::frexp() instead of floorl() and frexpl(), respectively. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=70012d3f48c6… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 29 10:02:33 2012 +0200 Typo fixed. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2b53a49d3837… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 29 10:01:54 2012 +0200 Typo fixed. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=88b390acbeb6… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Jun 28 14:20:36 2012 +0200 Spurious blank line removed. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c8e7c38d59d1… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Jun 28 14:19:30 2012 +0200 Added AmatoPS12.

1 0

[GIT] ppl/ppl(master): Use std::floor() and std::frexp() instead of floorl( ) and frexpl(), respectively.
by Roberto Bagnara 29 Jun '12

29 Jun '12

Module: ppl/ppl Branch: master Commit: 3349ebad2d6197b22f4453e61f40ea5782bdf3e5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3349ebad2d61… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 29 14:36:58 2012 +0200 Use std::floor() and std::frexp() instead of floorl() and frexpl(), respectively. --- src/checked_float.inlines.hh | 6 ++---- 1 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/checked_float.inlines.hh b/src/checked_float.inlines.hh index 42fd370..254e8c4 100644 --- a/src/checked_float.inlines.hh +++ b/src/checked_float.inlines.hh @@ -25,9 +25,7 @@ site: http://bugseng.com/products/ppl/ . */ #define PPL_checked_float_inlines_hh 1 #include "compiler.hh" -#ifndef __alpha #include <cmath> -#endif namespace Parma_Polyhedra_Library { @@ -1009,7 +1007,7 @@ assign_mpq_numeric_float(mpq_class& to, const long double from) { mpz_class& num = to.get_num(); mpz_class& den = to.get_den(); int exp; - long double n = frexpl(from, &exp); + long double n = std::frexp(from, &exp); bool neg = false; if (n < 0) { neg = true; @@ -1020,7 +1018,7 @@ assign_mpq_numeric_float(mpq_class& to, const long double from) { while (true) { n *= mult; exp -= bits; - long double intpart = floorl(n); + long double intpart = std::floor(n); num += (unsigned long)intpart; n -= intpart; if (n == 0)

1 0

[GIT] ppl/ppl(ppl-1_0-branch): Typo fixed.
by Roberto Bagnara 29 Jun '12

29 Jun '12

Module: ppl/ppl Branch: ppl-1_0-branch Commit: 734d8127c33feaf13a2125c403dfc229c700cf09 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=734d8127c33f… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 29 10:02:33 2012 +0200 Typo fixed. --- doc/Makefile.am | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/Makefile.am b/doc/Makefile.am index 9cde930..2fd6802 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -72,7 +72,7 @@ gpl.dox \ fdl.dox # NOTE: this variable is used to populate Doxygen configuration tag INPUT. -# The file path is that of the build directory, hence we ca not use +# The file path is that of the build directory, hence we cannot use # variable DOX_LICENSE_FILES defined above. DOX_LICENSE_INPUT = \ $(srcdir)/gpl.dox \

1 0

[GIT] ppl/ppl(ppl-1_0-branch): Typo fixed.
by Roberto Bagnara 29 Jun '12

29 Jun '12

Module: ppl/ppl Branch: ppl-1_0-branch Commit: 78dcbda0b861c2280a6598ed04b34be992538062 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=78dcbda0b861… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 29 10:01:54 2012 +0200 Typo fixed. --- doc/ppl_citations.bib | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 712dab4..51b2cff 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -2191,7 +2191,7 @@ Summarizing: Title = "Software Model Checking", Journal = "ACM Computing Surveys", Volume = 41, - Nnumber = 4, + Number = 4, Year = 2009, Pages = "1--54", Publisher = "ACM Press",

1 0

[GIT] ppl/ppl(ppl-1_0-branch): Spurious blank line removed.
by Roberto Bagnara 29 Jun '12

29 Jun '12

Module: ppl/ppl Branch: ppl-1_0-branch Commit: 1f4ca8be811bbc60056b0ddb38129f21587b513a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1f4ca8be811b… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Jun 28 14:20:36 2012 +0200 Spurious blank line removed. --- doc/ppl_citations.bib | 1 - 1 files changed, 0 insertions(+), 1 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 2e081fb..712dab4 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -304,7 +304,6 @@ Summarizing: programs and show some experimental evaluations." } - @Inproceedings{AmatoS12, Author = "G. Amato and F. Scozzari", Title = "Random: R-Based Analyzer for Numerical Domains",

1 0

[GIT] ppl/ppl(ppl-1_0-branch): Added AmatoPS12.
by Roberto Bagnara 29 Jun '12

29 Jun '12

Module: ppl/ppl Branch: ppl-1_0-branch Commit: 4bb66427092501c8c9fd641c0ae58ffd1370c186 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4bb664270925… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Jun 28 14:19:30 2012 +0200 Added AmatoPS12. --- doc/ppl_citations.bib | 20 ++++++++++++++++++++ 1 files changed, 20 insertions(+), 0 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 0e8e854..2e081fb 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -285,6 +285,26 @@ Summarizing: programs." } +@Article{AmatoPS12, + Author = "G. Amato and M. Parton and F. Scozzari", + Title = "Discovering Invariants via Simple Component Analysis", + Journal = "Journal of Symbolic Computation", + Volume = 47, + Number = 12, + Year = 2012, + Pages = "1533--1560", + Abstract = "We propose a new technique combining dynamic and static + analysis of programs to find linear invariants. We use a + statistical tool, called simple component analysis, to + analyze partial execution traces of a given program. We + get a new coordinate system in the vector space of + program variables, which is used to specialize numerical + abstract domains. As an application, we instantiate our + technique to interval analysis of simple imperative + programs and show some experimental evaluations." +} + + @Inproceedings{AmatoS12, Author = "G. Amato and F. Scozzari", Title = "Random: R-Based Analyzer for Numerical Domains",

1 0

[GIT] ppl/ppl(master): Typo fixed.
by Roberto Bagnara 29 Jun '12

29 Jun '12

Module: ppl/ppl Branch: master Commit: 70012d3f48c6aee21fd8e82617f70141461926fe URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=70012d3f48c6… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 29 10:02:33 2012 +0200 Typo fixed. --- doc/Makefile.am | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/Makefile.am b/doc/Makefile.am index 9cde930..2fd6802 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -72,7 +72,7 @@ gpl.dox \ fdl.dox # NOTE: this variable is used to populate Doxygen configuration tag INPUT. -# The file path is that of the build directory, hence we ca not use +# The file path is that of the build directory, hence we cannot use # variable DOX_LICENSE_FILES defined above. DOX_LICENSE_INPUT = \ $(srcdir)/gpl.dox \

1 0

[GIT] ppl/ppl(master): Typo fixed.
by Roberto Bagnara 29 Jun '12

29 Jun '12

Module: ppl/ppl Branch: master Commit: 2b53a49d3837c63dedad3ec660305c844b9d1e88 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2b53a49d3837… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 29 10:01:54 2012 +0200 Typo fixed. --- doc/ppl_citations.bib | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 712dab4..51b2cff 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -2191,7 +2191,7 @@ Summarizing: Title = "Software Model Checking", Journal = "ACM Computing Surveys", Volume = 41, - Nnumber = 4, + Number = 4, Year = 2009, Pages = "1--54", Publisher = "ACM Press",

1 0