Module NormAtLabels

module NormAtLabels: sig .. end

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 : exit:bool -> label_mapping
val labels_fct_assigns : exit:bool -> label_mapping
val labels_assert : kf:Cil_types.kernel_function -> Cil_types.stmt -> label_mapping
val labels_loop : 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 -> label_mapping
val labels_stmt_assigns : kf:Cil_types.kernel_function -> Cil_types.stmt -> label_mapping
val labels_stmt_post_l : kf:Cil_types.kernel_function ->
Cil_types.stmt -> Clabels.c_label option -> label_mapping
val labels_stmt_assigns_l : 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
val preproc_assigns : label_mapping -> Cil_types.from list -> Cil_types.from list
val has_postassigns : Cil_types.assigns -> bool