From b2c0bcf54a7ea6598a177fc006063384eb93577b Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 28 Nov 2019 15:26:31 +0100
Subject: [PATCH] [doc] update command line helpers
---
src/plugins/e-acsl/man/e-acsl-gcc.sh.1 | 11 +++++++++--
src/plugins/e-acsl/scripts/e-acsl-gcc.comp | 14 ++++++++++----
src/plugins/e-acsl/scripts/e-acsl-gcc.sh | 2 ++
3 files changed, 21 insertions(+), 6 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 ed7dc106207..530649ad13d 100644
--- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
+++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
@@ -70,7 +70,7 @@ By default the -\fIdebug\fP flag is unused.
pass a value to the \fBFrama-C\fP -\fIverbose\fP option.
By default the -\fIverbose\fP flag is unused.
.TP
-.B -V, --check
+.B --check
check integrity of the generated AST (mostly useful for developers).
.TP
.B -o, --ocode=\fI<FILE>
@@ -176,6 +176,9 @@ Trigger failure if a NULL-pointer is used as an input to free function
On assertion failure exit with the given integer code intead of raising an abort
signal
.TP
+.B --external-assert
+Set it if you provide your own implementation of e_acsl_assert
+.TP
.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.
@@ -186,13 +189,17 @@ Valid arguments are:
By default the Patricia trie memory model is used.
.TP
-.B --print-models
+.B --print-mmodels
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
first \fIframa-c\fP executable found in the system path is used.
.TP
+.B --e-acsl-share=\fI<DIR>
+the name of the \fBE-ACSL\fP share directory. If not provided, it is computed
+from your setting.
+.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.
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.comp b/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
index 56f49d1a9d4..4e075e196a5 100644
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
@@ -29,14 +29,20 @@ _eacsl_gcc() {
prev="${COMP_WORDS[COMP_CWORD-1]}"
opts="
- -i -C -p -d -o -O -v -f -E -L -M -l -e -g -q -s -F -P -N -D -I -G -X -a
- -h -c -msegment -mbittree
+ -i -C -p -d -o -O -v -V -f -E -L -M -l -e -g -q -s -F -P -N -D -I -G -X -a
+ -h -c -T -k
--verbose= --debug= --debug-log= --logfile= --quiet --rt-debug --help
+ --rt-verbose --check --then --keep-going --fail-with-code --external-assert=
+ --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=
- --compile --compile-only --print --frama-c-only --instrumented-only
- --gmp --full-mmodel --rte --no-int-overflow --no-stdlib --frama-c-stdlib"
+ --e-acsl-extra=
+ --compile --compile-only --print-mmodels --frama-c-only --instrumented-only
+ --gmp --full-mmodel --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"
case ${prev} in
-*)
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index 3baaacb93aa..63cd1360942 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -324,9 +324,11 @@ Usage: e-acsl-gcc.sh [options] files
Options:
-h show this help page
-c compile instrumented code
+ -C assume that the input files have already been instrumented
-l pass additional options to the linker
-e pass additional options to the prepreprocessor
-E pass additional arguments to the Frama-C preprocessor
+ -F pass additional options to the Frama-C command line
-p output the generated code to STDOUT
-o <file> output the generated code to <file> [a.out.frama.c]
-O <file> output the generated executables to <file> [a.out, a.out.e-acsl]
--
GitLab