diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh index 44a913ff6c1c275061185102e740bcb87a9bf430..f1b8bee53f38e1b9f61c94befbe33df772a028a7 100755 --- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh +++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh @@ -98,7 +98,7 @@ Options: -s <file> redirect all output to <file> -P compile executable without debug features -I <file> specify Frama-C executable [frama-c] - -G <file> specify GCC executable [gcc] + -G <file> specify C compiler executable [gcc] Notes: This help page shows only basic options. @@ -335,7 +335,13 @@ CFLAGS="$OPTION_CFLAGS -Wno-unused-function \ -Wno-unused-variable \ -Wno-unused-but-set-variable \ - -Wno-implicit-function-declaration" + -Wno-implicit-function-declaration \ + -Wno-unknown-warning-option \ + -Wno-extra-semi \ + -Wno-tautological-compare \ + -Wno-gnu-empty-struct \ + -Wno-incompatible-pointer-types-discards-qualifiers \ + -Wno-empty-body" CPPFLAGS="$OPTION_CPPFLAGS" LDFLAGS="$OPTION_LDFLAGS"