sig
  module Operation :
    sig
      type t = Abstraction.Operation.t
      val print : Format.formatter -> t -> unit
      val to_string : t -> string
      type exp = Ast.Expression.expression
      and lval = Abstraction.Operation.lval
      and info =
        Abstraction.Operation.info =
          Normal
        | Call of lval option * string * exp list
        | Ret of exp
      val get_info : t -> info
    end
  module Region :
    sig
      type t = Abstraction.Region.t
      val print : Format.formatter -> t -> unit
      val to_string : t -> string
      val eq : t -> t -> bool
      val leq : t -> t -> bool
      val cup : t -> t -> t
      val cap : t -> t -> t
      val bot : t
      val is_empty : t -> bool
      val concretize : t -> t
      val rename_vars :
        t -> (Ast.Expression.lval -> Ast.Expression.lval) -> t
      val change_location_and_stack : t -> t -> t
      type 'a coverers = 'Abstraction.Region.coverers
      val emptyCoverers : unit -> 'a coverers
      val clearCoverers : 'a coverers -> unit
      val addCoverer : 'a coverers -> t -> '-> unit
      val findCoverer : 'a coverers -> t -> 'a option
      type restriction = Abstraction.Region.restriction
      val negate_restriction : restriction -> restriction
      val locals_and_globals : string -> restriction
      val only_globals : restriction
      val only_locals : string -> restriction
      val restrict : restriction -> t -> t
    end
  val reg_to_strings : Region.t -> string list * string
  val reg_function_name : Region.t -> string
  val reg_to_string : Region.t -> string
  val op_to_string : Operation.t -> int * int * string
  type phi_table = (Ast.Expression.lval, Region.t ref) Hashtbl.t
  val post : Region.t -> Operation.t -> phi_table -> Region.t
  val pre : Region.t -> Operation.t -> phi_table -> Region.t
  val summary_post :
    Operation.t -> Region.t -> Region.t -> phi_table -> Region.t
  val spre : Region.t -> Operation.t -> phi_table -> Region.t
  val erase_data : Region.t -> Region.t
  val predicate_to_region : Ast.Predicate.predicate -> Region.t
  val create_concrete_true_region : Operation.t -> Region.t
  val create_abstract_true_region : Operation.t -> Region.t
  val trim_region_to_globals : Region.t -> Region.t
  val new_name : string -> Ast.Expression.lval -> Ast.Expression.lval
  val brand_new_suffix : unit -> string
  val assumed_invariants_region : Region.t ref
  val precise : Region.t -> Region.t
  exception NoNewPredicatesException
  val focus : Region.t -> Region.t -> Region.t
  val focus_stamp : Region.t -> Region.t
  val analyze_trace : Region.t list -> Operation.t list -> unit
  val block_analyze_trace :
    Region.t list -> Operation.t list -> int list -> int * Region.t
  val find_all_predicates : Region.t list -> Operation.t list -> unit
  val predicate_fixpoint_reached : unit -> bool
  val coverable : Region.t -> bool
  val covered : Region.t -> Region.t -> bool
  val intersect_with_abstraction : Region.t -> Region.t -> Region.t
  val print_abs_stats : unit -> unit
  val reset_abs_stats : unit -> unit
  val enabled_ops : Region.t -> Operation.t list
  val print_debug_info : Operation.t list -> unit
  val isPredicate : Operation.t -> bool
  val check_emptiness : Operation.t -> bool
  val reset : unit -> unit
  val can_escape : Ast.Expression.lval -> bool
  val is_lock : Ast.Expression.lval -> bool
  type proof_region = Abstraction.proof_region
  and lemma_index = Abstraction.lemma_index
  val post_proof :
    Region.t -> Operation.t -> phi_table -> proof_region * lemma_index
  val check_reg_eq : proof_region -> Region.t -> bool
  val extract_proof_region : Region.t -> proof_region
  val print_proof_region : proof_region -> unit
  val print_proofTable : unit -> unit
  val iter_global_variables : (Ast.Expression.lval -> unit) -> unit
  type access_type = Abstraction.access_type = Anone | Aread | Awrite | Aboth
  val accessing : Operation.t -> Ast.Expression.lval -> access_type
  val get_all_writes : Operation.t -> Ast.Expression.lval list
  val get_all_reads : Operation.t -> Ast.Expression.lval list
  val reads_and_writes :
    Operation.t -> Ast.Expression.lval list * Ast.Expression.lval list
  val aliasesOf : Ast.Expression.lval -> Ast.Expression.lval list
  val multiply_instantiable :
    Region.t ->
    Region.t -> Ast.Expression.lval -> Ast.Expression.lval -> Region.t option
  val make_multiply_instantiable_region :
    Region.t ->
    Region.t -> Ast.Expression.lval -> Ast.Expression.lval -> Region.t
  type spec = Abstraction.spec
  and spec_result =
    Abstraction.spec_result =
      Yes
    | No
    | Maybe of Ast.Predicate.predicate
  val init_spec : unit -> unit
  val build_spec : string -> (Region.t * Region.t list) list -> spec
  val check_spec : spec -> spec -> spec_result
  val predIndex : int ref
end