[doc] update command line helpers

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.

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
     -*)

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]