From 9d228c73f84a8c24b274bf6f731bec00317c6d20 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 14 Oct 2020 16:15:25 +0200
Subject: [PATCH] [eacsl] Update `e-acsl-gcc.sh` doc
---
src/plugins/e-acsl/man/e-acsl-gcc.sh.1 | 36 ++++++++++++++++++++--
src/plugins/e-acsl/scripts/e-acsl-gcc.comp | 8 +++--
2 files changed, 39 insertions(+), 5 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 39e15364d47..e3bc300bdb9 100644
--- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
+++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
@@ -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
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.comp b/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
index b05f8fe127e..2195d4cca8d 100644
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
@@ -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
-*)
--
GitLab