Module `RteGen.Visit`Source

Visitors to iterate over Alarms and/or generate Code-Annotations

val annotate : 
  ?flags:Flags.t ->
  Frama_c_kernel.Cil_types.kernel_function ->
  unit

Source

val get_annotations_kf : 
  ?flags:Flags.t ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.code_annotation list

Source

val get_annotations_stmt : 
  ?flags:Flags.t ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.code_annotation list

Source

val get_annotations_exp : 
  ?flags:Flags.t ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.exp ->
  Frama_c_kernel.Cil_types.code_annotation list

Source

val get_annotations_lval : 
  ?flags:Flags.t ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.lval ->
  Frama_c_kernel.Cil_types.code_annotation list

Source

type on_alarm =
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  invalid:bool ->
  Frama_c_kernel.Alarms.alarm ->
  unit

Source

type 'a iterator =
  ?flags:Flags.t ->
  on_alarm ->
  Frama_c_kernel.Kernel_function.t ->
  Frama_c_kernel.Cil_types.stmt ->
  'a ->
  unit

Sourceval iter_lval : Frama_c_kernel.Cil_types.lval iterator

Sourceval iter_exp : Frama_c_kernel.Cil_types.exp iterator

Sourceval iter_instr : Frama_c_kernel.Cil_types.instr iterator

Sourceval iter_stmt : Frama_c_kernel.Cil_types.stmt iterator

Source

val register : 
  Frama_c_kernel.Emitter.t ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  invalid:bool ->
  Frama_c_kernel.Alarms.alarm ->
  Frama_c_kernel.Cil_types.code_annotation * bool

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/frama-c-rtegen.core/RteGen/Visit/index.html

Module `RteGen.Visit`Source

package frama-c

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/frama-c-rtegen.core/RteGen/Visit/index.html

Module RteGen.VisitSource

dune-project
Dependency

Module `RteGen.Visit`Source