sig
  val signal_abort : unit -> unit
  module Computer :
    functor
      (Domain : Abstract_domain.External) (States : sig
                                                      type state = Domain.t
                                                      type t
                                                      val empty : t
                                                      val is_empty :
                                                        t -> bool
                                                      val singleton :
                                                        state -> t
                                                      val singleton' :
                                                        state Eval.or_bottom ->
                                                        t
                                                      val uncheck_add :
                                                        state -> t -> t
                                                      val add :
                                                        state -> t -> t
                                                      val add' :
                                                        state Eval.or_bottom ->
                                                        t -> t
                                                      val length : t -> int
                                                      val merge :
                                                        into:t ->
                                                        t -> t * bool
                                                      val join :
                                                        ?into:state
                                                              Eval.or_bottom ->
                                                        t ->
                                                        state Eval.or_bottom
                                                      val fold :
                                                        (state -> '-> 'a) ->
                                                        t -> '-> 'a
                                                      val iter :
                                                        (state -> unit) ->
                                                        t -> unit
                                                      val map :
                                                        (state -> state) ->
                                                        t -> t
                                                      val map_or_bottom :
                                                        (state ->
                                                         state Eval.or_bottom) ->
                                                        t -> t
                                                      val reorder : t -> t
                                                      val of_list :
                                                        state list -> t
                                                      val to_list :
                                                        t -> state list
                                                      val pretty :
                                                        Format.formatter ->
                                                        t -> unit
                                                    end) (Transfer : 
      sig
        type state = Domain.t
        type value = Domain.value
        val assign :
          state ->
          Cil_types.kinstr ->
          Cil_types.lval -> Cil_types.exp -> state Eval.or_bottom
        val assume :
          state ->
          Cil_types.stmt -> Cil_types.exp -> bool -> state Eval.or_bottom
        val call :
          Cil_types.stmt ->
          Cil_types.lval option ->
          Cil_types.exp ->
          Cil_types.exp list ->
          state -> state list Eval.or_bottom * Value_types.cacheable
        val split_final_states :
          Cil_types.kernel_function ->
          Cil_types.exp -> Integer.t list -> state list -> state list list
        val check_unspecified_sequence :
          Cil_types.stmt ->
          state ->
          (Cil_types.stmt * Cil_types.lval list * Cil_types.lval list *
           Cil_types.lval list * Cil_types.stmt ref list)
          list -> unit Eval.or_bottom
        type call_result = {
          states : state list Eval.or_bottom;
          cacheable : Value_types.cacheable;
        }
        val compute_call_ref :
          (Cil_types.kinstr -> value Eval.call -> state -> call_result) ref
      end) (Init : sig
                     val initial_state :
                       lib_entry:bool -> Domain.state Bottom.Type.or_bottom
                     val initial_state_with_formals :
                       lib_entry:bool ->
                       Cil_types.kernel_function ->
                       Domain.state Bottom.Type.or_bottom
                     val initialize_local_variable :
                       Cil_types.stmt ->
                       Cil_types.varinfo ->
                       Cil_types.init ->
                       Domain.state -> Domain.state Bottom.Type.or_bottom
                   end) (Logic : sig
                                   type state = Domain.t
                                   type states = States.t
                                   val create :
                                     state ->
                                     Cil_types.kernel_function ->
                                     Transfer_logic.ActiveBehaviors.t
                                   val create_from_spec :
                                     state ->
                                     Cil_types.spec ->
                                     Transfer_logic.ActiveBehaviors.t
                                   val check_fct_preconditions_for_behaviors :
                                     Cil_types.kinstr ->
                                     Cil_types.kernel_function ->
                                     Cil_types.behavior list ->
                                     Alarmset.status -> states -> states
                                   val check_fct_preconditions :
                                     Cil_types.kinstr ->
                                     Cil_types.kernel_function ->
                                     Transfer_logic.ActiveBehaviors.t ->
                                     state -> states Eval.or_bottom
                                   val check_fct_postconditions_for_behaviors :
                                     Cil_types.kernel_function ->
                                     Cil_types.behavior list ->
                                     Alarmset.status ->
                                     pre_state:state ->
                                     post_states:states ->
                                     result:Cil_types.varinfo option ->
                                     states
                                   val check_fct_postconditions :
                                     Cil_types.kernel_function ->
                                     Transfer_logic.ActiveBehaviors.t ->
                                     Cil_types.termination_kind ->
                                     pre_state:state ->
                                     post_states:states ->
                                     result:Cil_types.varinfo option ->
                                     states Eval.or_bottom
                                   val evaluate_assumes_of_behavior :
                                     state ->
                                     Cil_types.behavior -> Alarmset.status
                                   val interp_annot :
                                     limit:int ->
                                     record:bool ->
                                     Cil_types.kernel_function ->
                                     Transfer_logic.ActiveBehaviors.t ->
                                     Cil_types.stmt ->
                                     Cil_types.code_annotation ->
                                     initial_state:state -> states -> states
                                 end) (Spec : sig
                                                val treat_statement_assigns :
                                                  Cil_types.assigns ->
                                                  Domain.t -> Domain.t
                                              end->
      sig
        val compute :
          Cil_types.kernel_function ->
          Cil_types.kinstr ->
          Domain.t -> Domain.t list Eval.or_bottom * Value_types.cacheable
      end
end