Module Manager

module Manager: sig .. end

type funid =

`\|`	`Funid_unknown`
`\|`	`Funid_copy`
`\|`	`Funid_free`
`\|`	`Funid_asize`
`\|`	`Funid_minimize`
`\|`	`Funid_canonicalize`
`\|`	`Funid_hash`
`\|`	`Funid_approximate`
`\|`	`Funid_fprint`
`\|`	`Funid_fprintdiff`
`\|`	`Funid_fdump`
`\|`	`Funid_serialize_raw`
`\|`	`Funid_deserialize_raw`
`\|`	`Funid_bottom`
`\|`	`Funid_top`
`\|`	`Funid_of_box`
`\|`	`Funid_dimension`
`\|`	`Funid_is_bottom`
`\|`	`Funid_is_top`
`\|`	`Funid_is_leq`
`\|`	`Funid_is_eq`
`\|`	`Funid_is_dimension_unconstrained`
`\|`	`Funid_sat_interval`
`\|`	`Funid_sat_lincons`
`\|`	`Funid_sat_tcons`
`\|`	`Funid_bound_dimension`
`\|`	`Funid_bound_linexpr`
`\|`	`Funid_bound_texpr`
`\|`	`Funid_to_box`
`\|`	`Funid_to_lincons_array`
`\|`	`Funid_to_tcons_array`
`\|`	`Funid_to_generator_array`
`\|`	`Funid_meet`
`\|`	`Funid_meet_array`
`\|`	`Funid_meet_lincons_array`
`\|`	`Funid_meet_tcons_array`
`\|`	`Funid_join`
`\|`	`Funid_join_array`
`\|`	`Funid_add_ray_array`
`\|`	`Funid_assign_linexpr_array`
`\|`	`Funid_substitute_linexpr_array`
`\|`	`Funid_assign_texpr_array`
`\|`	`Funid_substitute_texpr_array`
`\|`	`Funid_add_dimensions`
`\|`	`Funid_remove_dimensions`
`\|`	`Funid_permute_dimensions`
`\|`	`Funid_forget_array`
`\|`	`Funid_expand`
`\|`	`Funid_fold`
`\|`	`Funid_widening`
`\|`	`Funid_closure`
`\|`	`Funid_change_environment`
`\|`	`Funid_rename_array`

type funopt = {

	`algorithm : int;`
	`timeout : int;`
	`max_object_size : int;`
	`flag_exact_wanted : bool;`
	`flag_best_wanted : bool;`

}

type exc =

`\|`	`Exc_none`
`\|`	`Exc_timeout`
`\|`	`Exc_out_of_space`
`\|`	`Exc_overflow`
`\|`	`Exc_invalid_argument`
`\|`	`Exc_not_implemented`

type exclog = {

	`exn : exc;`
	`funid : funid;`
	`msg : string;`

}

type 'a t

APRON Managers

The type parameter 'a allows to distinguish managers allocated by different underlying abstract domains.

Concerning the other types,

funid defines identifiers for the generic function working on abstrat values;

funopt defines the options associated to generic functions;

exc defines the different kind of exceptions;

exclog defines the exceptions raised by APRON functions.

NOTE: Managers are not totally ordered. As of 0.9.15, they do not implement the polymorphic compare function to avoid confusion. As a consequence, the polymorphic =, <=, etc. operators cannot be used.

val get_library : 'a t -> string

Get the name of the effective library which allocated the manager

val get_version : 'a t -> string

Get the version of the effective library which allocated the manager

val funopt_make : unit -> funopt

Return the default options for any function (0 or false for al fields)

val get_funopt : 'a t -> funid -> funopt

Get the options sets for the function. The result is a copy of the internal structure and may be freely modified. funid should be different from Funid_change_environment and Funid_rename_array (no option associated to them).

val set_funopt : 'a t -> funid -> funopt -> unit

Set the options for the function. funid should be different from Funid_change_environment and Funid_rename_array (no option associated to them).

val get_flag_exact : 'a t -> bool

Get the corresponding result flag

val get_flag_best : 'a t -> bool

Get the corresponding result flag

exception Error of exclog

Exception raised by functions of the interface

val string_of_funid : funid -> string

val string_of_exc : exc -> string

val print_funid : Stdlib.Format.formatter -> funid -> unit

val print_funopt : Stdlib.Format.formatter -> funopt -> unit

val print_exc : Stdlib.Format.formatter -> exc -> unit

val print_exclog : Stdlib.Format.formatter -> exclog -> unit

Printing functions

val set_deserialize : 'a t -> unit

Set / get the global manager used for deserialization

val get_deserialize : unit -> 'a t