E_ACSL.Rte
Accessing the RTE plug-in easily.
val stmt :
?warn:bool ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.code_annotation list
RTEs of a given stmt, as a list of code annotations.
val exp :
?warn:bool ->
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
RTEs of a given exp, as a list of code annotations.
val get_state_selection_with_dependencies :
unit ->
Frama_c_kernel.State_selection.t
Equivalent to State_selection.with_dependencies RteGen.Api.self
if the RTE plug-in is enabled, empty otherwise.