Commit 9d228c73 authored by Basile Desloges 's avatar Basile Desloges

[eacsl] Update `e-acsl-gcc.sh` doc

parent a07bd940
......@@ -153,7 +153,7 @@ Valid arguments are:
\fIfloat-to-int\fP \- casts from floating-point to integer.
\fIdiv\fP \- division by zero.
\fIshift\fP \- left and right shifts by a value out of bounds.
\fpointer-call\fP \- annotate functions calls through pointers.
\fIpointer-call\fP \- annotate functions calls through pointers.
\fIall\fP \- all of the above.
.TP
.B -A, --rte-select=\fI<OPTSTRING>
......@@ -212,7 +212,39 @@ launch of the \fBE-ACSL\fP plugin.
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
equivalent to \fB--frama-c-extra\fP.
.TP
.B --ar=\fI<FILE>
the name of the \fBAR\fP executable. Only relevant with
\fB--dlmalloc-from-sources\fP. By default the first \fIar\fP executable found in
the system path is used.
.TP
.B --ranlib=\fI<FILE>
the name of the \fBRANLIB\fP executable. Only relevant with
\fB--dlmalloc-from-sources\fP. By default the first \fIranlib\fP executable
found in the system path is used.
.TP
.B --with-dlmalloc=\fI<FILE>
use \fI<FILE>\fP instead of distributed dlmalloc library.
.TP
.B --dlmalloc-from-sources
compile and use dlmalloc library from sources instead of using the distributed
library. Incompatible with \fB--with-dlmalloc\fP.
.TP
.B --dlmalloc-compile-only
do not instrument or compile code, only compile dlmalloc library from sources.
Implies \fB--dlmalloc-from-sources\fP and incompatible with
\fB--with-dlmalloc\fP.
.TP
.B --dlmalloc-compile-flags=\fI<FLAGS>
compile dlmalloc library with \fI<FLAGS>\fP compile flags. Default to
\fI-O2 -g3\fP. Unused if \fB--dlmalloc-from-sources\fP or
\fB--dlmalloc-compile-only\fP isn't used.
.TP
.B --odlmalloc=\fI<FILE>
output compiled dlmalloc library to \fI<FILE>\fP. Unused if
\fB--dlmalloc-from-sources\fP or \fB--dlmalloc-compile-only\fP isn't used.
.SH EXIT STATUS
.TP
.B 0
......
......@@ -36,13 +36,15 @@ _eacsl_gcc() {
--no-trace
--ocode= --oexec= --oexec-e-acsl=
--ld-flags= --cpp-flags= --extra-cpp-args=
--frama-c-extra= --frama-c= --gcc= --e-acsl-share= --memory-model=
--e-acsl-extra=
--frama-c-extra= --frama-c= --gcc= --ar= --ranlib=
--e-acsl-share= --memory-model= --e-acsl-extra=
--compile --compile-only --print-mmodels --frama-c-only --instrumented-only
--gmp --full-mtracking --rte= --rte-select= --no-int-overflow
--no-stdlib --frama-c-stdlib --libc-replacements
--temporal --free-valid-address --weak-validity --validate-format-strings
--heap-size --stack-size"
--heap-size --stack-size
--with-dlmalloc --dlmalloc-from-sources --dlmalloc-compile-only
--dlmalloc-compile-flags --odlmalloc"
case ${prev} in
-*)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment