functor
  (Domain : Abstract_domain.S) (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->
  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