NormAtLabels (frama-c-wp.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_assert : 
  kf:Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  label_mapping

val labels_loop : Frama_c_kernel.Cil_types.stmt -> label_mapping

val labels_stmt_pre : 
  kf:Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  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_assigns : 
  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_stmt_assigns_l : 
  kf:Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  Clabels.c_label option ->
  label_mapping

val labels_predicate : 
  (Frama_c_kernel.Cil_types.logic_label * Frama_c_kernel.Cil_types.logic_label)
    list ->
  label_mapping

val labels_axiom : label_mapping

val preproc_term : 
  label_mapping ->
  Frama_c_kernel.Cil_types.term ->
  Frama_c_kernel.Cil_types.term

val preproc_annot : 
  label_mapping ->
  Frama_c_kernel.Cil_types.predicate ->
  Frama_c_kernel.Cil_types.predicate

val preproc_assigns : 
  label_mapping ->
  Frama_c_kernel.Cil_types.from list ->
  Frama_c_kernel.Cil_types.from list

val has_postassigns : Frama_c_kernel.Cil_types.assigns -> bool