Module Gauges_domain.D_Impl

module D_Impl: sig .. end

type value = Cvalue.V.t 
type state = Gauges_domain.G.t 
type location = Precise_locs.precise_location 
include G
val structure : 'a Abstract_domain.structure
val empty : 'a -> Gauges_domain.G.MV.t * 'b list
val pretty : Format.formatter -> Gauges_domain.G.t -> unit
val enter_scope : 'a -> 'b -> 'c -> 'c
val leave_scope : 'a ->
Cil_types.varinfo list -> state -> Gauges_domain.G.t
type origin = unit 
type return = unit 
module Return: Datatype.Unit
module Transfer: 
functor (Valuation : Abstract_domain.Valuation with type value = value and type origin = origin and type loc = location) -> sig .. end
val compute_using_specification : 'a ->
Kernel_function.t * 'b ->
Gauges_domain.G.t ->
[> `Value of (Gauges_domain.G.t, unit, Cvalue.V.t) Eval.return_state list ]
val extract_expr : 'a -> 'b -> 'c -> [> `Value of Cvalue.V.t * unit ] * Alarmset.t
val extract_lval : 'a ->
t ->
'b ->
Cil_datatype.Typ.t ->
Precise_locs.precise_location ->
[> `Value of Cvalue.V.t * unit ] * Alarmset.t
val backward_location : 'a -> 'b -> 'c -> 'd -> 'e -> [> `Value of 'd * 'e ]
val reduce_further : 'a -> 'b -> 'c -> 'd list
val filter_by_bases : 'a -> 'b -> 'b
val reuse : current_input:'a -> previous_output:'b -> 'b
val global_state : unit -> 'a option
val initialize_var_using_type : 'a -> 'b -> 'a
val initialize_var : 'a -> 'b -> 'c -> 'd -> 'a
type eval_env = state 
val env_current_state : 'a -> [> `Value of 'a ]
val env_annot : pre:'a -> here:'b -> unit -> 'b
val env_pre_f : pre:'a -> unit -> 'a
val env_post_f : pre:'a -> post:'b -> result:'c -> unit -> 'b
val eval_predicate : 'a -> 'b -> Alarmset.status
val reduce_by_predicate : 'a -> 'b -> 'c -> 'a
val top : Gauges_domain.G.MV.t * 'a list