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 loc
                    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 -> (Partition.key * state) list * Eval.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 : (Partition.key * state) list;
                      cacheable : Eval.cacheable;
                      builtin : bool;
                    }
                    val compute_call_ref :
                      (Cil_types.stmt ->
                       (loc, value) Eval.call ->
                       Eval.recursion option -> 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 ->
          (Partition.key * Abstract.Dom.t) list * Eval.cacheable
      end
end