diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh index a2061517b579317b47f94b3b2e526cec5d2bf9bf..22865148c51ae7db3e170d08c7c395eff3068682 100755 --- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh +++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh @@ -86,10 +86,14 @@ Usage: e-acsl-gcc.sh [options] files Options: -h show this help page -c compile instrumented code + -l pass additional options to the linker + -e pass additional options to the pre-preprocessor + -E pass additional arguments to the Frama-C pre-processor -p output the generated code with rich formatting 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] -M maximise memory-related instrumentation + -g always use GMP integers instead of C integral types -q suppress any output except for errors and warnings -s <file> redirect all output to <file> -P compile executatle without debug features