E_ACSL.RteAccessing 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 listRTEs 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 listRTEs of a given exp, as a list of code annotations.
val get_state_selection_with_dependencies :
unit ->
Frama_c_kernel.State_selection.tEquivalent to State_selection.with_dependencies RteGen.Api.self if the RTE plug-in is enabled, empty otherwise.