Module Gauges_domain.G

module G: sig .. end

val opt2 : ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option
val cache_name : string -> Hptmap_sig.cache_type
module Bounds: sig .. end
module MV: sig .. end
module MC: sig .. end
val sub_min_max_cvalue : Cvalue.V.t -> Cvalue.V.t -> Bounds.t option
val sub_mv : MV.t -> MV.t -> MC.t
val mv_minus_mc : MV.t -> MC.t -> MV.t
val forget : Bounds.t ->
MV.t -> MC.t -> MV.t
type multiple_iterations = {
   nb : Bounds.t;
   coeffs : MC.t;
}
module MultipleIterations: sig .. end
type iteration_info = 
| PreciseIteration of int
| MultipleIterations of multiple_iterations
module IterationInfo: sig .. end
include struct ... end
val empty : MV.t * 'a list
val top : t -> t
val pretty_iteration_info : Format.formatter -> iteration_info -> unit
val pretty_loop_step : Format.formatter -> Cil_types.stmt * iteration_info -> unit
val pretty_loop_info : Datatype.List(Datatype.Pair(Cil_datatype.Stmt)(IterationInfo)).t
Pretty_utils.formatter
val pretty : Format.formatter -> t -> unit
val inc : t -> t
val remove_coeffs : MC.t -> int -> MV.t -> MV.t
val join_consecutive_lambda : int ->
MV.t ->
MV.t ->
MC.t * MV.t * MV.t
val join_same_lambda : MV.t -> MV.t -> MV.t
exception MessyJoin
val join_iterations : t ->
t ->
MV.t * MV.t *
(Cil_datatype.Stmt.t * iteration_info) list * bool
val join : t -> t -> t
val is_included : t -> t -> bool
val join_and_is_included : t -> t -> t * bool
val widen : 'a -> Cil_datatype.Stmt.t -> t -> t -> t
val enter_loop : Cil_datatype.Stmt.t -> t -> t
val leave_loop : Cil_datatype.Stmt.t -> t -> t
val tracked_variable : Cil_types.varinfo -> bool
val kill_base : MC.key -> t -> t
exception Untranslatable
module Gauge: sig .. end
val extract_gauge : t -> MV.key -> Gauge.t option
val eval_gauge : t -> Gauge.t -> Cvalue.V.t
val backward_loop : t -> MC.key -> Cvalue.V.t -> t option
val loc_to_base : Locations.location -> Cil_datatype.Typ.t -> Base.t
val gauge_from_state : MV.key -> t -> Gauge.t
val translate_exp : t ->
(Cil_types.lval -> Locations.location) ->
(Cil_types.exp -> Cvalue.V.t) -> Cil_types.exp -> Gauge.t
val store_gauge : MC.key -> Gauge.t -> t -> t
val assign : (Cil_types.lval -> Locations.location) ->
(Cil_types.exp -> Cvalue.V.t) -> Cil_types.lval -> Cil_types.exp -> t -> t