Index of modules

B
Bool_value [Generator]
D
Div_mod [Generator]
DoDivMod [Options]
DoFloatToInt [Options]
DoInitialized [Options]
DoMemAccess [Options]
DoPointerCall [Options]
DoShift [Options]
E
Enabled [Options]
F
Finite_float [Generator]
Flags

Filtering Categories of Alarms

Flags [RteGen]

Flags for filtering Alarms

Float_to_int [Generator]
FunctionSelection [Options]
G
Generator
Generator [RteGen]

RTE Generator Status & Emitters

I
Initialized [Generator]
L
Left_shift_negative [Generator]
M
Mem_access [Generator]
O
Options
P
Pointer_call [Generator]
Pointer_downcast [Generator]
Pointer_value [Generator]
R
Register

Register the plugin in the Frama-C kernel.

Right_shift_negative [Generator]
Rte
RteGen

Consult internal plug-in documentation for more details

S
Shift [Generator]
Signed_downcast [Generator]
Signed_overflow [Generator]
T
Trivial [Options]
U
Unsigned_downcast [Generator]
Unsigned_overflow [Generator]
V
Visit

Runtime Error annotation generation plugin

Visit [RteGen]

Visitors to iterate over Alarms and/or generate Code-Annotations

W
Warn [Options]