Frama-C API - NormAtLabels
val labels_empty : label_mappingval labels_fct_pre : label_mappingval labels_fct_post : exit:bool -> label_mappingval labels_fct_assigns : exit:bool -> label_mappingval labels_assert : kf:Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> label_mappingval labels_loop : Frama_c_kernel.Cil_types.stmt -> label_mappingval labels_stmt_pre : kf:Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> label_mappingval labels_stmt_post : kf:Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> label_mappingval labels_stmt_assigns : kf:Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> label_mappingval labels_stmt_post_l : kf:Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> Clabels.c_label option -> label_mappingval labels_stmt_assigns_l : kf:Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> Clabels.c_label option -> label_mappingval labels_predicate : (Frama_c_kernel.Cil_types.logic_label * Frama_c_kernel.Cil_types.logic_label) list -> label_mappingval labels_axiom : label_mappingval preproc_term : label_mapping -> Frama_c_kernel.Cil_types.term -> Frama_c_kernel.Cil_types.termval preproc_annot : label_mapping -> Frama_c_kernel.Cil_types.predicate -> Frama_c_kernel.Cil_types.predicateval preproc_assigns : label_mapping -> Frama_c_kernel.Cil_types.from list -> Frama_c_kernel.Cil_types.from listval has_postassigns : Frama_c_kernel.Cil_types.assigns -> bool