Frama-C:
Plug-ins:
Libraries:

Frama-C API - Abstract0

type 'a t
val set_gc : int -> unit
val copy : 'a Manager.t -> 'a t -> 'a t
val size : 'a Manager.t -> 'a t -> int
val minimize : 'a Manager.t -> 'a t -> unit
val canonicalize : 'a Manager.t -> 'a t -> unit
val hash : 'a Manager.t -> 'a t -> int
val approximate : 'a Manager.t -> 'a t -> int -> unit
val fdump : 'a Manager.t -> 'a t -> unit
val print : (int -> string) -> Stdlib.Format.formatter -> 'a t -> unit
val bottom : 'a Manager.t -> int -> int -> 'a t
val top : 'a Manager.t -> int -> int -> 'a t
val of_box : 'a Manager.t -> int -> int -> Interval.t array -> 'a t
val dimension : 'a Manager.t -> 'a t -> Dim.dimension
val manager : 'a t -> 'a Manager.t
val is_bottom : 'a Manager.t -> 'a t -> bool
val is_top : 'a Manager.t -> 'a t -> bool
val is_leq : 'a Manager.t -> 'a t -> 'a t -> bool
val is_eq : 'a Manager.t -> 'a t -> 'a t -> bool
val sat_lincons : 'a Manager.t -> 'a t -> Lincons0.t -> bool
val sat_tcons : 'a Manager.t -> 'a t -> Tcons0.t -> bool
val sat_interval : 'a Manager.t -> 'a t -> Dim.t -> Interval.t -> bool
val is_dimension_unconstrained : 'a Manager.t -> 'a t -> Dim.t -> bool
val bound_dimension : 'a Manager.t -> 'a t -> Dim.t -> Interval.t
val bound_linexpr : 'a Manager.t -> 'a t -> Linexpr0.t -> Interval.t
val bound_texpr : 'a Manager.t -> 'a t -> Texpr0.t -> Interval.t
val to_box : 'a Manager.t -> 'a t -> Interval.t array
val to_lincons_array : 'a Manager.t -> 'a t -> Lincons0.t array
val to_tcons_array : 'a Manager.t -> 'a t -> Tcons0.t array
val to_generator_array : 'a Manager.t -> 'a t -> Generator0.t array
val meet : 'a Manager.t -> 'a t -> 'a t -> 'a t
val meet_array : 'a Manager.t -> 'a t array -> 'a t
val meet_lincons_array : 'a Manager.t -> 'a t -> Lincons0.t array -> 'a t
val meet_tcons_array : 'a Manager.t -> 'a t -> Tcons0.t array -> 'a t
val join : 'a Manager.t -> 'a t -> 'a t -> 'a t
val join_array : 'a Manager.t -> 'a t array -> 'a t
val add_ray_array : 'a Manager.t -> 'a t -> Generator0.t array -> 'a t
val meet_with : 'a Manager.t -> 'a t -> 'a t -> unit
val meet_lincons_array_with : 'a Manager.t -> 'a t -> Lincons0.t array -> unit
val meet_tcons_array_with : 'a Manager.t -> 'a t -> Tcons0.t array -> unit
val join_with : 'a Manager.t -> 'a t -> 'a t -> unit
val add_ray_array_with : 'a Manager.t -> 'a t -> Generator0.t array -> unit
val assign_linexpr_array : 'a Manager.t -> 'a t -> Dim.t array -> Linexpr0.t array -> 'a t option -> 'a t
val substitute_linexpr_array : 'a Manager.t -> 'a t -> Dim.t array -> Linexpr0.t array -> 'a t option -> 'a t
val assign_texpr_array : 'a Manager.t -> 'a t -> Dim.t array -> Texpr0.t array -> 'a t option -> 'a t
val substitute_texpr_array : 'a Manager.t -> 'a t -> Dim.t array -> Texpr0.t array -> 'a t option -> 'a t
val assign_linexpr_array_with : 'a Manager.t -> 'a t -> Dim.t array -> Linexpr0.t array -> 'a t option -> unit
val substitute_linexpr_array_with : 'a Manager.t -> 'a t -> Dim.t array -> Linexpr0.t array -> 'a t option -> unit
val assign_texpr_array_with : 'a Manager.t -> 'a t -> Dim.t array -> Texpr0.t array -> 'a t option -> unit
val substitute_texpr_array_with : 'a Manager.t -> 'a t -> Dim.t array -> Texpr0.t array -> 'a t option -> unit
val forget_array : 'a Manager.t -> 'a t -> Dim.t array -> bool -> 'a t
val forget_array_with : 'a Manager.t -> 'a t -> Dim.t array -> bool -> unit
val add_dimensions : 'a Manager.t -> 'a t -> Dim.change -> bool -> 'a t
val remove_dimensions : 'a Manager.t -> 'a t -> Dim.change -> 'a t
val apply_dimchange2 : 'a Manager.t -> 'a t -> Dim.change2 -> bool -> 'a t
val permute_dimensions : 'a Manager.t -> 'a t -> Dim.perm -> 'a t
val add_dimensions_with : 'a Manager.t -> 'a t -> Dim.change -> bool -> unit
val remove_dimensions_with : 'a Manager.t -> 'a t -> Dim.change -> unit
val apply_dimchange2_with : 'a Manager.t -> 'a t -> Dim.change2 -> bool -> unit
val permute_dimensions_with : 'a Manager.t -> 'a t -> Dim.perm option -> unit
val expand : 'a Manager.t -> 'a t -> Dim.t -> int -> 'a t
val fold : 'a Manager.t -> 'a t -> Dim.t array -> 'a t
val expand_with : 'a Manager.t -> 'a t -> Dim.t -> int -> unit
val fold_with : 'a Manager.t -> 'a t -> Dim.t array -> unit
val widening : 'a Manager.t -> 'a t -> 'a t -> 'a t
val widening_threshold : 'a Manager.t -> 'a t -> 'a t -> Lincons0.t array -> 'a t
val closure : 'a Manager.t -> 'a t -> 'a t
val closure_with : 'a Manager.t -> 'a t -> unit
val of_lincons_array : 'a Manager.t -> int -> int -> Lincons0.t array -> 'a t
val of_tcons_array : 'a Manager.t -> int -> int -> Tcons0.t array -> 'a t
val assign_linexpr : 'a Manager.t -> 'a t -> Dim.t -> Linexpr0.t -> 'a t option -> 'a t
val substitute_linexpr : 'a Manager.t -> 'a t -> Dim.t -> Linexpr0.t -> 'a t option -> 'a t
val assign_texpr : 'a Manager.t -> 'a t -> Dim.t -> Texpr0.t -> 'a t option -> 'a t
val substitute_texpr : 'a Manager.t -> 'a t -> Dim.t -> Texpr0.t -> 'a t option -> 'a t
val assign_linexpr_with : 'a Manager.t -> 'a t -> Dim.t -> Linexpr0.t -> 'a t option -> unit
val substitute_linexpr_with : 'a Manager.t -> 'a t -> Dim.t -> Linexpr0.t -> 'a t option -> unit
val assign_texpr_with : 'a Manager.t -> 'a t -> Dim.t -> Texpr0.t -> 'a t option -> unit
val substitute_texpr_with : 'a Manager.t -> 'a t -> Dim.t -> Texpr0.t -> 'a t option -> unit
val print_array : ?first:(unit, Stdlib.Format.formatter, unit) Stdlib.format -> ?sep:(unit, Stdlib.Format.formatter, unit) Stdlib.format -> ?last:(unit, Stdlib.Format.formatter, unit) Stdlib.format -> (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a array -> unit