From 396490f4056b0182b32ab9958aa50ee91f996611 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Fri, 24 Jun 2016 13:07:28 +0200
Subject: [PATCH] Update man page for e-acsl-gcc.sh with --rte option

---
 src/plugins/e-acsl/man/e-acsl-gcc.sh.1 | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

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 46a5565d776..fbce9931bcf 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)
-- 
GitLab