February 2016 - PPL-devel - BUGSENG Mailman

C_Polyhedron ray and lines
by Thomas LE MÉZO 01 Mar '16

01 Mar '16

Dear PPL-developers, I'm currently working on guaranteed integration using interval analysis. I need to compute the projection and intersection of close polyhedron and that is why it appears the PPL library could do the job. However, I need to work with floating numbers and I would like to know if there is a way to use floating numbers in the building vector of a "ray" or a "line" ? (or any alternative method which does not imply to compute the projection for each points of the polyhedron). Thank you in advance, Thomas

2 2

Complement of a logical Equation
by Rao,Nakul I 01 Mar '16

01 Mar '16

Hi I am using Parma Polyhedra library in a Formal Verification project. I was unable to find a function that computes the complement of a logical equation. For example, complement of a=5 will be a!=5. Could you tell me how I could do this. Thanks and Regards Nakul

3 2

[GIT] ppl/ppl(master): Added missing macro definition.
by Roberto Bagnara 14 Feb '16

14 Feb '16

Module: ppl/ppl Branch: master Commit: ca9227e0a5828b6653ae4ca7cf52b8c0840b871b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ca9227e0a582… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Feb 14 17:04:37 2016 +0100 Added missing macro definition. Fixes violations of rule MP1.16-0-7 detected by ECLAIR. --- configure.ac | 12 ++++++++---- 1 files changed, 8 insertions(+), 4 deletions(-) diff --git a/configure.ac b/configure.ac index 5081714..5d350ef 100644 --- a/configure.ac +++ b/configure.ac @@ -84,21 +84,25 @@ AH_TOP([ #ifndef PPL_ppl_config_h #define PPL_ppl_config_h 1 +/* Unique (nonzero) code for the IEEE 754 Half Precision + floating point format. */ +#define PPL_FLOAT_IEEE754_HALF 1 + /* Unique (nonzero) code for the IEEE 754 Single Precision floating point format. */ -#define PPL_FLOAT_IEEE754_SINGLE 1 +#define PPL_FLOAT_IEEE754_SINGLE 2 /* Unique (nonzero) code for the IEEE 754 Double Precision floating point format. */ -#define PPL_FLOAT_IEEE754_DOUBLE 2 +#define PPL_FLOAT_IEEE754_DOUBLE 3 /* Unique (nonzero) code for the IEEE 754 Quad Precision floating point format. */ -#define PPL_FLOAT_IEEE754_QUAD 3 +#define PPL_FLOAT_IEEE754_QUAD 4 /* Unique (nonzero) code for the Intel Double-Extended floating point format. */ -#define PPL_FLOAT_INTEL_DOUBLE_EXTENDED 4 +#define PPL_FLOAT_INTEL_DOUBLE_EXTENDED 5 ]) AH_BOTTOM([

1 0

[GIT] ppl/ppl(master): Added `virtual' to overriding virtual funcion declarations.
by Roberto Bagnara 13 Feb '16

13 Feb '16

Module: ppl/ppl Branch: master Commit: 529bc41610bf74f9b284246ff222a4b04bed506d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=529bc41610bf… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Feb 13 11:06:56 2016 +0100 Added `virtual' to overriding virtual funcion declarations. Fixes violations of rule MP1.10-3-2 detected by ECLAIR. --- demos/ppl_pips/ppl_pips.cc | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/demos/ppl_pips/ppl_pips.cc b/demos/ppl_pips/ppl_pips.cc index 188eebe..ddfb70a 100644 --- a/demos/ppl_pips/ppl_pips.cc +++ b/demos/ppl_pips/ppl_pips.cc @@ -258,7 +258,7 @@ public: PIP_PolyLib_Parser(): PIP_Parser() { } - bool read(std::istream& in) { + virtual bool read(std::istream& in) { std::string line; PPL::dimension_type num_ctx_rows; @@ -339,7 +339,7 @@ public: : PIP_Parser(), comment() { } - bool read(std::istream& in) { + virtual bool read(std::istream& in) { if (!expect(in, '(')) { return false; }

1 0

[GIT] ppl/ppl(master): Fixed hexadecimal integer literal.
by Roberto Bagnara 13 Feb '16

13 Feb '16

Module: ppl/ppl Branch: master Commit: 223ee038719298d2bc6146689aa4e5109332b71b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=223ee0387192… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Feb 13 11:03:14 2016 +0100 Fixed hexadecimal integer literal. Fixes a violation of rule MP1.2-13-3 detected by ECLAIR. --- src/checked_int_inlines.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/checked_int_inlines.hh b/src/checked_int_inlines.hh index 885d7dc..c0eae32 100644 --- a/src/checked_int_inlines.hh +++ b/src/checked_int_inlines.hh @@ -797,7 +797,7 @@ PPL_SPECIALIZE_ASSIGN(assign_int_mpq, unsigned long long, mpq_class) #error "Unexpected max for unsigned short" #endif -#if UINT_MAX == 0xffffffff +#if UINT_MAX == 0xffffffffU #define INT_BITS 32 #else #error "Unexpected max for unsigned int"

1 0

[GIT] ppl/ppl(master): Include <cstring> instead of <string.h>.
by Roberto Bagnara 13 Feb '16

13 Feb '16

Module: ppl/ppl Branch: master Commit: b5451eae8eb5e136dbb987edaab7ce523c6be108 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b5451eae8eb5… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Feb 13 11:01:16 2016 +0100 Include <cstring> instead of <string.h>. Fixes a violation of rule MP1.18-0-1 detected by ECLAIR. --- src/Watchdog.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/Watchdog.cc b/src/Watchdog.cc index 6643dc2..26e370a 100644 --- a/src/Watchdog.cc +++ b/src/Watchdog.cc @@ -31,7 +31,7 @@ site: http://bugseng.com/products/ppl/ . */ #include <stdexcept> #include <cerrno> #include <string> -#include <string.h> +#include <cstring> #ifdef PPL_TIME_WITH_SYS_TIME # include <sys/time.h>

1 0

[GIT] ppl/ppl(master): Const correctness improved.
by Roberto Bagnara 13 Feb '16

13 Feb '16

Module: ppl/ppl Branch: master Commit: d20a0a11262ad86a3439a1ddfe57448c753cb1e4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d20a0a11262a… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Feb 13 08:24:47 2016 +0100 Const correctness improved. Fixes violations of rule MP1.7-1-1 detected by ECLAIR. --- demos/ppl_lcdd/ppl_lcdd.cc | 18 ++-- demos/ppl_pips/ppl_pips.cc | 30 ++++---- src/BDS_Status_inlines.hh | 2 +- src/Bit_Matrix.cc | 8 +- src/Bit_Row_inlines.hh | 16 ++-- src/Boundary_defs.hh | 147 ++++++++++++++++++----------------- src/Box_Status_inlines.hh | 2 +- src/CO_Tree.cc | 58 +++++++------- src/CO_Tree_inlines.hh | 55 +++++++------ src/CO_Tree_templates.hh | 2 +- src/C_Polyhedron_inlines.hh | 4 +- src/Checked_Number.cc | 2 +- src/Checked_Number_inlines.hh | 8 +- src/Concrete_Expression_inlines.hh | 2 +- src/Congruence.cc | 18 ++-- src/Congruence_System.cc | 11 ++- src/Congruence_System_inlines.hh | 17 +++-- src/Congruence_inlines.hh | 24 +++--- src/Constraint.cc | 14 ++-- src/Constraint_System.cc | 2 +- src/Constraint_System_inlines.hh | 40 +++++---- src/Constraint_inlines.hh | 26 ++++--- src/Dense_Row.cc | 27 ++++--- src/Dense_Row_inlines.hh | 54 ++++++------- src/Doubly_Linked_Object_inlines.hh | 4 +- src/Generator.cc | 28 ++++---- src/Generator_System.cc | 2 +- src/Generator_System_inlines.hh | 38 +++++---- src/Generator_inlines.hh | 46 ++++++----- src/Grid_Generator.cc | 24 +++--- src/Grid_Generator_System.cc | 2 +- src/checked_mpq_inlines.hh | 10 +- 32 files changed, 381 insertions(+), 360 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=d20a0a11…

1 0

some questions regarding PPL
by Bishoksan Kafle 12 Feb '16

12 Feb '16

Hi PPL-developers I would be glad if you could help me find answers to the following questions: 1. Having software verification in mind (problems over integers) which abstract domain(s) (more precisely domains provided by PPL) provide good trade-off between complexity and expressiveness? 2. In the article (http://bugseng.com/products/ppl/documentation/BagnaraRZH02.pdf), you mentioned that poly_hull_assign is different from upper_bound_assign for Polyhedra, but in the user manual I found the following text: [cid:BC9F6334-FB66-4E2B-BE47-2E4A8D844CD6] What are the differences between these two functions? Do they differ in precision? complexity? 3. What is the function corresponding to poly_hull_assign for Octagon? Many thanks in advance Bishoksan

2 5

[GIT] ppl/ppl(master): Updated.
by Roberto Bagnara 12 Feb '16

12 Feb '16

Module: ppl/ppl Branch: master Commit: 72041c4d0d7fc5c1ec4c172248275bcdf41e7300 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=72041c4d0d7f… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Fri Feb 12 10:03:55 2016 +0100 Updated. --- NEWS | 16 ++++++++++++++++ configure.ac | 2 +- interfaces/C/Makefile.am | 8 +++++++- src/Makefile.am | 3 ++- 4 files changed, 26 insertions(+), 3 deletions(-) diff --git a/NEWS b/NEWS index baff7b0..58d532e 100644 --- a/NEWS +++ b/NEWS @@ -9,6 +9,22 @@ Parma Polyhedra Library NEWS -- history of user-visible changes =============================================================== -------------------------------------------------------------------------- +NEWS for version 1.3 (released date to be decided) +-------------------------------------------------------------------------- + +New and Changed Features +======================== + +o TBW + + +Bugfixes +======== + +o TBW + + +-------------------------------------------------------------------------- NEWS for version 1.2 (released on February 11, 2016) -------------------------------------------------------------------------- diff --git a/configure.ac b/configure.ac index c00a204..5081714 100644 --- a/configure.ac +++ b/configure.ac @@ -24,7 +24,7 @@ # Process this file with Autoconf to produce a configure script. # Every other copy of the package version number gets its value from here. -AC_INIT([the Parma Polyhedra Library], [1.2], [ppl-devel(a)cs.unipr.it], [ppl]) +AC_INIT([the Parma Polyhedra Library], [1.3pre1], [ppl-devel(a)cs.unipr.it], [ppl]) # Minimum Autoconf version required. AC_PREREQ(2.61) diff --git a/interfaces/C/Makefile.am b/interfaces/C/Makefile.am index 431b54b..2f2431d 100644 --- a/interfaces/C/Makefile.am +++ b/interfaces/C/Makefile.am @@ -72,8 +72,14 @@ C_interface.dox # 0.10.1 2:0:0 (was not updated by mistake) # 0.10.2 3:0:1 # 0.11 4:0:0 - -LIBPPL_C_LT_CURRENT = 4 +# 0.12 4:0:0 (was not updated by mistake) +# 0.12.1 4:0:0 (was not updated by mistake) +# 1.0 4:0:0 (was not updated by mistake) +# 1.1 4:0:0 (was not updated by mistake) +# 1.2 4:0:0 (was not updated by mistake) +# 1.3 5:0:0 + +LIBPPL_C_LT_CURRENT = 5 LIBPPL_C_LT_REVISION = 0 LIBPPL_C_LT_AGE = 0 diff --git a/src/Makefile.am b/src/Makefile.am index 119fc32..5f3e650 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -61,8 +61,9 @@ # 1.0 12:0:0 # 1.1 13:0:0 # 1.2 14:0:0 +# 1.3 15:0:0 -LIBPPL_LT_CURRENT = 14 +LIBPPL_LT_CURRENT = 15 LIBPPL_LT_REVISION = 0 LIBPPL_LT_AGE = 0

1 0

Parma Polyhedra Library 1.2
by Roberto Bagnara 11 Feb '16

11 Feb '16

The core development team is very pleased to announce the availability of the long-awaited release 1.2 of the Parma Polyhedra Library. This release includes a major efficiency improvement to the conversion procedure for polyhedra, a few bugfixes and numerous portability improvements. The precise list of user-visible changes is below. For more information, please come and visit the PPL web site at http://bugseng.com/products/ppl On behalf of all the past and present developers listed at http://bugseng.com/products/ppl/credits and in the file CREDITS, Roberto Bagnara Patricia M. Hill Enea Zaffanella Abramo Bagnara -------------------------------------------------------------------------- NEWS for version 1.2 (released on February 11, 2016) -------------------------------------------------------------------------- New and Changed Features ======================== o Improved the efficiency of the conversion procedure for polyhedra by adding a quick adjacency check. o In the Java language interface, throw an exception when trying to build a disequality Constraint. Bugfixes ======== o Fixed a bug in the implementation of methods Pointset_Powerset<PSET>::relation_with(const Constraint&) const; and Pointset_Powerset<PSET>::relation_with(const Congruence&) const; whereby the computed result for relations strictly_intersects() and saturates() could have been wrong. o Fixed a bug in the implementation of dense rows. o Portability improved. -- 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

1 0