Improved the documentation of the e-acsl wrapper script

src/plugins/e-acsl/man/e-acsl-gcc.sh.1

@@ -33,100 +33,118 @@
 .I files
 .SH DESCRIPTION
 .B e-acsl-gcc.sh
-is convenience wrapper for instrumentation of C programs using the
-E-ACSL Frama-C plugin and their subsequent compilation using the GNU compiler
-collection (GCC).
+is a convenience wrapper for instrumentation of C programs using the
+\fBE-ACSL\fP \fBFrama-C\fP plugin and their subsequent compilation using
+the GNU compiler collection (\fBGCC\fP).
 .SH OPTIONS
+.TP
 .B -h, --help
-show help page.
+show a help page.
 .TP
 .B -c, --compile
-compile generated and original files.
+compile the generated and the original (supplied) sources.
+By default no compilation is performed.
 .TP
 .B -C, --compile-only
-compile input files as if they were generated by E-ACSL.
+compile the input files as if they were generated by \fBE-ACSL\fP.
 .TP
 .B -p, --print
-output the code generated by E-ACSL to \fISTDOUT\fP.
+output the code generated by E-ACSL to \fISTDOUT\fP using rich formatting
+features enabled via \fBpygmentize\fP. If no \fBpygmentize\fP
+executable is found in the system path, the generated sources are
+printed as is using the \fBcat\fP command.
 .TP \fI \fP
 .B -d, --debug=\fI<N>
-pass a value to Frama-C -debug option.
+pass a value to the \fBFrama-C\fP -\fIdebug\fP option.
+By default the -\fIdebug\fP flag is unused.
+.TP
+.B -v, --verbose=\fI<N>
+pass a value to the \fBFrama-C\fP -\fIverbose\fP option.
+By default the -\fIverbose\fP flag is unused.
 .TP
-.B -o, --ocode=\fI<FILENAME>
-name of the output source file. Defaults to \fIa.out.frama.c\fP.
+.B -o, --ocode=\fI<FILE>
+output the \fBE-ACSL\fP instrumented code to \fI<FILE>\fP.
+Defaults to \fIa.out.frama.c\fP.
 .TP
-.B -O, --oexec=\fI<FILENAME>
-name of the executable generated from the un-instrumented code.
-Executable compiled from the E-ACSL instrumented sources is
-appended \fI.e.acsl\fP suffix.
+.B -O, --oexec=\fI<FILE>
+output the code compiled from the uninstrumented sources to \fI<FILE>\fP.
+The executable compiled from the files generated by \fBE-ACSL\fP is
+appended the \fI.e.acsl\fP suffix.
 Unless specified, the
 names of the executables generated from the original
 and the modified programs are
 \fIa.out\fP and \fIa.out.e-acsl\fP respectively.
 .TP
-.B -v, --verbose=\fI<N>
-pass a value to the Frama-C -verbose option.
-.TP
 .B -f, --frama-c-only
-run input source files through Frama-C without E-ACSL instrumentations.
+run input source files through \fBFrama-C\fP without \fBE-ACSL\fP instrumentations.
 .TP
 .B -E, --extra-cpp-args=\fI<FLAGS>
-pass additional arguments to the Frama-C pre-processor.
+pass additional arguments to the \fBFrama-C\fP pre-processor.
 .TP
 .B -L, --frama-c-stdlib
-use Frama-C standard library instead of the system-wide one.
+use the \fBFrama-C\fP standard library instead of a system-wide one.
 .TP
 .B -M, --full-mmodel
-maximise memory-related instrumentation.
+maximize memory-related instrumentation.
 .TP
 .B -g, --gmp
 always use GMP integers instead of C integral types.
+By default the GMP integers are used on as-needed basis.
 .TP
 .B -l, --ld-flags=\fI<FLAGS>
 pass the specified flags to the linker.
 .TP
 .B -e, --cpp-flags=\fI<FLAGS>
 pass the specified flags to the pre-processor at compile-time.
-For instrumentation-time proprocessor flags see \fB--extra-cpp-args\fP option.
+For instrumentation-time pre-processor flags see \fB--extra-cpp-args\fP option.
 .TP
 .B -q, --quiet
-suppress any output except errors and warnings.
+suppress any output except for errors and warnings.
 .TP
 .B -s, --logfile=\fI<FILE>
 redirect all output to a given file.
 .TP
-.B -F, --frama-c-extra=\fI<OPTION>
-pass an extra option to frama-c invocation.
+.B -F, --frama-c-extra=\fI<FLAGS>
+pass an extra option to a \fBFrama-C\fP invocation.
 .TP
-.B -m, --memory-model=\fI<bittree|tree|list|splaytree>
-memory model (i.e., runtime library for checking memory related annotations)
+.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.
 
 Valid arguments are:
-  bittree     \- memory modelling using a Patricie trie ADT.
-  splaytree   \- memory modelling using a splay tree ADT.
-  list        \- memory modelling using a linked-list ADT.
-  tree        \- memory modelling using a binary tree ADT.
+  \fIbittree\fP     \- memory modelling using a Patricia trie ADT.
+  \fIsplay_tree\fP  \- memory modelling using a splay tree ADT.
+  \fIlist\fP        \- memory modelling using a linked-list ADT.
+  \fItree\fP        \- memory modelling using a binary tree ADT.
 
-By default Patricia trie  memory model is used.
+By default the Patricia trie  memory model is used.
 .TP
 .B -P, --production
-Compile optimized executatle without debug features.
-Note that un-optimized executables may lead to significant
+generate an optimized executable with all debug features disabled.
+Unoptimized executables (default) may lead to a significant
 performance slowdown.
 .TP
 .B -N, --no-stdlib
-If specified the E-ACSL run-time library uses custom
-implementations of standard library functions (such as memset).
-By default GCC builtins are used (e.g., \fB__builtin_memset\fP).
+if specified the \fBE-ACSL\fP runtime library uses custom
+implementations of standard library functions (such as \fBmemset\fP).
+By default \fBGCC\fP builtins are used (e.g., \fB__builtin_memset\fP).
 .TP
 .B -D, --debug-log=\fI<FILE>
-Specify the name of the file for logging of debugging output of
-modified modified executables. If '-' is specified then the
-output is redirected to the \fISTDERR\fP. By default
-\fI/tmp/e-acsl.log\fP file is used. Note that this option is meaningful
-in the absence of the -P flag, which diables debug logging for
+the name of the file for logging of the debugging output of
+modified executables. If '-' is specified then the
+output is redirected to \fISTDERR\fP. By default
+the debug output is redirected to
+\fI/tmp/e-acsl.log\fP. This option is only meaningful
+in the absence of the \fB-P\fP flag that disables debug logging for
 performance reasons.
+.TP
+.B -I, --frama-c=\fI<FILE>
+the name of the \fBFrama-C\fP executable. By default the
+first \fIframa-c\fP executable found in the system path is used.
+.TP
+.B -G, --gcc=\fI<FILE>
+the name of the \fBGCC\fP executable. By default the first \fIgcc\fP
+executable found in the system path is used.
 
 .SH EXIT STATUS
 .TP
@@ -136,27 +154,26 @@ Successful execution
 .B 1
 Invalid user input
 .TP
-.B frama-c or gcc error code
+.B \fBFrama-C\fP or \fBGCC\fP error code
 Instrumentation- or compile-time error
 
 .SH EXAMPLES
 
-Instrument foo.c and output the instrumented code to \fIa.out.frama.c\fP
-
 .B e-acsl-gcc.sh foo.c
 
+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
 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 -P -c -ogen_foo.c -Ofoo foo.c
-
-Assume \fIgen_foo.c\fP has been instrumented by E-ACSL and compile it into
-\fIa.out.e-acsl\fP using \fBsplaytree\fB memory model instead of the default
-one.
+.B e-acsl-gcc.sh --memory-model=splay_tree -C gen_foo.c
 
-.B e-acsl-gcc.sh --memory-model=splaytree -C gen_foo.c
+Assume \fIgen_foo.c\fP has been instrumented by \fBE-ACSL\fP and compile it into
+\fIa.out.e-acsl\fP using \fBsplay_tree\fP memory model.
 
 .SH SEE ALSO
 \fBgcc\fP(1), \fBcpp\fP(1), \fBld\fP(1), \fBframa-c\fP(1)