functor
  (Domain : LogicDomain) (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->
  sig
    type state = Domain.t
    type states = States.t
    val create : state -> Cil_types.kernel_function -> ActiveBehaviors.t
    val create_from_spec : state -> Cil_types.spec -> 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 ->
      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 ->
      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 ->
      ActiveBehaviors.t ->
      Cil_types.stmt ->
      Cil_types.code_annotation -> initial_state:state -> states -> states
  end