module Oct:sig
..end
type
internal
Octagon abstract domain.
type
t
Type of octagons.
Octagons are defined by conjunctions of inequalities of the form
+/-x_i +/- x_j >= 0
.
Abstract values which are octagons have the type t Apron.AbstractX.t
.
Managers allocated for octagons have the type t Apron.manager.t
.
val manager_alloc : unit -> t Apron.Manager.t
Allocate a new manager to manipulate octagons.
val manager_get_internal : t Apron.Manager.t -> internal
No internal parameters for now...
val of_generator_array : t Apron.Manager.t ->
int -> int -> Apron.Generator0.t array -> t Apron.Abstract0.t
Approximate a set of generators to an abstract value, with best precision.
val widening_thresholds : t Apron.Manager.t ->
t Apron.Abstract0.t ->
t Apron.Abstract0.t -> Apron.Scalar.t array -> t Apron.Abstract0.t
Widening with scalar thresholds.
val narrowing : t Apron.Manager.t ->
t Apron.Abstract0.t -> t Apron.Abstract0.t -> t Apron.Abstract0.t
Standard narrowing.
val add_epsilon : t Apron.Manager.t ->
t Apron.Abstract0.t -> Apron.Scalar.t -> t Apron.Abstract0.t
Perturbation.
val add_epsilon_bin : t Apron.Manager.t ->
t Apron.Abstract0.t ->
t Apron.Abstract0.t -> Apron.Scalar.t -> t Apron.Abstract0.t
Perturbation.
val pre_widening : int
Algorithms.
val manager_is_oct : 'a Apron.Manager.t -> bool
Return true
iff the argument manager is an octagon manager
val manager_of_oct : t Apron.Manager.t -> 'a Apron.Manager.t
Make an octagon manager generic
val manager_to_oct : 'a Apron.Manager.t -> t Apron.Manager.t
Instanciate the type of an octagon manager.
Raises Failure
if the argument manager is not an octagon manager
module Abstract0:sig
..end
module Abstract1:sig
..end
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 octD.cma mlexample.ml
ocamlc -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -make-runtime -o myrun \
bigarray.cma gmp.cma apron.cma octD.cma
ocamlc -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -use-runtime myrun -o mlexample.byte \
bigarray.cma gmp.cma apron.cma octD.cma mlexample.ml
ocamlopt -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -o mlexample.opt \
bigarray.cmxa gmp.cmxa apron.cmxa octD.cmxa mlexample.ml
ocamlopt -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -noautolink -o mlexample.opt \
bigarray.cmxa gmp.cmxa apron.cmxa octD.cmxa mlexample.ml \
-cclib "-L$MLGMPIDL_PREFIX/lib -L$APRON_PREFIX/lib \
-loctD_caml_debug -loctD_debug \
-lapron_caml_debug -lapron_debug \
-lgmp_caml -L$MPFR_PREFIX/lib -lmpfr -L$GMP_PREFIX/lib -lgmp \
-L$CAMLIDL_PREFIX/lib/ocaml -lcamlidl \
-lbigarray"