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