Frama-C:
Plug-ins:
Libraries:

Frama-C API - Abstract1

type !'a t = {
  1. mutable abstract0 : 'a Abstract0.t;
  2. mutable env : Environment.t;
}
type box1 = {
  1. mutable interval_array : Interval.t array;
  2. mutable box1_env : Environment.t;
}
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 : Stdlib.Format.formatter -> 'a t -> unit
val bottom : 'a Manager.t -> Environment.t -> 'a t
val top : 'a Manager.t -> Environment.t -> 'a t
val of_box : 'a Manager.t -> Environment.t -> Var.t array -> Interval.t array -> 'a t
val manager : 'a t -> 'a Manager.t
val env : 'a t -> Environment.t
val abstract0 : 'a t -> 'a Abstract0.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 -> Lincons1.t -> bool
val sat_tcons : 'a Manager.t -> 'a t -> Tcons1.t -> bool
val sat_interval : 'a Manager.t -> 'a t -> Var.t -> Interval.t -> bool
val is_variable_unconstrained : 'a Manager.t -> 'a t -> Var.t -> bool
val bound_variable : 'a Manager.t -> 'a t -> Var.t -> Interval.t
val bound_linexpr : 'a Manager.t -> 'a t -> Linexpr1.t -> Interval.t
val bound_texpr : 'a Manager.t -> 'a t -> Texpr1.t -> Interval.t
val to_box : 'a Manager.t -> 'a t -> box1
val to_lincons_array : 'a Manager.t -> 'a t -> Lincons1.earray
val to_tcons_array : 'a Manager.t -> 'a t -> Tcons1.earray
val to_generator_array : 'a Manager.t -> 'a t -> Generator1.earray
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 -> Lincons1.earray -> 'a t
val meet_tcons_array : 'a Manager.t -> 'a t -> Tcons1.earray -> '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 -> Generator1.earray -> 'a t
val meet_with : 'a Manager.t -> 'a t -> 'a t -> unit
val meet_lincons_array_with : 'a Manager.t -> 'a t -> Lincons1.earray -> unit
val meet_tcons_array_with : 'a Manager.t -> 'a t -> Tcons1.earray -> unit
val join_with : 'a Manager.t -> 'a t -> 'a t -> unit
val add_ray_array_with : 'a Manager.t -> 'a t -> Generator1.earray -> unit
val assign_linexpr_array : 'a Manager.t -> 'a t -> Var.t array -> Linexpr1.t array -> 'a t option -> 'a t
val substitute_linexpr_array : 'a Manager.t -> 'a t -> Var.t array -> Linexpr1.t array -> 'a t option -> 'a t
val assign_texpr_array : 'a Manager.t -> 'a t -> Var.t array -> Texpr1.t array -> 'a t option -> 'a t
val substitute_texpr_array : 'a Manager.t -> 'a t -> Var.t array -> Texpr1.t array -> 'a t option -> 'a t
val assign_linexpr_array_with : 'a Manager.t -> 'a t -> Var.t array -> Linexpr1.t array -> 'a t option -> unit
val substitute_linexpr_array_with : 'a Manager.t -> 'a t -> Var.t array -> Linexpr1.t array -> 'a t option -> unit
val assign_texpr_array_with : 'a Manager.t -> 'a t -> Var.t array -> Texpr1.t array -> 'a t option -> unit
val substitute_texpr_array_with : 'a Manager.t -> 'a t -> Var.t array -> Texpr1.t array -> 'a t option -> unit
val forget_array : 'a Manager.t -> 'a t -> Var.t array -> bool -> 'a t
val forget_array_with : 'a Manager.t -> 'a t -> Var.t array -> bool -> unit
val change_environment : 'a Manager.t -> 'a t -> Environment.t -> bool -> 'a t
val minimize_environment : 'a Manager.t -> 'a t -> 'a t
val rename_array : 'a Manager.t -> 'a t -> Var.t array -> Var.t array -> 'a t
val change_environment_with : 'a Manager.t -> 'a t -> Environment.t -> bool -> unit
val minimize_environment_with : 'a Manager.t -> 'a t -> unit
val rename_array_with : 'a Manager.t -> 'a t -> Var.t array -> Var.t array -> unit
val expand : 'a Manager.t -> 'a t -> Var.t -> Var.t array -> 'a t
val fold : 'a Manager.t -> 'a t -> Var.t array -> 'a t
val expand_with : 'a Manager.t -> 'a t -> Var.t -> Var.t array -> unit
val fold_with : 'a Manager.t -> 'a t -> Var.t array -> unit
val widening : 'a Manager.t -> 'a t -> 'a t -> 'a t
val widening_threshold : 'a Manager.t -> 'a t -> 'a t -> Lincons1.earray -> '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 -> Environment.t -> Lincons1.earray -> 'a t
val of_tcons_array : 'a Manager.t -> Environment.t -> Tcons1.earray -> 'a t
val assign_linexpr : 'a Manager.t -> 'a t -> Var.t -> Linexpr1.t -> 'a t option -> 'a t
val substitute_linexpr : 'a Manager.t -> 'a t -> Var.t -> Linexpr1.t -> 'a t option -> 'a t
val assign_texpr : 'a Manager.t -> 'a t -> Var.t -> Texpr1.t -> 'a t option -> 'a t
val substitute_texpr : 'a Manager.t -> 'a t -> Var.t -> Texpr1.t -> 'a t option -> 'a t
val assign_linexpr_with : 'a Manager.t -> 'a t -> Var.t -> Linexpr1.t -> 'a t option -> unit
val substitute_linexpr_with : 'a Manager.t -> 'a t -> Var.t -> Linexpr1.t -> 'a t option -> unit
val assign_texpr_with : 'a Manager.t -> 'a t -> Var.t -> Texpr1.t -> 'a t option -> unit
val substitute_texpr_with : 'a Manager.t -> 'a t -> Var.t -> Texpr1.t -> 'a t option -> unit
val unify : 'a Manager.t -> 'a t -> 'a t -> 'a t
val unify_with : 'a Manager.t -> 'a t -> 'a t -> unit