Module Ppl

module Ppl: sig .. end

Convex Polyhedra and Linear Congruences abstract domains (PPL wrapper)

This module is a wrapper around the Parma Polyhedra Library.

type loose

type strict

Two flavors for convex polyhedra: loose or strict.

Loose polyhedra cannot have strict inequality constraints like x>0. They are algorithmically more efficient (less generators, simpler normalization). Convex polyhedra are defined by the conjunction of a set of linear constraints of the form a_0*x_0 + ... + a_n*x_n + b >= 0 or a_0*x_0 + ... + a_n*x_n + b > 0 where a_0, ..., a_n, b, c are constants and x_0, ..., x_n variables.

type grid

Linear congruences.

Linear congruences are defined by the conjunction of equality constraints modulo a rational number, of the form a_0*x_0 + ... + a_n*x_n = b mod c, where a_0, ..., a_n, b, c are constants and x_0, ..., x_n variables.

type 'a t

Type of convex polyhedra/linear congruences, where 'a is loose, strict or grid.

Abstract values which are convex polyhedra have the type loose t Apron.AbstractX.t or strict t Apron.AbstractX.t. Abstract values which are conjunction of linear congruences equalities have the type grid t Apron.AbstractX.t. Managers allocated by PPL have the type 'a t Apron.Manager.t.

val manager_alloc_loose : unit -> loose t Apron.Manager.t

Allocate a PPL manager for loose convex polyhedra.

val manager_alloc_strict : unit -> strict t Apron.Manager.t

Allocate a PPL manager for strict convex polyhedra.

val manager_alloc_grid : unit -> grid t Apron.Manager.t

Allocate a new manager for linear congruences (grids)

val manager_is_ppl : 'a Apron.Manager.t -> bool

Type conversions

val manager_is_ppl_loose : 'a Apron.Manager.t -> bool

val manager_is_ppl_strict : 'a Apron.Manager.t -> bool

val manager_is_ppl_grid : 'a Apron.Manager.t -> bool

Return true iff the argument manager is a ppl manager

val manager_of_ppl : 'a t Apron.Manager.t -> 'b Apron.Manager.t

val manager_of_ppl_loose : loose t Apron.Manager.t -> 'a Apron.Manager.t

val manager_of_ppl_strict : strict t Apron.Manager.t -> 'a Apron.Manager.t

val manager_of_ppl_grid : grid t Apron.Manager.t -> 'a Apron.Manager.t

Make a ppl manager generic

val manager_to_ppl : 'a Apron.Manager.t -> 'b t Apron.Manager.t

val manager_to_ppl_loose : 'a Apron.Manager.t -> loose t Apron.Manager.t

val manager_to_ppl_strict : 'a Apron.Manager.t -> strict t Apron.Manager.t

val manager_to_ppl_grid : 'a Apron.Manager.t -> grid t Apron.Manager.t

Instanciate the type of a ppl manager. Raises Failure if the argument manager is not a ppl manager

module Abstract0: sig .. end

module Abstract1: sig .. end

Compilation information

See Introduction.compilation for complete explanations. We just show examples with the file mlexample.ml.

Do not forget the -cc "g++" option: PPL is a C++ library which requires a C++ linker.

Bytecode compilation

ocamlc -cc "g++"-I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -o mlexample.byte \ bigarray.cma gmp.cma apron.cma ppl.cma mlexample.ml

ocamlc -cc "g++" -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -make-runtime -o myrun \ bigarray.cma gmp.cma apron.cma ppl.cma ocamlc -cc "g++" -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -use-runtime myrun -o mlexample.byte \ bigarray.cma gmp.cma apron.cma ppl.cma mlexample.ml

Native-code compilation

ocamlopt -cc "g++" -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -o mlexample.opt \ bigarray.cmxa gmp.cmxa apron.cmxa ppl.cmxa mlexample.ml

Without auto-linking feature

ocamlopt -cc "g++" -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -noautolink -o mlexample.opt \ bigarray.cmxa gmp.cmxa apron.cmxa ppl.cmxa mlexample.ml \ -cclib "-L$MLGMPIDL_PREFIX/lib -L$APRON_PREFIX/lib -L$PPL_PREFIX/lib\ -lap_ppl_caml_debug -lap_ppl_debug -lppl -lgmpxx \ -lapron_caml_debug -lapron_debug \ -lgmp_caml -L$MPFR_PREFIX/lib -lmpfr -L$GMP_PREFIX/lib -lgmp \ -L$CAMLIDL_PREFIX/lib/ocaml -lcamlidl \ -lbigarray"