sig
val catch_label_error : exn -> string -> string -> unit
type label_mapping
val labels_empty : NormAtLabels.label_mapping
val labels_fct_pre : NormAtLabels.label_mapping
val labels_fct_post : NormAtLabels.label_mapping
val labels_fct_assigns : NormAtLabels.label_mapping
val labels_assert_before : Cil_types.stmt -> NormAtLabels.label_mapping
val labels_assert_after :
Cil_types.stmt ->
Cil_types.logic_label option -> NormAtLabels.label_mapping
val labels_loop_inv : Cil_types.stmt -> NormAtLabels.label_mapping
val labels_loop_assigns : Cil_types.stmt -> NormAtLabels.label_mapping
val labels_stmt_pre : Cil_types.stmt -> NormAtLabels.label_mapping
val labels_stmt_post :
Cil_types.stmt ->
Cil_types.logic_label option -> NormAtLabels.label_mapping
val labels_stmt_assigns :
Cil_types.stmt ->
Cil_types.logic_label option -> NormAtLabels.label_mapping
val labels_predicate :
(Cil_types.logic_label * Cil_types.logic_label) list ->
NormAtLabels.label_mapping
val labels_axiom : NormAtLabels.label_mapping
val preproc_annot :
NormAtLabels.label_mapping ->
Cil_types.predicate Cil_types.named ->
Cil_types.predicate Cil_types.named
val preproc_assigns :
NormAtLabels.label_mapping ->
Cil_types.identified_term Cil_types.from list ->
Cil_types.identified_term Cil_types.from list
val preproc_label :
NormAtLabels.label_mapping ->
Cil_types.logic_label -> Cil_types.logic_label
end