Module `Wp.NormAtLabels`Source

Sourceval catch_label_error : exn -> string -> string -> unit

Sourcetype label_mapping

Sourceval labels_empty : label_mapping

Sourceval labels_fct_pre : label_mapping

Sourceval labels_fct_post : exit:bool -> label_mapping

Sourceval 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

Sourceval labels_loop : Frama_c_kernel.Cil_types.stmt -> label_mapping

Source

val labels_stmt_pre : 
  kf:Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  label_mapping

Source

val labels_stmt_post : 
  kf:Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  label_mapping

Source

val labels_stmt_assigns : 
  kf:Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  label_mapping

Source

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

Source

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

Source

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

Sourceval labels_axiom : label_mapping

Source

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

Source

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

Source

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

Sourceval has_postassigns : Frama_c_kernel.Cil_types.assigns -> bool

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/NormAtLabels/index.html

Module `Wp.NormAtLabels`Source

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/NormAtLabels/index.html

Module Wp.NormAtLabelsSource

Module `Wp.NormAtLabels`Source