functor (Abstraction : BlastArch.ABSTRACTION->
  sig
    module Abstraction :
      sig
        module Operation :
          sig
            type t = Abstraction.Operation.t
            val print : Format.formatter -> t -> unit
            val to_string : t -> string
            type exp = Abstraction.Operation.exp
            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
    type error_path =
      Abstraction.Region.t * Abstraction.Operation.t list *
      Abstraction.Region.t
    and model_check_outcome = error_path BlastArch.ModelCheckOutcome.outcome
    val model_check_tar :
      Abstraction.Region.t ->
      Abstraction.Region.t option -> model_check_outcome
    val model_check :
      Abstraction.Region.t ->
      Abstraction.Region.t option -> model_check_outcome
    val print_stats : Format.formatter -> unit -> unit
    val print_phis : bool -> string
    val process_env_assumptions :
      (Ast.Expression.lval * Ast.Predicate.predicate) list -> unit
  end