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