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 return =                                                                     Domain.return                                                                    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,                                                                     return,                                                                     value)                                                                     Eval.return_state                                                                     Eval.or_bottom                                                                    val enter_loop :                                                                     Cil_types.stmt ->                                                                     state ->                                                                     state                                                                    val incr_loop_counter :                                                                     Cil_types.stmt ->                                                                     state ->                                                                     state                                                                    val leave_loop :                                                                     Cil_types.stmt ->                                                                     state ->                                                                     state                                                                    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,                                                                     return,                                                                     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.return, Domain.value) Eval.call_result *       Value_types.cacheable   end