Next: pkgrid, Previous: NewPolka, Up: Managers and 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.
| • Use of APRON PPL | ||
| • Allocating APRON PPL managers | ||
| • APRON PPL standard options |
Next: Allocating APRON PPL managers, Up: 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, using ‘g++’ (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: APRON PPL standard options, Previous: Use of APRON PPL, Up: PPL
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.
Allocate an APRON manager for linear equalities, linked to the PPL library.
Previous: Allocating APRON PPL managers, Up: PPL
Currently, the only options available are related to the widening operators.
| Function | algo | Comments |
| widening | <=0 | CH78 standard widening (Cousot & Halbwachs, POPL’1978). |
| >0 | BHRZ03 widening (Bagnara, Hill, Ricci & Zafanella, SAS’2003) | |
| widening_threshold | <=0 | standard widening with threshold |
| =1 | standard widening with threshold, intersected by the bounding box of the convex hull pof the two arguments | |
| <=0 | standard widening with threshold | |
| =1 | standard 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) | |
| =2 | BHRZ03 widening with threshold | |
| =3 | BHRZ03 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: Allocating APRON PPL managers, Up: PPL