From bad792f3f27e8ec882f74a0266a30d301c04ad25 Mon Sep 17 00:00:00 2001 From: Julien Signoles <julien.signoles@cea.fr> Date: Thu, 28 Nov 2019 19:10:38 +0100 Subject: [PATCH] [E-ACSL:doc] consistency (capitalization, etc) --- src/plugins/e-acsl/man/e-acsl-gcc.sh.1 | 38 +++++++++++++------------- 1 file changed, 19 insertions(+), 19 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 1fad5fba936..1c311181133 100644 --- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 +++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 @@ -46,17 +46,17 @@ compile the generated and the original (supplied) sources. By default no compilation is performed. .TP .B -D, --rt-debug -Enable runtime debug features, i.e., compile unoptimized executable +enable runtime debug features, i.e., compile unoptimized executable with assertions and extra checks. .TP .B --no-trace -Disable stack trace reporting in debug mode +disable stack trace reporting in debug mode .TP .B -V, --rt-verbose -Output extra messages when executing generated code +output extra messages when executing generated code .TP .B -X, --instrumented-only -Do not compile original code. Has effect only in the presence of the \fI-c\fP +do not compile original code. Has effect only in the presence of the \fI-c\fP flag. .TP .B -C, --compile-only @@ -157,23 +157,23 @@ Valid arguments are: \fIall\fP \- all of the above. .TP .B -A, --rte-select=\fI<OPTSTRING> -Restrict annotations to a given list of functions. +restrict annotations to a given list of functions. \fIOPTSTRING\fP is a comma-separated string comprising function names. .TP .B --stack-size=\fI<NUMBER> -Set the size (in MB) of the stack shadow space +set the size (in MB) of the stack shadow space .TP .B --heap-size=\fI<NUMBER> -Set the size (in MB) of the heap shadow space +set the size (in MB) of the heap shadow space .TP .B -k, --keep-going -Continue execution after an assertion failure +continue execution after an assertion failure .TP .B --free-valid-address -Trigger failure if a NULL-pointer is used as an input to free function +trigger failure if a NULL-pointer is used as an input to free function .TP .B --fail-with-code=\fI<NUMBER> -On assertion failure exit with the given integer code intead of raising an abort +on assertion failure exit with the given integer code intead of raising an abort signal .TP .B --external-assert=\fI<FILE> @@ -190,7 +190,7 @@ Valid arguments are: By default the Patricia trie memory model is used. .TP .B --print-mmodels -Print the names of the supported memory models +print the names of the supported memory models .TP .B -I, --frama-c=\fI<FILE> the name of the \fBFrama-C\fP executable. By default the @@ -205,42 +205,42 @@ the name of the \fBGCC\fP executable. By default the first \fIgcc\fP executable found in the system path is used. .TP .B --then -Separate with a \fB-then\fP the first \fBFrama-C\fP options from the actual +separate with a \fB-then\fP the first \fBFrama-C\fP options from the actual launch of the \fBE-ACSL\fP plugin. Prepends \fB-e-acsl-prepare\fP to the list of options passed to \fBFrama-C\fP. .TP .B --e-acsl-extra=\fI<OPTS> -Adds \fI<OPTS>\fP to the list of options that will be given to the \fBE-ACSL\fP +add \fI<OPTS>\fP to the list of options that will be given to the \fBE-ACSL\fP analysis. Only useful when \fB--then\fP is in use, in which case \fI<OPTS>\fP will be placed after the \fB-then\fP on \fBFrama-C\fP's command-line. Otherwise, equivalent to \fB--frama-c-extra\fP .SH EXIT STATUS .TP .B 0 -Successful execution +successful execution .TP .B 1 -Invalid user input +invalid user input .TP .B \fBFrama-C\fP or \fBGCC\fP error code -Instrumentation- or compile-time error +instrumentation- or compile-time error .SH EXAMPLES .B e-acsl-gcc.sh foo.c -Instrument foo.c and output the instrumented code to \fIa.out.frama.c\fP. +instrument foo.c and output the instrumented code to \fIa.out.frama.c\fP. .B e-acsl-gcc.sh -P -c -ogen_foo.c -Ofoo foo.c -Instrument \fIfoo.c\fP, output the instrumented code to \fIgen_foo.c\fP and +instrument \fIfoo.c\fP, output the instrumented code to \fIgen_foo.c\fP and compile \fIfoo.c\fP into \fIfoo\fP and \fIgen_foo.c\fP into \fIfoo.e-acsl\fP. The \fB-P\fP option specifies that the instrumentation should omit debug functionality. .B e-acsl-gcc.sh --memory-model=bittree -C gen_foo.c -Assume \fIgen_foo.c\fP has been instrumented by \fBE-ACSL\fP and compile it into +assume \fIgen_foo.c\fP has been instrumented by \fBE-ACSL\fP and compile it into \fIa.out.e-acsl\fP using \fBbittree\fP memory model. .SH SEE ALSO -- GitLab