sig   val signal_abort : unit -> unit   module Computer :     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 end