Wp.NormAtLabels
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