Functor Gauges_domain.D_Impl.Transfer

module Transfer: 
functor (Valuation : Abstract_domain.Valuation with type value = value and type origin = origin and type loc = location) -> sig .. end
Parameters:
Valuation : Abstract_domain.Valuation with type value = value and type origin = origin and type loc = location

type value = Cvalue.V.t 
type state = Gauges_domain.G.t 
type location = Precise_locs.precise_location 
type return = unit 
type valuation = Valuation.t 
val update : 'a -> 'b -> 'b
val assign : 'a ->
Precise_locs.precise_location Eval.left_value ->
Cil_types.exp ->
'b ->
Valuation.t ->
state -> [> `Value of Gauges_domain.G.t ]
val assume : 'a -> 'b -> 'c -> Valuation.t -> t -> [> `Value of t ]
val make_return : 'a -> 'b -> 'c -> 'd -> 'e -> unit
val finalize_call : 'a -> 'b -> pre:'c -> post:'c -> [> `Value of 'c ]
val assign_return : 'a ->
Precise_locs.precise_location Eval.left_value ->
'b ->
unit ->
'c ->
'd -> state -> [> `Value of Gauges_domain.G.t ]
val start_call : 'a -> Cvalue.V.t Eval.call -> 'b -> t -> (t, 'c, 'd) Eval.call_action
val default_call : 'a ->
'b Eval.call ->
Gauges_domain.G.t ->
[> `Value of (Gauges_domain.G.t, unit, Cvalue.V.t) Eval.return_state list ]
val enter_loop : Cil_datatype.Stmt.t -> Gauges_domain.G.t -> Gauges_domain.G.t
val incr_loop_counter : 'a -> Gauges_domain.G.t -> Gauges_domain.G.t
val leave_loop : Cil_datatype.Stmt.t -> Gauges_domain.G.t -> Gauges_domain.G.t