Frama-C API - `Generator`

RTE Generator Status & Emitters

type status_accessor = string * (Frama_c_kernel.Cil_types.kernel_function -> bool -> unit) * (Frama_c_kernel.Cil_types.kernel_function -> bool)

module type S = sig ... end

module Initialized : S

module Mem_access : S

module Pointer_value : S

module Pointer_call : S

module Div_mod : S

module Shift : S

module Left_shift_negative : S

module Right_shift_negative : S

module Signed_overflow : S

module Signed_downcast : S

module Unsigned_overflow : S

module Unsigned_downcast : S

module Pointer_downcast : S

module Float_to_int : S

module Finite_float : S

module Bool_value : S

val all_statuses : status_accessor list

val emitter : Frama_c_kernel.Emitter.t

The Emitter for Annotations registered by RTE

val get_registered_annotations : Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.code_annotation list

Returns all annotations actually registered by RTE so far

val self : Frama_c_kernel.State.t

Frama-C API - Generator