module NormAtLabels: sig
.. 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.
val catch_label_error : exn -> string -> string -> unit
type
label_mapping
val labels_empty : label_mapping
val labels_fct_pre : label_mapping
val labels_fct_post : label_mapping
val labels_fct_assigns : label_mapping
val labels_assert_before : kf:Cil_types.kernel_function -> Cil_types.stmt -> label_mapping
val labels_assert_after : kf:Cil_types.kernel_function ->
Cil_types.stmt -> Clabels.c_label option -> label_mapping
val labels_loop_inv : established:bool -> Cil_types.stmt -> label_mapping
val labels_loop_assigns : Cil_types.stmt -> label_mapping
val labels_stmt_pre : kf:Cil_types.kernel_function -> Cil_types.stmt -> label_mapping
val labels_stmt_post : kf:Cil_types.kernel_function ->
Cil_types.stmt -> Clabels.c_label option -> label_mapping
val labels_stmt_assigns : kf:Cil_types.kernel_function ->
Cil_types.stmt -> Clabels.c_label option -> label_mapping
val labels_predicate : (Cil_types.logic_label * Cil_types.logic_label) list ->
label_mapping
val labels_axiom : label_mapping
val preproc_annot : label_mapping -> Cil_types.predicate -> Cil_types.predicate
Raises LabelError
if there is a label in p
that is incompatible
with the labels
translation
val preproc_assigns : label_mapping -> Cil_types.from list -> Cil_types.from list
Raises LabelError
if there is a label in p
that is incompatible
with the labels
translation