sig
  val signal_abort : unit -> unit
  module Computer :
    functor
      (Abstract : Abstractions.Eva) (States : sig
                                                type state = Abstract.Dom.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 =
                                                                    Abstract.Dom.t
                                                                 type value =
                                                                    Abstract.Val.t
                                                                 type location
                                                                 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 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
                                                                 val enter_scope :
                                                                   Cil_types.kernel_function ->
                                                                   Cil_types.varinfo
                                                                   list ->
                                                                   state ->
                                                                   state
                                                                 type call_result = {
                                                                   states :
                                                                    state
                                                                    list
                                                                    Eval.or_bottom;
                                                                   cacheable :
                                                                    Value_types.cacheable;
                                                                   builtin :
                                                                    bool;
                                                                 }
                                                                 val compute_call_ref :
                                                                   (Cil_types.stmt ->
                                                                    (location,
                                                                    value)
                                                                    Eval.call ->
                                                                    state ->
                                                                    call_result)
                                                                   ref
                                                               end) (Init : 
      sig
        val initial_state :
          lib_entry:bool -> Abstract.Dom.t Bottom.Type.or_bottom
        val initial_state_with_formals :
          lib_entry:bool ->
          Cil_types.kernel_function -> Abstract.Dom.t Bottom.Type.or_bottom
        val initialize_local_variable :
          Cil_types.stmt ->
          Cil_types.varinfo ->
          Cil_types.init ->
          Abstract.Dom.t -> Abstract.Dom.t Bottom.Type.or_bottom
      end) (Logic : sig
                      type state = Abstract.Dom.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 ->
                                     Abstract.Dom.t -> Abstract.Dom.t
                                 end->
      sig
        val compute :
          Cil_types.kernel_function ->
          Cil_types.kinstr ->
          Abstract.Dom.t ->
          Abstract.Dom.t list Eval.or_bottom * Value_types.cacheable
      end
end