sig   module type Results =     sig       type state       type value       val get_stmt_state :         Cil_types.stmt -> Analysis.Results.state Eval.or_bottom       val eval_expr :         Analysis.Results.state ->         Cil_types.exp -> Analysis.Results.value Eval.evaluated     end   module Make :     functor (Abstract : Abstractions.S->       sig         val compute : ?library:bool -> Cil_types.kernel_function -> unit         type state = Abstract.Dom.state         type value = Abstract.Val.t         val get_stmt_state : Cil_types.stmt -> state Eval.or_bottom         val eval_expr : state -> Cil_types.exp -> value Eval.evaluated       end   module type S =     sig       module Val : Abstractions.Value       module Loc :         sig           type value = Val.t           type location = Precise_locs.precise_location           type offset           val equal_loc : location -> location -> bool           val equal_offset : offset -> offset -> bool           val pretty_loc : Format.formatter -> location -> unit           val pretty_offset : Format.formatter -> offset -> unit           val to_value : location -> value           val size : location -> Int_Base.t           val partially_overlap : location -> location -> bool           val check_non_overlapping :             (Cil_types.lval * location) list ->             (Cil_types.lval * location) list -> unit Eval.evaluated           val offset_cardinal_zero_or_one : offset -> bool           val no_offset : offset           val forward_field :             Cil_types.typ -> Cil_types.fieldinfo -> offset -> offset           val forward_index : Cil_types.typ -> value -> offset -> offset           val reduce_index_by_array_size :             size_expr:Cil_types.exp ->             index_expr:Cil_types.exp ->             Integer.t -> value -> value Eval.evaluated           val forward_variable :             Cil_types.typ ->             Cil_types.varinfo -> offset -> location Eval.or_bottom           val forward_pointer :             Cil_types.typ -> value -> offset -> location Eval.or_bottom           val eval_varinfo : Cil_types.varinfo -> location           val reduce_loc_by_validity :             for_writing:bool ->             bitfield:bool ->             Cil_types.lval -> location -> location Eval.evaluated           val backward_variable :             Cil_types.varinfo -> location -> offset Eval.or_bottom           val backward_pointer :             value -> offset -> location -> (value * offset) Eval.or_bottom           val backward_field :             Cil_types.typ ->             Cil_types.fieldinfo -> offset -> offset Eval.or_bottom           val backward_index :             Cil_types.typ ->             index:value ->             remaining:offset -> offset -> (value * offset) Eval.or_bottom           val mem : 'Abstract_location.key -> bool           val get : 'Abstract_location.key -> (location -> 'a) option           val set : 'Abstract_location.key -> '-> location -> location         end       module Dom :         sig           type state           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           module Set :             sig               type elt = t               type t               val empty : t               val is_empty : t -> bool               val mem : elt -> t -> bool               val add : elt -> t -> t               val singleton : elt -> t               val remove : elt -> t -> t               val union : t -> t -> t               val inter : t -> t -> t               val diff : t -> t -> t               val subset : t -> t -> bool               val iter : (elt -> unit) -> t -> unit               val fold : (elt -> '-> 'a) -> t -> '-> 'a               val for_all : (elt -> bool) -> t -> bool               val exists : (elt -> bool) -> t -> bool               val filter : (elt -> bool) -> t -> t               val partition : (elt -> bool) -> t -> t * t               val cardinal : t -> int               val elements : t -> elt list               val choose : t -> elt               val split : elt -> t -> t * bool * t               val find : elt -> t -> elt               val of_list : elt list -> t               val min_elt : t -> elt               val max_elt : t -> elt               val nearest_elt_le : elt -> t -> elt               val nearest_elt_ge : elt -> t -> elt               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 Map :             sig               type key = t               type +'a t               val empty : 'a t               val is_empty : 'a t -> bool               val mem : key -> 'a t -> bool               val add : key -> '-> 'a t -> 'a t               val singleton : key -> '-> 'a t               val remove : key -> 'a t -> 'a t               val merge :                 (key -> 'a option -> 'b option -> 'c option) ->                 'a t -> 'b t -> 'c t               val compare : ('-> '-> int) -> 'a t -> 'a t -> int               val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool               val iter : (key -> '-> unit) -> 'a t -> unit               val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b               val for_all : (key -> '-> bool) -> 'a t -> bool               val exists : (key -> '-> bool) -> 'a t -> bool               val filter : (key -> '-> bool) -> 'a t -> 'a t               val partition : (key -> '-> bool) -> 'a t -> 'a t * 'a t               val cardinal : 'a t -> int               val bindings : 'a t -> (key * 'a) list               val min_binding : 'a t -> key * 'a               val max_binding : 'a t -> key * 'a               val choose : 'a t -> key * 'a               val split : key -> 'a t -> 'a t * 'a option * 'a t               val find : key -> 'a t -> 'a               val map : ('-> 'b) -> 'a t -> 'b t               val mapi : (key -> '-> 'b) -> 'a t -> 'b t               module Key :                 sig                   type t = key                   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 (Data : Datatype.S->                   sig                     type t = Data.t t                     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             end           module Hashtbl :             sig               type key = t               type 'a t               val create : int -> 'a t               val clear : 'a t -> unit               val reset : 'a t -> unit               val copy : 'a t -> 'a t               val add : 'a t -> key -> '-> unit               val remove : 'a t -> key -> unit               val find : 'a t -> key -> 'a               val find_all : 'a t -> key -> 'a list               val replace : 'a t -> key -> '-> unit               val mem : 'a t -> key -> bool               val iter : (key -> '-> unit) -> 'a t -> unit               val filter_map_inplace :                 (key -> '-> 'a option) -> 'a t -> unit               val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b               val length : 'a t -> int               val stats : 'a t -> Hashtbl.statistics               val iter_sorted :                 ?cmp:(key -> key -> int) ->                 (key -> '-> unit) -> 'a t -> unit               val fold_sorted :                 ?cmp:(key -> key -> int) ->                 (key -> '-> '-> 'b) -> 'a t -> '-> 'b               val iter_sorted_by_entry :                 cmp:(key * '-> key * '-> int) ->                 (key -> '-> unit) -> 'a t -> unit               val fold_sorted_by_entry :                 cmp:(key * '-> key * '-> int) ->                 (key -> '-> '-> 'b) -> 'a t -> '-> 'b               val iter_sorted_by_value :                 cmp:('-> '-> int) -> (key -> '-> unit) -> 'a t -> unit               val fold_sorted_by_value :                 cmp:('-> '-> int) ->                 (key -> '-> '-> 'b) -> 'a t -> '-> 'b               val structural_descr : Structural_descr.t -> Structural_descr.t               val make_type : 'Type.t -> 'a t Type.t               val memo : 'a t -> key -> (key -> 'a) -> 'a               module Key :                 sig                   type t = key                   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 (Data : Datatype.S->                   sig                     type t = Data.t t                     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             end           val top : t           val is_included : t -> t -> bool           val join : t -> t -> t           val join_and_is_included : t -> t -> t * bool           val widen :             Cil_types.kernel_function -> Cil_types.stmt -> t -> t -> t           type value = Val.t           type location = Loc.location           type origin           val extract_expr :             (Cil_types.exp -> value Eval.evaluated) ->             t -> Cil_types.exp -> (value * origin) Eval.evaluated           val extract_lval :             (Cil_types.exp -> value Eval.evaluated) ->             t ->             Cil_types.lval ->             Cil_types.typ -> location -> (value * origin) Eval.evaluated           val backward_location :             t ->             Cil_types.lval ->             Cil_types.typ ->             location -> value -> (location * value) Eval.or_bottom           val reduce_further :             t -> Cil_types.exp -> value -> (Cil_types.exp * value) list           type return           module Return :             sig               type t = return               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 Transfer :             functor               (Valuation : sig                              type t                              type value = value                              type origin = origin                              type loc = location                              val find :                                t ->                                Cil_types.exp ->                                (value, origin) Eval.record_val Eval.or_top                              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                            end->               sig                 type state = t                 type return = return                 type value = value                 type location = location                 type valuation = Valuation.t                 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               end           val compute_using_specification :             Cil_types.kinstr ->             Cil_types.kernel_function * Cil_types.funspec ->             t -> (t, return, value) Eval.call_result           type eval_env           val env_current_state : eval_env -> t Eval.or_bottom           val env_annot : pre:t -> here:t -> unit -> eval_env           val env_pre_f : pre:t -> unit -> eval_env           val env_post_f :             pre:t ->             post:t -> result:Cil_types.varinfo option -> unit -> eval_env           val eval_predicate :             eval_env -> Cil_types.predicate -> Alarmset.status           val reduce_by_predicate :             eval_env -> bool -> Cil_types.predicate -> eval_env           val enter_scope :             Cil_types.kernel_function -> Cil_types.varinfo list -> t -> t           val leave_scope :             Cil_types.kernel_function -> Cil_types.varinfo list -> t -> t           val empty : unit -> t           val initialize_var :             t ->             Cil_types.lval -> location -> (value * bool) Eval.or_bottom -> t           val initialize_var_using_type : t -> Cil_types.varinfo -> t           val global_state : unit -> t Eval.or_bottom option           val filter_by_bases : Base.Hptset.t -> t -> t           val reuse : current_input:t -> previous_output:t -> t           val structure : t Abstract_domain.structure           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           val mem : 'Abstract_domain.key -> bool           val get : 'Abstract_domain.key -> (state -> 'a) option           val set : 'Abstract_domain.key -> '-> state -> state         end       type state = Dom.state       type value = Val.t       val get_stmt_state : Cil_types.stmt -> state Eval.or_bottom       val eval_expr : state -> Cil_types.exp -> value Eval.evaluated     end   val current : (module Analysis.SPervasives.ref   val compute :     Abstractions.config -> ?library:bool -> Cil_types.kernel_function -> unit   val force_compute : unit -> unit   val cvalue_initial_state : unit -> Cvalue.Model.t end