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 :
    kf:Cil_types.kernel_function ->
    Cil_types.stmt -> NormAtLabels.label_mapping
  val labels_assert_after :
    kf:Cil_types.kernel_function ->
    Cil_types.stmt -> Clabels.c_label option -> 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 -> Clabels.c_label option -> NormAtLabels.label_mapping
  val labels_stmt_assigns :
    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_annot :
    NormAtLabels.label_mapping -> Cil_types.predicate -> Cil_types.predicate
  val preproc_assigns :
    NormAtLabels.label_mapping -> Cil_types.from list -> Cil_types.from list
end