Frama-C:
Plug-ins:
Libraries:

Frama-C API - Red_statuses

This modules stores the alarms and properties for which a red status has been emitted.

type alarm_or_property =
  1. | Alarm of Frama_c_kernel.Alarms.t
  2. | Prop of Frama_c_kernel.Property.t
val is_red : Frama_c_kernel.Property.t -> bool
val is_red_in_callstack : Frama_c_kernel.Cil_types.kinstr -> alarm_or_property -> Callstack.t -> bool
val get_all : unit -> (Frama_c_kernel.Cil_types.kinstr * alarm_or_property * int) list
val report : unit -> unit
val register_hook : (alarm_or_property -> unit) -> unit