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:
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 ]
: 'a -> 'b -> 'c -> [> `Value of Cvalue.V.t * unit ] * Alarmset.t
: '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