Index of values


_ignore [Register]

A
accessor [Generator.S]
all [Flags]
All flags set to true.
all_statuses [Generator]
annotate [Visit]
Annotate kernel-function with respect to options and current generator status.
annotate [RteGen.Visit]

B
bool_value [Rte]

C
compute [Register]

D
default [Flags]
Defaults flags are taken from the Kernel and RTE plug-in options.
divmod_assertion [Rte]
do_all_rte [Register]
do_rte [Register]
downcast_assertion [Rte]

E
emitter [Generator]
The Emitter for Annotations registered by RTE
exists [Parameter_sig.Set]
Is there some element satisfying the given predicate?

F
finite_float_assertion [Rte]
float_to_int_assertion [Rte]

G
get_annotations_exp [Visit]
Returns annotations associated to alarms without registering them.
get_annotations_exp [RteGen.Visit]
get_annotations_kf [Visit]
Returns annotations associated to alarms without registering them.
get_annotations_kf [RteGen.Visit]
get_annotations_lval [Visit]
Returns annotations associated to alarms without registering them.
get_annotations_lval [RteGen.Visit]
get_annotations_stmt [Visit]
Returns annotations associated to alarms without registering them.
get_annotations_stmt [RteGen.Visit]
get_registered_annotations [Generator]
Returns all annotations actually registered by RTE so far

I
is_computed [Generator.S]
iter_exp [Visit]
iter_exp [RteGen.Visit]
iter_instr [Visit]
iter_instr [RteGen.Visit]
iter_lval [Visit]
iter_lval [RteGen.Visit]
iter_stmt [Visit]
iter_stmt [RteGen.Visit]

J
journal_register [Register]

L
lval_assertion [Rte]
lval_initialized_assertion [Rte]

M
main [Register]
mem [Parameter_sig.Set]
Does the given element belong to the set?
mult_sub_add_assertion [Rte]

N
nojournal_register [Register]
none [Flags]
All flags set to false.

O
off [Parameter_sig.Bool]
Set the boolean to false.
on [Parameter_sig.Bool]
Set the boolean to true.

P
pointer_call [Rte]
pointer_value [Rte]

R
register [Visit]
Registers and returns the annotation associated with the alarm, and a boolean flag indicating whether it has been freshly generated or not.
register [RteGen.Visit]

S
set [Generator.S]
shift_negative_assertion [Rte]
shift_overflow_assertion [Rte]
shift_width_assertion [Rte]
signed_div_assertion [Rte]
status [Visit]
Returns a False_if_reachable status when invalid.

U
uminus_assertion [Rte]

W
warn [Options]