Class NormAtLabels.norm_at

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 :
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