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