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 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
        type summary = Domain.summary
        val assign :
          with_alarms:CilE.warn_mode ->
          state ->
          Cil_types.kernel_function ->
          Cil_types.stmt ->
          Cil_types.lval -> Cil_types.exp -> state Eval.or_bottom
        val assume :
          with_alarms:CilE.warn_mode ->
          state ->
          Cil_types.stmt -> Cil_types.exp -> bool -> state Eval.or_bottom
        val call :
          with_alarms:CilE.warn_mode ->
          Cil_types.stmt ->
          Cil_types.lval option ->
          Cil_types.exp ->
          Cil_types.exp list ->
          state -> state list Eval.or_bottom * Value_types.cacheable
        val return :
          with_alarms:CilE.warn_mode ->
          Cil_types.kernel_function ->
          Cil_types.stmt ->
          Cil_types.lval option ->
          state -> (state, summary, value) Eval.return Eval.or_bottom
        val split_final_states :
          Cil_types.kernel_function ->
          Cil_types.exp -> Integer.t list -> state list -> state list list
        val check_unspecified_sequence :
          with_alarms:CilE.warn_mode ->
          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 res =
            (state, summary, value) Eval.call_result * Value_types.cacheable
        val compute_call_ref :
          (Cil_types.kinstr -> value Eval.call -> state -> res) ref
      end) (Logic : sig
                      type state = Domain.t
                      type states = States.t
                      type active_behaviors
                      val create :
                        state ->
                        Cil_types.kernel_function -> active_behaviors
                      val check_fct_preconditions :
                        Cil_types.kernel_function ->
                        active_behaviors ->
                        Cil_types.kinstr -> state -> states Eval.or_bottom
                      val check_fct_postconditions :
                        Cil_types.kernel_function ->
                        active_behaviors ->
                        Cil_types.termination_kind ->
                        init_state:state ->
                        post_states:states ->
                        result:Cil_types.varinfo option ->
                        states Eval.or_bottom
                      val interp_annot :
                        limit:int ->
                        record:bool ->
                        Cil_types.kernel_function ->
                        active_behaviors ->
                        Cil_types.stmt ->
                        Cil_types.code_annotation ->
                        initial_state:state -> states -> states
                    end->
      sig
        val compute :
          Cil_types.kernel_function ->
          Cil_types.kinstr ->
          Domain.t ->
          (Domain.t, Domain.summary, Domain.value) Eval.call_result *
          Value_types.cacheable
      end
end