From 3c92b8022ff03a7e6c1709c8243b27ca771d5bb5 Mon Sep 17 00:00:00 2001 From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr> Date: Thu, 4 Feb 2016 19:07:34 +0100 Subject: [PATCH] Improved the documentation of the e-acsl wrapper script --- src/plugins/e-acsl/man/e-acsl-gcc.sh.1 | 119 ++++++++++++++----------- 1 file changed, 68 insertions(+), 51 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 67d45782fcd..22532840035 100644 --- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 +++ b/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) -- GitLab