Index of values

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]
D
default [Flags]

Defaults flags are taken from the Kernel and RTE plug-in options.

divmod_assertion [Rte]
dkey_annot [Options]
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]
L
lval_assertion [Rte]
lval_initialized_assertion [Rte]
M
mem [Parameter_sig.Set]

Does the given element belong to the set?

mult_sub_add_assertion [Rte]
N
none [Flags]

All flags set to false, empty for initialized

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]