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 : exit:bool -> NormAtLabels.label_mapping
val labels_fct_assigns : exit:bool -> NormAtLabels.label_mapping
val labels_assert :
kf:Cil_types.kernel_function ->
Cil_types.stmt -> NormAtLabels.label_mapping
val labels_loop : Cil_types.stmt -> NormAtLabels.label_mapping
val labels_stmt_pre :
kf:Cil_types.kernel_function ->
Cil_types.stmt -> NormAtLabels.label_mapping
val labels_stmt_post :
kf:Cil_types.kernel_function ->
Cil_types.stmt -> NormAtLabels.label_mapping
val labels_stmt_assigns :
kf:Cil_types.kernel_function ->
Cil_types.stmt -> NormAtLabels.label_mapping
val labels_stmt_post_l :
kf:Cil_types.kernel_function ->
Cil_types.stmt -> Clabels.c_label option -> NormAtLabels.label_mapping
val labels_stmt_assigns_l :
kf:Cil_types.kernel_function ->
Cil_types.stmt -> Clabels.c_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_term :
NormAtLabels.label_mapping -> Cil_types.term -> Cil_types.term
val preproc_annot :
NormAtLabels.label_mapping -> Cil_types.predicate -> Cil_types.predicate
val preproc_assigns :
NormAtLabels.label_mapping -> Cil_types.from list -> Cil_types.from list
val has_postassigns : Cil_types.assigns -> bool
end