Use of APRON PPLite ¶

To use APRON PPLite you need to install PPLite and its dependencies Flint and GMP; currently, the APRON wrapper requires PPLite version 0.12. You need to add

#include "ap_pplite.h"

in your C source file(s) and add ‘-I$(APRON_PREFIX)/include’ in the command line specified in your Majefile to compile C code.

Your object files should be linked with the APRON PPLite library using ‘g++’ (instead of ‘gcc’) because libpplite.a is a C++ library, adding link options ‘-L$(APRON_PREFIX)/lib -lap_pplite -L$(PPLITE_PREFIX)/lib -lpplite -L$(FLINT_PREFIX)/lib -lflint’ (followed by the standard ‘-lapron -litvmpq -litvdbl -L$(MPFR_PREFIX)/lib -lmpfr -L$(GMP_PREFIX)/lib -lgmp’).

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

Allocating APRON PPLite managers ¶

Function: ap_manager_t* ap_pplite_manager_alloc (bool strict) ¶

Allocate an APRON manager for convex polyhedra linked to the PPLite 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: void ap_pplite_manager_set_kind (ap_manager_t* man, const char* name) ¶

Set the abstract domain polyhedron kind (i.e., variant implementation) to name. The default kind is "Poly"; other legal values are "F_Poly" (applies Cartesian factoring), "U_Poly" (avoids wasting space for unconstrained dimensions), "P_Set" (uses finite powerset of polyhedra), "FP_Set" (uses finite powerset of Cartesian factored polyhedra). Note that objects of different kinds are incompatible and should not be mixed in computations: hence, the kind should be set (if ever) at the beginning of the computation and then never changed; also note that powerset domains are experimental.

Function: const char* ap_pplite_manager_get_kind (ap_manager_t* man) ¶

Returns the currently set value for the polyhedron kind.

Function: void ap_pplite_manager_set_widen_spec (ap_manager_t* man, const char* name) ¶

Sets the specification for the widening operator to value name, which should be either "safe" (default value) or "risky".

The "risky" specification is the alternative one (see footnote 6 in Cousot-Cousot PLILP 1992 paper), which assumes that the second argument of the widening contains the first one; hence, when using this specification the user is usually required to compute the join before the widening (otherwise, an undefined behavior may result). Note: this assumption is done by other APRON’s domains, including the polyhedra domains in NewPolka and PPL.

The "safe" specification is the classical one (see Cousot-Cousot POPL 1977 paper), without the assumption; hence, the user can directly apply the widening without computing a join.

Function: const char* ap_pplite_manager_get_widen_spec (ap_manager_t* man) ¶

Returns the widening specification currently in use.

APRON PPLite standard options ¶

Currently, the choice of the specific variant of widening operator (both with and without thresholds) is controlled by option algorithm. Possible values are:

• 0 for standard widening (Cousot & Halbwachs POPL 1978);
• 1 for BHRZ03 widening (Bagnara et al., SAS 2003);
• 2 for the boxed standard widening (combining the intervals and polyhedra widenings).