Module Wp.NormAtLabels

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_stmt_post : kf:Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> label_mapping
val labels_stmt_post_l : kf:Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> Clabels.c_label option -> label_mapping
val labels_axiom : label_mapping
val has_postassigns : Frama_c_kernel.Cil_types.assigns -> bool