package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c-rtegen.core/RteGen/Flags/index.html

Module `RteGen.Flags`Source

Flags for filtering Alarms

Filtering Categories of Alarms

Sourcetype 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.

Source

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.

Sourceval all : unit -> t

All flags set to true, "@all" for initialized

Sourceval none : t

All flags set to false, empty for initialized