sig   module type S =     sig       type state       type states       type active_behaviors       val create :         Transfer_logic.S.state ->         Cil_types.kernel_function -> Transfer_logic.S.active_behaviors       val check_fct_preconditions :         Cil_types.kernel_function ->         Transfer_logic.S.active_behaviors ->         Cil_types.kinstr ->         Transfer_logic.S.state -> Transfer_logic.S.states Eval.or_bottom       val check_fct_postconditions :         Cil_types.kernel_function ->         Transfer_logic.S.active_behaviors ->         Cil_types.termination_kind ->         init_state:Transfer_logic.S.state ->         post_states:Transfer_logic.S.states ->         result:Cil_types.varinfo option ->         Transfer_logic.S.states Eval.or_bottom       val interp_annot :         limit:int ->         record:bool ->         Cil_types.kernel_function ->         Transfer_logic.S.active_behaviors ->         Cil_types.stmt ->         Cil_types.code_annotation ->         initial_state:Transfer_logic.S.state ->         Transfer_logic.S.states -> Transfer_logic.S.states     end   module Make :     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 end