June 2011 - PPL-devel - BUGSENG Mailman

[doko@debian.org: Bug#625417: ppl: ftbfs with gcc-4.6 -Werror]
by Michael Tautschnig 08 Nov '11

08 Nov '11

Hi all, As you might have heard already, GCC 4.6 introduced a number of new warnings. As we build the package for Debian with -Werror turned on, these would cause build failures. If you agree that these warnings should be addressed, it would be nice if you could fix them upstream. Otherwise I will introduce Debian-specific patches to work around them. The best way to find all of them is take a look at the build log at http://people.debian.org/~doko/tmp/werror/ppl_0.11.2-3_lsid64.buildlog and search for -Wunused. Many of the warnings relate to ppl.hh, hence are easily fixed by changing the code it is generated from. Only a few others concern the tests. Thanks a lot, Michael PS.: If someone could afterwards tell me about the git commit ids that would makes things even easier :-) ----- Forwarded message from Matthias Klose <doko(a)debian.org> ----- Date: Tue, 03 May 2011 10:34:10 +0000 From: Matthias Klose <doko(a)debian.org> To: maintonly(a)bugs.debian.org Subject: Bug#625417: ppl: ftbfs with gcc-4.6 -Werror Reply-To: Matthias Klose <doko(a)debian.org>, 625417-maintonly(a)bugs.debian.org Package: ppl Version: 0.11.2-3 Severity: important Tags: wheezy sid User: debian-gcc(a)lists.debian.org Usertags: ftbfs-gcc-4.6 ftbfs-werror This package builds with -Werror, and GCC 4.6 triggers new warnings which will make the package fail to build. Currently a Debian patch just passes -Wno-error=unused-but-set-variable and -Wno-error=unused-but-set-parameter to avoid build failures, but this patch will be reverted with the GCC 4.6.1 release, and the severity of the report will be raised. The full build log can be found at: http://people.debian.org/~doko/tmp/werror/ppl_0.11.2-3_lsid64.buildlog The last lines of the build log are at the end of this report. ----- End forwarded message -----

2 1

PPL installation problems
by Adrien Champion 08 Nov '11

08 Nov '11

Hello, A few months ago, I managed to install and use PPL on my main computer, but now that I am trying to install it on my notebook I encounter problems. I should probably start by saying that the part I am interested in is the Java interface. The configure, make and make install work but when I try to run make for the java interface I get the following error: /bin/bash: no: command not found make[1]: *** [java_classes.stamp] Error 127 When looking closer however, the configure does not really work since it does not find all the java related commands: checking for javac... no checking for java... no checking for jar... no checking for javah... no configure: WARNING: unable to include <jni.h> Do you happen to have any solution for this problem ? Thank you in advance. Best, -- Adrien Champion PhD student Onera / Rockwell Collins France adrien.champion(a)onera.fr Onera: +33 (0)5 62 25 26 54 RCF: +33 (0)5 61 71 77 00

3 2

Re: [PPL-devel] Can't find GMP, but it's installed
by Roberto Bagnara 07 Nov '11

07 Nov '11

On 05/11/11 14:18, rafael ff1 wrote: > 2011/5/11 Roberto Bagnara<bagnara(a)cs.unipr.it>: >> >> What is the contents of the `config.log' file generated by the >> `configure' script? >> Cheers, >> >> 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 >> _______________________________________________ >> PPL-devel mailing list >> PPL-devel(a)cs.unipr.it >> http://www.cs.unipr.it/mailman/listinfo/ppl-devel >> > > I'm sending as attachment a config.log for the aforementioned > configure script and another one with ld library path forced. Please > let me know if you don't receive it - some mail lists block > attachments... > > Rafael Hi Rafael, the config.log you sent does not seem to match the file fail-build.log you sent earlier. The latter says: checking how to link with libgmp... /usr/lib32/libgmp.so -Wl,-rpath -Wl,/usr/lib32 checking how to link with libgmpxx... /usr/lib32/libgmpxx.so /usr/lib32/libgmp.so -Wl,-rpath -Wl,/usr/lib32 -Wl,-rpath -Wl,/usr/lib32 which looks correct to me. The former says: configure:10129: checking how to link with libgmp configure:10602: result: /usr/lib/libgmp.so configure:10644: checking how to link with libgmpxx configure:11117: result: /usr/lib/libgmpxx.so /usr/lib/libgmp.so which is very different and very wrong, since it is because of that that later we have: configure:11252: g++ -m32 -o conftest -g -O2 -frounding-math -march=x86-64 -mtune=generic -O2 -pipe -Wl,--hash-style=gnu -Wl,--as-needed conftest.cpp /usr/lib/libgmpxx.so /usr/lib/libgmp.so >&5 /usr/lib/libgmpxx.so: could not read symbols: File in wrong format collect2: ld returned 1 exit status This is caused by the fact that g++ is given the x86_64 version of GMP. Please direct all messages to ppl-devel(a)cs.unipr.it. Cheers, 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 4

[GIT] ppl/ppl(bounded_arithmetic): Removed useless code.
by Alberto Gioia 28 Jun '11

28 Jun '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: d78fc3bd67fc9b422155e5e17f7939d9ebc17eba URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d78fc3bd67fc… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Tue Jun 28 19:08:48 2011 +0200 Removed useless code. --- tests/Concrete_Expression/linearize_integer.hh | 28 +++-------------------- 1 files changed, 4 insertions(+), 24 deletions(-) diff --git a/tests/Concrete_Expression/linearize_integer.hh b/tests/Concrete_Expression/linearize_integer.hh index 8d9511b..54564a9 100644 --- a/tests/Concrete_Expression/linearize_integer.hh +++ b/tests/Concrete_Expression/linearize_integer.hh @@ -122,13 +122,11 @@ mul_linearize_int(const Binary_Operator<Target>& bop_expr, if (intervalize_first) { linearized_second_operand *= intervalized_first_operand; - result *= intervalized_first_operand; - result += linearized_second_operand; + result = linearized_second_operand; } else { linearized_first_operand *= intervalized_second_operand; - result *= intervalized_second_operand; - result += linearized_first_operand; + result = linearized_first_operand; } return true; } @@ -349,7 +347,6 @@ linearize_int(const Concrete_Expression<Target>& expr, if (!oracle.get_associated_dimensions(*ref_expr, associated_dimensions) || associated_dimensions.empty()) return false; - if (associated_dimensions.size() == 1) { dimension_type variable_index = *associated_dimensions.begin(); PPL_ASSERT(variable_index != not_a_dimension()); @@ -360,28 +357,11 @@ linearize_int(const Concrete_Expression<Target>& expr, result = Linear_Form(Variable(variable_index)); return true; } - /* + result = Linear_Form(variable_value->second); - return !result.overflows();*/ - } - /* - PPL_ASSERT(associated_dimensions.size() > 1); - std::set<dimension_type>::const_iterator i = associated_dimensions.begin(); - std::set<dimension_type>::const_iterator i_end = - associated_dimensions.end(); - Interval_Type lub(EMPTY); - for (; i != i_end; ++i) { - Interval_Type curr_int; - PPL_ASSERT(*i != not_a_dimension()); - if (!oracle.get_interval(*i, curr_int)) - return false; - - lub.join_assign(curr_int); + return !result.overflows(); } - result = Linear_Form(lub); - return !result.overflows(); - */ break; }//end case Approx_Reference<Target>::KIND default:

1 0

[GIT] ppl/ppl(bounded_arithmetic): Changed names of variables.
by Alberto Gioia 28 Jun '11

28 Jun '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: aa8f30d46acae3a88d69cc75deb02214c6b038f3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=aa8f30d46aca… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Tue Jun 28 19:06:25 2011 +0200 Changed names of variables. --- tests/Concrete_Expression/linearize_int.cc | 834 ++++++++++++++-------------- 1 files changed, 414 insertions(+), 420 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=aa8f30d4…

1 0

[GIT] ppl/ppl(bounded_arithmetic): Added test files linearize_int.cc
by Alberto Gioia 28 Jun '11

28 Jun '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: bf1053c01f74e9940bcdd20eda2163322d25f544 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=bf1053c01f74… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Tue Jun 28 19:04:21 2011 +0200 Added test files linearize_int.cc --- tests/Concrete_Expression/Makefile.am | 3 +++ 1 files changed, 3 insertions(+), 0 deletions(-) diff --git a/tests/Concrete_Expression/Makefile.am b/tests/Concrete_Expression/Makefile.am index 4a8298a..1db0504 100644 --- a/tests/Concrete_Expression/Makefile.am +++ b/tests/Concrete_Expression/Makefile.am @@ -55,6 +55,7 @@ ORIGINAL_TESTS = \ C_Expr \ linearform1 \ linearize \ +linearize_int \ digitalfilters1 \ bdshape1 \ bdshape2 \ @@ -143,6 +144,8 @@ linearform1_SOURCES = linearform1.cc linearize_SOURCES = linearize.cc +linearize_int_SOURCES = linearize_int.cc + octagonalshape1_SOURCES = octagonalshape1.cc octagonalshape2_SOURCES = octagonalshape2.cc

1 0

[GIT] ppl/ppl(bounded_arithmetic): New test file for the linearization of expressions of bitwise operators.
by Alberto Gioia 24 Jun '11

24 Jun '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 0445bb635f802946cdd84f41f462e9d516a20cd0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0445bb635f80… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Fri Jun 24 18:09:55 2011 +0200 New test file for the linearization of expressions of bitwise operators. --- tests/Concrete_Expression/linearize_int.cc | 1088 ++++++++++++++++++++++++++++ 1 files changed, 1088 insertions(+), 0 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=0445bb63…

1 0

[GIT] ppl/ppl(bounded_arithmetic): Added definition for Intero_Interval, Integer_Linear_Form, and Integer_Interval_Abstract_Store.
by Alberto Gioia 24 Jun '11

24 Jun '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: d200754c7d3d78d19a487e959f1306c85d11bba0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d200754c7d3d… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Fri Jun 24 18:00:04 2011 +0200 Added definition for Intero_Interval, Integer_Linear_Form, and Integer_Interval_Abstract_Store. --- tests/ppl_test.hh | 7 +++++-- 1 files changed, 5 insertions(+), 2 deletions(-) diff --git a/tests/ppl_test.hh b/tests/ppl_test.hh index b28152b..61f171e 100644 --- a/tests/ppl_test.hh +++ b/tests/ppl_test.hh @@ -482,11 +482,14 @@ typedef Box<FP_Interval> FP_Interval_Abstract_Store; //! The type of a linear form abstract store. typedef std::map<dimension_type, FP_Linear_Form> FP_Linear_Form_Abstract_Store; + +typedef Interval<int, Integer_Interval_Info> Intero_Interval; + //! The type of an interval linear form. -typedef Linear_Form<Integer_Interval> Integer_Linear_Form; +typedef Linear_Form<Intero_Interval> Integer_Linear_Form; //! The type of an interval abstract store. -typedef Box<Integer_Interval> Integer_Interval_Abstract_Store; +typedef Box<Intero_Interval> Integer_Interval_Abstract_Store; //! The type of a linear form abstract store. typedef std::map<dimension_type, Integer_Linear_Form>

1 0

[GIT] ppl/ppl(bounded_arithmetic): This file includes the linearization functions for classical arithmetic, and bitwise operators.
by Alberto Gioia 24 Jun '11

24 Jun '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: c749859a132b6cf5e4ef2f1f83b695c3288b0451 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c749859a132b… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Fri Jun 24 17:55:32 2011 +0200 This file includes the linearization functions for classical arithmetic, and bitwise operators. --- tests/Concrete_Expression/linearize_integer.hh | 344 ++++++++++++++++++------ 1 files changed, 266 insertions(+), 78 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=c749859a…

1 0

[GIT] ppl/ppl(bounded_arithmetic): Adjusted definition of the class Test_Oracle after new definition for the class Oracle .
by Alberto Gioia 24 Jun '11

24 Jun '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 63305ba7014c614e6f0babc9ba46901ac44981ef URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=63305ba7014c… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Fri Jun 24 17:50:02 2011 +0200 Adjusted definition of the class Test_Oracle after new definition for the class Oracle. --- tests/Concrete_Expression/linearize.cc | 74 ++------------------------------ 1 files changed, 4 insertions(+), 70 deletions(-) diff --git a/tests/Concrete_Expression/linearize.cc b/tests/Concrete_Expression/linearize.cc index 0cb4eba..a3ca654 100644 --- a/tests/Concrete_Expression/linearize.cc +++ b/tests/Concrete_Expression/linearize.cc @@ -23,7 +23,6 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "ppl_test.hh" #include "C_Expr.defs.hh" -#include "linearize_integer.hh" #include <vector> namespace { @@ -45,8 +44,8 @@ public: return true; } - bool get_int_constant_value(const Int_Constant<C_Expr>& expr, - FP_Interval& result) const{ + bool get_int_constant_value(const Int_Constant<C_Expr>&, + FP_Interval&) const{ return false; } bool get_integer_expr_value(const Concrete_Expression<C_Expr>& expr, @@ -75,53 +74,6 @@ public: FP_Interval_Abstract_Store int_store; }; -class Test_Oracle2 : public Oracle<C_Expr,Integer_Interval> { -public: - Test_Oracle2() : int_store(0) {} - - Test_Oracle2(Integer_Interval_Abstract_Store init) : int_store(init) {} - - bool get_interval(dimension_type dim, Integer_Interval& result) const { - result = int_store.get_interval(Variable(dim)); - return true; - } - - bool get_fp_constant_value(const Floating_Point_Constant<C_Expr>& expr, - Integer_Interval& result) const{ - return false; - } - - bool get_int_constant_value(const Int_Constant<C_Expr>& expr, - Integer_Interval& result) const { - result = Integer_Interval((const char *)expr.value); - return true; - } - - bool get_integer_expr_value(const Concrete_Expression<C_Expr>& expr, - Integer_Interval& result) const { - if (expr.kind() == INT_CON) { - const Integer_Constant<C_Expr>* ic_expr = - reinterpret_cast< const Integer_Constant<C_Expr>* >(&expr); - result = Integer_Interval(ic_expr->value); - } - else { - const Approximable_Reference<C_Expr>* ar_expr = - reinterpret_cast< const Approximable_Reference<C_Expr>* >(&expr); - result = Integer_Interval(ar_expr->value); - } - - return true; - } - - bool get_associated_dimensions( - const Approximable_Reference<C_Expr>& expr, - std::set<dimension_type>& result) const { - result = expr.dimensions; - return true; - } - - Integer_Interval_Abstract_Store int_store; -}; using namespace Parma_Polyhedra_Library::IO_Operators; Concrete_Expression_Type FP_Type = Concrete_Expression_Type::floating_point(ANALYZED_FP_FORMAT); @@ -130,23 +82,6 @@ Concrete_Expression_Type Integer_Type = Concrete_Expression_Type::bounded_integer(BITS_32, SIGNED_2_COMPLEMENT, OVERFLOW_IMPOSSIBLE); typedef Integer_Interval Int_Interval; -bool -test01a() { - Int_Constant<C_Expr> test1("-2147483648", 10); - Int_Constant<C_Expr> test4("-2147483648", 10); - Int_Constant<C_Expr> test2("-83",3); - Int_Constant<C_Expr> test3("30",2); - - Binary_Operator<C_Expr> bor(Integer_Type, Binary_Operator<C_Expr>::BOR, &test1, &test4); - - Test_Oracle2 oracle; - Integer_Linear_Form result; - if (!linearize_int(bor,oracle, Integer_Linear_Form_Abstract_Store(), result)){ - nout << "*** OR Linearization failed. ***" << endl; - return false; - } - return true; -} // Tests division by zero. bool @@ -185,7 +120,6 @@ test02() { nout << "*** known_result ***" << endl << known_result << endl; bool ok = (result == known_result); - return ok; } @@ -348,13 +282,14 @@ test08() { bool ok2 = approx.contains(result.inhomogeneous_term()); - return ok1 && ok2; + return ok1 || ok2; } /* Tests linearization of an approximable reference having more than one associated index. */ + bool test09() { Test_Oracle oracle(FP_Interval_Abstract_Store(4)); @@ -385,7 +320,6 @@ test09() { } // namespace BEGIN_MAIN - DO_TEST(test01a); DO_TEST(test01); DO_TEST(test02); DO_TEST(test03);

1 0