Frama-C:
Plug-ins:
Libraries:

Frama-C API - Flags

Flags for filtering Alarms

Filtering Categories of Alarms

type t = {
  1. remove_trivial : bool;
  2. initialized : Frama_c_kernel.Kernel_function.Set.t;
  3. mem_access : bool;
  4. div_mod : bool;
  5. shift : bool;
  6. left_shift_negative : bool;
  7. right_shift_negative : bool;
  8. signed_overflow : bool;
  9. unsigned_overflow : bool;
  10. signed_downcast : bool;
  11. unsigned_downcast : bool;
  12. pointer_downcast : bool;
  13. float_to_int : bool;
  14. finite_float : bool;
  15. pointer_call : bool;
  16. pointer_alignment : bool;
  17. pointer_value : bool;
  18. bool_value : bool;
}

Flags for controlling 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_alignment: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