Next: , Previous: , Up: Managers and Abstract Domains  

PPL (ap_ppl.h): convex polyhedra and linear congruences abstract domains

The APRON PPL library is an APRON wrapper around the Parma Polyhedra Library (PPL). The wrapper offers the convex polyhedra and linear congruences abstract domains.


Next: , Up: PPL  

Use of APRON PPL

To use APRON PPL in C, you need of course to install PPL, after having patched it following the recommendations of the README file. You need also to add

#include "apron_ppl.h"

in your source file(s) and add ‘-I$(APRON_PREFIX)/include’ in the command line in your Makefile.

You should also link your object files with the APRON PPL library to produce an executable, usingg++’ (instead of ‘gcc’, because libppl.a is a C++ library), and adding something like ‘-L$(APRON_PREFIX)/lib -lapron_ppl -L$(PPL_PREFIX)/lib -lppl -L$(GMP_PREFIX)/lib -lgmpxx’ in the command line in your Makefile (followed by the standard ‘-lapron -litvmpq -litvdbl -L$(MPFR_PREFIX)/lib -lmpfr -L$(GMP_PREFIX)/lib -lgmp’). The libgmpxx.a library is the C++ wrapper on top of the GMP library. Ensure that your GMP installation contains it, as it is not always installed by default.

All scalars of type double are converted to scalars of type mpq_t inside APRON PPL, as APRON PPL works internally with exact rational arithmetics. So when possible it is better for the user (in term of efficiency) to convert already double scalars to mpq_t scalars.

The wrapper library is available in debug mode (‘libapron_ppl_debug.a’).


Next: , Previous: , Up: PPL  

Allocating APRON PPL managers

Function: ap_manager_t* ap_ppl_poly_manager_alloc (bool strict)

Allocate a APRON manager for convex polyhedra, linked to the PPL library.

The strict option, when true, enables strict constraints in polyhedra (like x>0). Managers in strict mode or in loose mode (strict constraints disabled) are not compatible, and so are corresponding abstract values.

Function: ap_manager_t* ap_ppl_grid_manager_alloc ()

Allocate an APRON manager for linear equalities, linked to the PPL library.


Previous: , Up: PPL  

APRON PPL standard options

Currently, the only options available are related to the widening operators.

FunctionalgoComments
widening<=0CH78 standard widening (Cousot & Halbwachs, POPL’1978).
>0BHRZ03 widening (Bagnara, Hill, Ricci & Zafanella, SAS’2003)
widening_threshold<=0standard widening with threshold
=1standard widening with threshold, intersected by the bounding box of the convex hull pof the two arguments
<=0standard widening with threshold
=1standard widening with threshold, intersected by the bounding box of the convex hull of the second argument. This is actually an extrapolation rather than a widening (termination is not guaranteed)
=2BHRZ03 widening with threshold
=3BHRZ03 widening with threshold, intersected by the bounding box of the convex hull of the second argument. This is actually an extrapolation rather than a widening (termination is not guaranteed)

Previous: , Up: PPL