RteGen.Flags
Flags for filtering Alarms
Filtering Categories of Alarms
type t = {
remove_trivial : bool; |
initialized : Frama_c_kernel.Kernel_function.Set.t; |
mem_access : bool; |
div_mod : bool; |
shift : bool; |
left_shift_negative : bool; |
right_shift_negative : bool; |
signed_overflow : bool; |
unsigned_overflow : bool; |
signed_downcast : bool; |
unsigned_downcast : bool; |
pointer_downcast : bool; |
float_to_int : bool; |
finite_float : bool; |
pointer_call : bool; |
pointer_value : bool; |
bool_value : bool; |
}
Flags for controling the low-level API. Each flag control whether a category of alarms will be visited or not.
val default :
?remove_trivial:bool ->
?initialized:Frama_c_kernel.Kernel_function.Set.t ->
?mem_access:bool ->
?div_mod:bool ->
?shift:bool ->
?left_shift_negative:bool ->
?right_shift_negative:bool ->
?signed_overflow:bool ->
?unsigned_overflow:bool ->
?signed_downcast:bool ->
?unsigned_downcast:bool ->
?pointer_downcast:bool ->
?float_to_int:bool ->
?finite_float:bool ->
?pointer_call:bool ->
?pointer_value:bool ->
?bool_value:bool ->
unit ->
t
Defaults flags are taken from the Kernel and RTE plug-in options.
val all : unit -> t
All flags set to true
, "@all" for initialized
val none : t
All flags set to false
, empty for initialized