sig   module Make :     functor       (Value : Abstract_value.S) (Left : 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 = Value.t                                            type 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                                          end) (Right : 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 =                                                              Left.value                                                          type location =                                                              Left.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                                                        end->       sig         type state = Left.state * Right.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 = Value.t         type location = Left.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       end end