Module Pplite

module Pplite: sig .. end

Polyhedra abstract domains (PPLite wrapper)

type loose

type strict

Two flavors for convex polyhedra: loose or strict.

Loose polyhedra cannot have strict inequality constraints like x>0. 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 'a t

Type of convex polyhedra, where 'a is loose or strict.

Abstract values which are convex polyhedra have the type loose t Apron.AbstractX.t or strict t Apron.AbstractX.t. Managers allocated by PPLite have the type 'a t Apron.Manager.t.

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

Allocate a PPLite manager for loose convex polyhedra.

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

Allocate a PPLite manager for strict convex polyhedra.

val manager_set_kind : 'a t Apron.Manager.t -> string -> unit

Set the polyhedra kind for PPLite manager.

val manager_get_kind : 'a t Apron.Manager.t -> string

Get the polyhedra kind from PPLite manager.

val manager_set_widen_spec : 'a t Apron.Manager.t -> string -> unit

Set the widening specification for PPLite manager. legal values are:

"safe": the Cousot&Cousot POPL77 specification, which does not assume the inclusion between arguments;
"risky": the Cousot&Cousot PLILP92 footnote 6 alternative specification, assuming the inclusion between arguments.

val manager_get_widen_spec : 'a t Apron.Manager.t -> string

Get the widening specification from PPLite manager.

PPLite's abstract0 ad-hoc functions

val abstract0_split : 'a t Apron.Manager.t ->
       'a t Apron.Abstract0.t ->
       Apron.Lincons0.t -> bool -> bool -> 'a t Apron.Abstract0.t

Splits abstract element on linear constraint

val abstract0_is_disjunctive : 'a t Apron.Manager.t -> 'a t Apron.Abstract0.t -> bool

Returns true if abs is a powerset of polyhedra

val abstract0_num_disjuncts : 'a t Apron.Manager.t -> 'a t Apron.Abstract0.t -> int

Get the number of disjuncts of a polyhedra powerset.

val abstract0_disj_to_lincons_array : 'a t Apron.Manager.t ->
       'a t Apron.Abstract0.t -> int -> Apron.Lincons0.t array

Get the linear constraints of the n-th disjunct.

val abstract0_disj_to_tcons_array : 'a t Apron.Manager.t ->
       'a t Apron.Abstract0.t -> int -> Tcons0.t array

Get the tree constraints of the n-th disjunct.

val abstract0_geom_subseteq : 'a t Apron.Manager.t ->
       'a t Apron.Abstract0.t -> 'a t Apron.Abstract0.t -> bool

Returns true if abs1 is geometrically contained in abs2

val abstract0_collapse : 'a t Apron.Manager.t -> 'a t Apron.Abstract0.t -> int -> unit

Modify abstract element to have n disjunct at most.

Type conversions

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

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

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

Return true iff the argument manager is a PPLite manager

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

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

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

Make a PPLite manager generic

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

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

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

Instantiate the type of a PPLite manager. Raises Failure if the argument manager is not a PPLite manager

module Abstract0: sig .. end

module Abstract1: sig .. end

Compilation information

See Compiling and linking client programs against APRON for complete explanations. We just show examples with the file mlexample.ml.

Do not forget the -cc "g++" option: PPLite 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 pplite.cma mlexample.ml

ocamlc -cc "g++" -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -make-runtime -o myrun \
  bigarray.cma gmp.cma apron.cma pplite.cma

ocamlc -cc "g++" -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -use-runtime myrun -o mlexample.byte \
  bigarray.cma gmp.cma apron.cma pplite.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 pplite.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 pplite.cmxa mlexample.ml \
  -cclib "-L$MLGMPIDL_PREFIX/lib -L$APRON_PREFIX/lib -L$PPLITE_PREFIX/lib\
	  -lap_pplite_caml_debug -lap_pplite_debug -lpplite \
          -L$FLINT_PREFIX/lib -lflint \
	  -lapron_caml_debug -lapron_debug \
	  -lgmp_caml -L$MPFR_PREFIX/lib -lmpfr -L$GMP_PREFIX/lib -lgmp \
	  -L$CAMLIDL_PREFIX/lib/ocaml -lcamlidl \
	  -lbigarray"