Module Box

module Box: sig .. end

Intervals abstract domain

type t

Type of boxes.

Boxes constrains each dimension/variable x_i to belong to an interval I_i.

Abstract values which are boxes have the type t Apron.AbstractX.t.

Managers allocated for boxes have the type t Apron.manager.t.

val manager_alloc : unit -> t Apron.Manager.t

Create a Box manager.

Type conversions

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

Return true iff the argument manager is a box manager

val manager_of_box : t Apron.Manager.t -> 'a Apron.Manager.t

Make a box manager generic

val manager_to_box : 'a Apron.Manager.t -> t Apron.Manager.t

Instanciate the type of a box manager. Raises Failure if the argument manager is not a box 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.

Bytecode compilation

ocamlc -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -o mlexample.byte \
  bigarray.cma gmp.cma apron.cma boxMPQ.cma mlexample.ml

ocamlc -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -make-runtime -o myrun \
  bigarray.cma gmp.cma apron.cma boxMPQ.cma

ocamlc -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -use-runtime myrun -o mlexample.byte \
  bigarray.cma gmp.cma apron.cma boxMPQ.cma mlexample.ml

Native-code compilation

ocamlopt -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -o mlexample.opt \
  bigarray.cmxa gmp.cmxa apron.cmxa boxMPQ.cmxa mlexample.ml

Without auto-linking feature

ocamlopt -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -noautolink -o mlexample.opt \
  bigarray.cmxa gmp.cmxa apron.cmxa boxMPQ.cmxa mlexample.ml \
  -cclib "-L$MLGMPIDL_PREFIX/lib -L$APRON_PREFIX/lib \
	  -lboxMPQ_caml_debug -lboxMPQ_debug \
	  -lapron_caml_debug -lapron_debug \
	  -lgmp_caml -L$MPFR_PREFIX/lib -lmpfr -L$GMP/lib_PREFIX/lib -lgmp \
	  -L$CAMLIDL_PREFIX/lib/ocaml -lcamlidl \
	  -lbigarray"