class norm_at : (Cil_types.logic_label -> Cil_types.logic_label) ->
object
.. end
push the Tat down to the 'data' operations.
This can be useful in cases like \at (x + \at(y, Ly), Lx) because
it gives \at(x, Lx) + \at(y, Ly) so there is no more \at imbrications.
Also try to "normalize" label :
- remove Here because its meaning change when propagating,
- remove Old because its meaning depend on where it comes from.
Inherits
val mutable current_label : Cil_types.logic_label option
method private change_label : Cil_types.logic_label -> Cil_types.logic_label option
method private restore_term : Cil_types.logic_label option -> Cil_types.term -> Cil_types.term
method private restore_pred : Cil_types.logic_label option ->
Cil_types.predicate Cil_types.named -> Cil_types.predicate Cil_types.named
method vterm : Cil_types.term -> Cil_types.term Cil.visitAction
method vpredicate_named : Cil_types.predicate Cil_types.named ->
Cil_types.predicate Cil_types.named Cil.visitAction