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"