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.
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
module Policy:sig
..end
val policy_manager_alloc : t Apron.Manager.t -> t Apron.Policy.man
See Compiling and linking client programs against APRON for complete explanations.
We just show examples with the file mlexample.ml
.
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
ocamlopt -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -o mlexample.opt \
bigarray.cmxa gmp.cmxa apron.cmxa boxMPQ.cmxa mlexample.ml
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"