Frama-C:
Plug-ins:
Libraries:

Frama-C API - Api

  • deprecated Use Visit, Flags and Generator modules

Runtime Error Annotation Generation plugin.

val compute : unit -> unit

Same result as having -rte on the command line

Generates RTE for a single function. Uses the status of the various RTE options do decide which kinds of annotations must be generated.

Generates all possible RTE for a given function.

  • deprecated Use RteGen.Visit.annotate instead

Generates all possible RTE except pre-conditions for a given function.

  • deprecated Use RteGen.Visit.annotate instead
type status_accessor = string * (Frama_c_kernel.Cil_types.kernel_function -> bool -> unit) * (Frama_c_kernel.Cil_types.kernel_function -> bool)
val get_all_status : unit -> status_accessor list
val get_divMod_status : unit -> status_accessor
val get_initialized_status : unit -> status_accessor
val get_memAccess_status : unit -> status_accessor
val get_pointerCall_status : unit -> status_accessor
val get_signedOv_status : unit -> status_accessor
val get_signed_downCast_status : unit -> status_accessor
val get_unsignedOv_status : unit -> status_accessor
val get_unsignedDownCast_status : unit -> status_accessor
val get_pointer_downcast_status : unit -> status_accessor
val get_float_to_int_status : unit -> status_accessor
val get_finite_float_status : unit -> status_accessor
val get_pointer_value_status : unit -> status_accessor
val get_bool_value_status : unit -> status_accessor