sig   val current_kf_inout : unit -> Inout_type.t option   module type S =     sig       type state       type value       type return       val assign :         with_alarms:CilE.warn_mode ->         Transfer_stmt.S.state ->         Cil_types.kernel_function ->         Cil_types.stmt ->         Cil_types.lval ->         Cil_types.exp -> Transfer_stmt.S.state Eval.or_bottom       val assume :         with_alarms:CilE.warn_mode ->         Transfer_stmt.S.state ->         Cil_types.stmt ->         Cil_types.exp -> bool -> Transfer_stmt.S.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 ->         Transfer_stmt.S.state ->         Transfer_stmt.S.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 ->         Transfer_stmt.S.state ->         (Transfer_stmt.S.state, Transfer_stmt.S.return,          Transfer_stmt.S.value)         Eval.return_state Eval.or_bottom       val enter_loop :         Cil_types.stmt -> Transfer_stmt.S.state -> Transfer_stmt.S.state       val incr_loop_counter :         Cil_types.stmt -> Transfer_stmt.S.state -> Transfer_stmt.S.state       val leave_loop :         Cil_types.stmt -> Transfer_stmt.S.state -> Transfer_stmt.S.state       val split_final_states :         Cil_types.kernel_function ->         Cil_types.exp ->         Integer.t list ->         Transfer_stmt.S.state list -> Transfer_stmt.S.state list list       val check_unspecified_sequence :         with_alarms:CilE.warn_mode ->         Transfer_stmt.S.state ->         (Cil_types.stmt * Cil_types.lval list * Cil_types.lval list *          Cil_types.lval list * Cil_types.stmt Pervasives.ref list)         list -> unit Eval.or_bottom       type res =           (Transfer_stmt.S.state, Transfer_stmt.S.return,            Transfer_stmt.S.value)           Eval.call_result * Value_types.cacheable       val compute_call_ref :         (Cil_types.kinstr ->          Transfer_stmt.S.value Eval.call ->          Transfer_stmt.S.state -> Transfer_stmt.S.res)         Pervasives.ref     end   module type Domain =     sig       type state       type return       type value       type location       type valuation       val update : valuation -> state -> state       val assign :         Cil_types.kinstr ->         location Eval.left_value ->         Cil_types.exp ->         value Eval.assigned -> valuation -> state -> state Eval.or_bottom       val assume :         Cil_types.stmt ->         Cil_types.exp -> bool -> valuation -> state -> state Eval.or_bottom       val start_call :         Cil_types.stmt ->         value Eval.call ->         valuation -> state -> (state, return, value) Eval.call_action       val finalize_call :         Cil_types.stmt ->         value Eval.call -> pre:state -> post:state -> state Eval.or_bottom       val make_return :         Cil_types.kernel_function ->         Cil_types.stmt -> value Eval.assigned -> valuation -> state -> return       val assign_return :         Cil_types.stmt ->         location Eval.left_value ->         Cil_types.kernel_function ->         return ->         value Eval.assigned -> valuation -> state -> state Eval.or_bottom       val default_call :         Cil_types.stmt ->         value Eval.call -> state -> (state, return, value) Eval.call_result       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 leave_scope :         Cil_types.kernel_function -> Cil_types.varinfo list -> state -> state       module Store :         sig           val register_initial_state : Value_types.callstack -> state -> unit           val register_state_before_stmt :             Value_types.callstack -> Cil_types.stmt -> state -> unit           val register_state_after_stmt :             Value_types.callstack -> Cil_types.stmt -> state -> unit           val get_initial_state :             Cil_types.kernel_function -> state Eval.or_bottom           val get_initial_state_by_callstack :             Cil_types.kernel_function ->             state Value_types.Callstack.Hashtbl.t option           val get_stmt_state : Cil_types.stmt -> state Eval.or_bottom           val get_stmt_state_by_callstack :             after:bool ->             Cil_types.stmt -> state Value_types.Callstack.Hashtbl.t option         end       type t = state       val ty : t Type.t       val name : string       val descr : t Descr.t       val packed_descr : Structural_descr.pack       val reprs : t list       val equal : t -> t -> bool       val compare : t -> t -> int       val hash : t -> int       val pretty_code : Format.formatter -> t -> unit       val internal_pretty_code :         Type.precedence -> Format.formatter -> t -> unit       val pretty : Format.formatter -> t -> unit       val varname : t -> string       val mem_project : (Project_skeleton.t -> bool) -> t -> bool       val copy : t -> t     end   module Make :     functor       (Value : Abstract_value.S) (Location : Abstract_location.External) (Domain :        sig         type state         type return         type value = Value.t         type location = Location.location         type valuation         val update : valuation -> state -> state         val assign :           Cil_types.kinstr ->           location Eval.left_value ->           Cil_types.exp ->           value Eval.assigned -> valuation -> state -> state Eval.or_bottom         val assume :           Cil_types.stmt ->           Cil_types.exp -> bool -> valuation -> state -> state Eval.or_bottom         val start_call :           Cil_types.stmt ->           value Eval.call ->           valuation -> state -> (state, return, value) Eval.call_action         val finalize_call :           Cil_types.stmt ->           value Eval.call -> pre:state -> post:state -> state Eval.or_bottom         val make_return :           Cil_types.kernel_function ->           Cil_types.stmt ->           value Eval.assigned -> valuation -> state -> return         val assign_return :           Cil_types.stmt ->           location Eval.left_value ->           Cil_types.kernel_function ->           return ->           value Eval.assigned -> valuation -> state -> state Eval.or_bottom         val default_call :           Cil_types.stmt ->           value Eval.call -> state -> (state, return, value) Eval.call_result         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 leave_scope :           Cil_types.kernel_function ->           Cil_types.varinfo list -> state -> state         module Store :           sig             val register_initial_state :               Value_types.callstack -> state -> unit             val register_state_before_stmt :               Value_types.callstack -> Cil_types.stmt -> state -> unit             val register_state_after_stmt :               Value_types.callstack -> Cil_types.stmt -> state -> unit             val get_initial_state :               Cil_types.kernel_function -> state Eval.or_bottom             val get_initial_state_by_callstack :               Cil_types.kernel_function ->               state Value_types.Callstack.Hashtbl.t option             val get_stmt_state : Cil_types.stmt -> state Eval.or_bottom             val get_stmt_state_by_callstack :               after:bool ->               Cil_types.stmt -> state Value_types.Callstack.Hashtbl.t option           end         type t = state         val ty : t Type.t         val name : string         val descr : t Descr.t         val packed_descr : Structural_descr.pack         val reprs : t list         val equal : t -> t -> bool         val compare : t -> t -> int         val hash : t -> int         val pretty_code : Format.formatter -> t -> unit         val internal_pretty_code :           Type.precedence -> Format.formatter -> t -> unit         val pretty : Format.formatter -> t -> unit         val varname : t -> string         val mem_project : (Project_skeleton.t -> bool) -> t -> bool         val copy : t -> t       end) (Eva : sig                     type state = Domain.state                     type value = Domain.value                     type origin                     type loc = Domain.location                     module Valuation :                       sig                         type t = Domain.valuation                         type value = value                         type origin = origin                         type loc = loc                         val empty : t                         val find :                           t ->                           Cil_types.exp ->                           (value, origin) Eval.record_val Eval.or_top                         val add :                           t ->                           Cil_types.exp ->                           (value, origin) Eval.record_val -> t                         val fold :                           (Cil_types.exp ->                            (value, origin) Eval.record_val -> '-> 'a) ->                           t -> '-> 'a                         val find_loc :                           t ->                           Cil_types.lval -> loc Eval.record_loc Eval.or_top                         val remove : t -> Cil_types.exp -> t                         val remove_loc : t -> Cil_types.lval -> t                       end                     val evaluate :                       ?valuation:Valuation.t ->                       ?reduction:bool ->                       state ->                       Cil_types.exp -> (Valuation.t * value) Eval.evaluated                     val copy_lvalue :                       ?valuation:Valuation.t ->                       state ->                       Cil_types.lval ->                       (Valuation.t * value Eval.flagged_value) Eval.evaluated                     val lvaluate :                       ?valuation:Valuation.t ->                       for_writing:bool ->                       state ->                       Cil_types.lval ->                       (Valuation.t * loc * Cil_types.typ) Eval.evaluated                     val reduce :                       ?valuation:Valuation.t ->                       state ->                       Cil_types.exp -> bool -> Valuation.t Eval.evaluated                     val assume :                       ?valuation:Valuation.t ->                       state ->                       Cil_types.exp -> value -> Valuation.t Eval.or_bottom                     val loc_size : loc -> Int_Base.t                     val reinterpret :                       Cil_types.exp ->                       Cil_types.typ -> value -> value Eval.evaluated                     val do_promotion :                       src_typ:Cil_types.typ ->                       dst_typ:Cil_types.typ ->                       Cil_types.exp -> value -> value Eval.evaluated                     val split_by_evaluation :                       Cil_types.exp ->                       Integer.t list ->                       state list ->                       (Integer.t * state list * bool) list * state list                     val check_copy_lval :                       Cil_types.lval * loc ->                       Cil_types.lval * loc -> bool Eval.evaluated                     val check_non_overlapping :                       state ->                       Cil_types.lval list ->                       Cil_types.lval list -> unit Eval.evaluated                     val eval_function_exp :                       Cil_types.exp ->                       state ->                       (Kernel_function.t * Valuation.t) list Eval.evaluated                   end->       sig         type state = Domain.state         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 end