March 2013 - PPL-devel - BUGSENG Mailman

Parma Polyhedra Library
by varza victor 28 Mar '13

28 Mar '13

Hi, My name is Victor Varza, I'm student at Politehnica University of Bucharest and I working at a research about actual fuzzing testing tools and methods.I want to use your library (PPL) to generate some test case from a given constraint sistem. I have searched in your papers to find how to do this but I haven't find something that could help me. I'm working in C++ and I need some example to generate data for a poliedrom. Could you please help me in this way? Best regards, VIctor T

2 4

Use of non-integers in Java
by Étienne André 14 Mar '13

14 Mar '13

Dear PPL developers, My intern would like to link PPL with a Java program. I have some experience of using PPL with OCaml, but not with Java. And in particular I could not find how to use non-integers coefficients (but rationals instead). In OCaml, it was easy, e.g., using the "Gmp.Q.from_ints i j" function. But in the Java interface, I only see constructors from int, big int, long and string. How can we build some rational coefficients in the Java interface? Thank you very much, -- Étienne André LIPN, Université Paris 13, Sorbonne Paris Cité http://www-lipn.univ-paris13.fr/~andre

2 2

Configure errors on Solaris 10
by Marc Girod 10 Mar '13

10 Mar '13

Hello, I get two warnings and on error while configuring ppl-1.0 for Solaris 10, with gcc 3.4.3 My command: ppl-1.0> ./configure --prefix=/vobs/cello/cade_A_tools_utils/ppl --with-gmp=/vobs/cello/cade_A_tools_utils/gmp CFLAGS='-O2 -pedantic -m64 -mptr64 -mcpu=ultrasparc' CC='/usr/sfw/bin/gcc -std=gnu99' The warnings: configure: WARNING: ieeefp.h: present but cannot be compiled configure: WARNING: ieeefp.h: check for missing prerequisite headers? configure: WARNING: ieeefp.h: see the Autoconf documentation configure: WARNING: ieeefp.h: section "Present But Cannot Be Compiled" configure: WARNING: ieeefp.h: proceeding with the compiler's result configure: WARNING: ## ------------------------------------ ## configure: WARNING: ## Report this to ppl-devel(a)cs.unipr.it ## configure: WARNING: ## ------------------------------------ ## configure: WARNING: getopt.h: present but cannot be compiled configure: WARNING: getopt.h: check for missing prerequisite headers? configure: WARNING: getopt.h: see the Autoconf documentation configure: WARNING: getopt.h: section "Present But Cannot Be Compiled" configure: WARNING: getopt.h: proceeding with the compiler's result configure: WARNING: ## ------------------------------------ ## configure: WARNING: ## Report this to ppl-devel(a)cs.unipr.it ## configure: WARNING: ## ------------------------------------ ## The error: checking for the GMP library version 4.1.3 or above... no configure: error: Cannot find GMP version 4.1.3 or higher. I assume the two headers are the ones in /usr/include, and part of: ppl-1.0> pkginfo -l SUNWhea PKGINST: SUNWhea NAME: SunOS Header Files CATEGORY: system ARCH: sparc VERSION: 11.10.0,REV=2005.01.21.15.53 BASEDIR: / VENDOR: Oracle Corporation DESC: SunOS C/C++ header files for general development of software PSTAMP: on10-patch20120806013413 INSTDATE: Aug 25 2012 11:34 HOTLINE: Please contact your local service provider STATUS: completely installed FILES: 1623 installed pathnames 43 shared pathnames 128 directories 22681 blocks used (approx) GMP I just installed and it is 5.1.1 gmp-5.1.1> ll /vobs/cello/cade_A_tools_utils/gmp/lib total 3102 drwxrwxr-x 2 emagiro ossdes 154 Mar 4 19:02 . drwxrwxr-x 5 emagiro ossdes 75 Mar 4 19:02 .. -r--r--r-- 1 emagiro ossdes 1040202 Mar 4 18:49 libgmp.a -r-xr-xr-x 1 emagiro ossdes 938 Mar 4 18:49 libgmp.la lr-xr-xr-x 1 emagiro ossdes 16 Mar 4 19:02 libgmp.so -> libgmp.so.10.1.1 lr-xr-xr-x 1 emagiro ossdes 16 Mar 4 19:02 libgmp.so.10 -> libgmp.so.10.1.1 -r-xr-xr-x 1 emagiro ossdes 544608 Mar 4 18:49 libgmp.so.10.1.1 I attache my config.log Thanks, Marc

2 3

[GIT] ppl/ppl(master): Fixed constructor from a different partially reduced product element.
by Enea Zaffanella 03 Mar '13

03 Mar '13

Module: ppl/ppl Branch: master Commit: eaac930eb9a08b129381fc9cf96d6cfa45f57d6a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=eaac930eb9a0… Author: Enea Zaffanella <enea.zaffanella(a)bugseng.com> Date: Sun Mar 3 16:03:15 2013 +0100 Fixed constructor from a different partially reduced product element. --- src/Partially_Reduced_Product_inlines.hh | 5 +---- 1 files changed, 1 insertions(+), 4 deletions(-) diff --git a/src/Partially_Reduced_Product_inlines.hh b/src/Partially_Reduced_Product_inlines.hh index 591fbba..378b5a7 100644 --- a/src/Partially_Reduced_Product_inlines.hh +++ b/src/Partially_Reduced_Product_inlines.hh @@ -156,14 +156,11 @@ inline Partially_Reduced_Product<D1, D2, R> ::Partially_Reduced_Product(const Partially_Reduced_Product<E1, E2, S>& y, Complexity_Class complexity) - : d1(y.space_dimension()), d2(y.space_dimension()) { + : d1(y.space_dimension()), d2(y.space_dimension()), reduced(false) { Partially_Reduced_Product<D1, D2, R> pg1(y.domain1(), complexity); Partially_Reduced_Product<D1, D2, R> pg2(y.domain2(), complexity); pg1.intersection_assign(pg2); m_swap(pg1); - /* Even if y is reduced, the built product may not be reduced as - the reduction method may have changed (i.e., S != R). */ - clear_reduced_flag(); } template <typename D1, typename D2, typename R>

1 0

[GIT] ppl/ppl(master): Fix indentation.
by Enea Zaffanella 03 Mar '13

03 Mar '13

Module: ppl/ppl Branch: master Commit: 87f09547a592229bfbd7722103f8e64ef074fb92 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=87f09547a592… Author: Enea Zaffanella <enea.zaffanella(a)bugseng.com> Date: Sun Mar 3 15:43:46 2013 +0100 Fix indentation. --- src/Bit_Matrix.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/Bit_Matrix.cc b/src/Bit_Matrix.cc index 4b4235f..85eedf0 100644 --- a/src/Bit_Matrix.cc +++ b/src/Bit_Matrix.cc @@ -124,7 +124,7 @@ PPL::Bit_Matrix::transpose_assign(const Bit_Matrix& y) { void PPL::Bit_Matrix::resize(dimension_type new_n_rows, - dimension_type new_n_columns) { + dimension_type new_n_columns) { PPL_ASSERT(OK()); const dimension_type old_num_rows = num_rows(); if (new_n_columns < row_size) {

1 0

[GIT] ppl/ppl(master): Activate a couple of tests that were ignored.
by Enea Zaffanella 03 Mar '13

03 Mar '13

Module: ppl/ppl Branch: master Commit: 464f7b65bde5166d2ac665289389f2b0c92a1c54 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=464f7b65bde5… Author: Enea Zaffanella <enea.zaffanella(a)bugseng.com> Date: Sun Mar 3 15:42:56 2013 +0100 Activate a couple of tests that were ignored. --- tests/Box/refinewithcongruences1.cc | 14 +++++++------- 1 files changed, 7 insertions(+), 7 deletions(-) diff --git a/tests/Box/refinewithcongruences1.cc b/tests/Box/refinewithcongruences1.cc index e94e270..3f4a8d0 100644 --- a/tests/Box/refinewithcongruences1.cc +++ b/tests/Box/refinewithcongruences1.cc @@ -122,7 +122,8 @@ test05() { cgs.insert(B %= 0); cgs.insert(C %= 7); - TBox box(cgs); + TBox box(3); + box.refine_with_congruences(cgs); TBox box1(box.congruences()); @@ -147,16 +148,13 @@ test06() { Congruence_System cgs; cgs.insert((A %= 7) / 0); cgs.insert((B %= 3) / 0); - // This inconsistent equality is ignored when congruences - // are added to the box. cgs.insert((A + B %= 0) / 0); cgs.insert(C %= 7); - TBox box(cgs); + TBox box(3); + box.refine_with_congruences(cgs); - Rational_Box known_result(3); - known_result.add_constraint(A == 7); - known_result.add_constraint(B == 3); + Rational_Box known_result(3, EMPTY); bool ok = check_result(box, known_result); @@ -376,6 +374,8 @@ BEGIN_MAIN DO_TEST(test02); DO_TEST(test03); DO_TEST(test04); + DO_TEST(test05); + DO_TEST(test06); DO_TEST(test07); DO_TEST(test08); DO_TEST(test09);

1 0