diff --git a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 index 9648bdc10443ed063e1ec625b99d5978f5ad47c9..cda898dd5cb7d284cd405a790cd08631cead058b 100644 --- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 +++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 @@ -111,6 +111,9 @@ redirect all output to a given file. .B -F, --frama-c-extra=\fI<FLAGS> pass an extra option to a \fBFrama-C\fP invocation. .TP +.B -a, --rte +annotate a source program with assertions validating pointer or array access prior to instrumentation. +.TP .B -m, --memory-model=\fI<model> memory model (i.e., a runtime library for checking memory related annotations) to be linked against the instrumented file.