Skip to content
Snippets Groups Projects
Commit d26a2b0c authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl] Remove mention of -P option in wrapper script

The `-P` option does not exist.
parent d85b8701
No related branches found
No related tags found
No related merge requests found
...@@ -269,12 +269,10 @@ instrumentation- or compile-time error ...@@ -269,12 +269,10 @@ instrumentation- or compile-time error
instrument foo.c and output the instrumented code to \fIa.out.frama.c\fP. 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 .B e-acsl-gcc.sh -c -ogen_foo.c -Ofoo foo.c
instrument \fIfoo.c\fP, output the instrumented code to \fIgen_foo.c\fP and 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. 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 --memory-model=bittree -C gen_foo.c .B e-acsl-gcc.sh --memory-model=bittree -C gen_foo.c
......
...@@ -29,7 +29,7 @@ _eacsl_gcc() { ...@@ -29,7 +29,7 @@ _eacsl_gcc() {
prev="${COMP_WORDS[COMP_CWORD-1]}" prev="${COMP_WORDS[COMP_CWORD-1]}"
opts=" opts="
-i -C -d -o -O -v -V -f -E -L -M -l -e -g -q -s -F -P -N -D -I -G -X -a -i -C -d -o -O -v -V -f -E -L -M -l -e -g -q -s -F -N -D -I -G -X -a
-h -c -T -k -h -c -T -k
--verbose= --debug= --debug-log= --logfile= --quiet --rt-debug --help --verbose= --debug= --debug-log= --logfile= --quiet --rt-debug --help
--rt-verbose --check --then --keep-going --fail-with-code --external-assert= --rt-verbose --check --then --keep-going --fail-with-code --external-assert=
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment