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 46a5565d7765ee25f62393bc89c27301746baa38..fbce9931bcf00300153c7fa8f859b757c20762f9 100644 --- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 +++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 @@ -115,8 +115,19 @@ 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. +.B -a, --rte=\fI<OPTSTRING> +annotate a source program with assertions using a run of an RTE plugin prior to +E-ACSL. \fIOPTSTRING\fP is a comma-separated string that specifies the types of +generated assertions. +Valid arguments are: + \fImem\fP \- valid pointer or array accesses. + \fIint\fP \- integer overflows. + \fIfloat\fP \- casts from floating-point to integer. + \fIdiv\fP \- division by zero. + \fIret\fP \- return value in non-void functions. + \fIprecond\fP \- function calls based on contracts. + \fIshift\fP \- left and right shifts by a value out of bounds. + \fIall\fP \- all of the above. .TP .B -m, --memory-model=\fI<model> memory model (i.e., a runtime library for checking memory related annotations)