Module Oct

module Oct: sig .. end
Octagon abstract domain.

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.

Type conversions


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

Compilation information

See Introduction.compilation 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 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

Native-code compilation

ocamlopt -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -o mlexample.opt \ bigarray.cmxa gmp.cmxa apron.cmxa octD.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 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"