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 init :
          with_alarms:CilE.warn_mode ->
          state ->
          Cil_types.kernel_function ->
          Cil_types.stmt ->
          Cil_types.varinfo -> Cil_types.init -> state Eval.or_bottom
        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 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 ->
          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) (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_behavior :
                        Cil_types.kernel_function ->
                        Transfer_logic.ActiveBehaviors.t ->
                        per_behavior:bool ->
                        Cil_types.kinstr ->
                        states -> Cil_types.behavior -> states
                      val check_fct_preconditions :
                        Cil_types.kernel_function ->
                        Transfer_logic.ActiveBehaviors.t ->
                        Cil_types.kinstr -> state -> states Eval.or_bottom
                      val check_fct_postconditions_for_behaviors :
                        Cil_types.kernel_function ->
                        Transfer_logic.ActiveBehaviors.t ->
                        Cil_types.behavior list ->
                        Cil_types.termination_kind ->
                        per_behavior:bool ->
                        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 reduce_by_assumes_of_behavior :
                        Cil_types.kernel_function ->
                        Cil_types.behavior -> states -> states
                      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->
      sig
        val compute :
          Cil_types.kernel_function ->
          Cil_types.kinstr ->
          Domain.t -> Domain.t list Eval.or_bottom * Value_types.cacheable
      end
end