diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh index 8e7e994fde781262b38947199cc94bf5524b469b..99084b7c7dfbb720fb426de237eb97873325de75 100755 --- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh +++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh @@ -48,7 +48,7 @@ check_tool() { LONGOPTIONS="help,compile,compile-only,print,debug:,ocode:,oexec:,verbose:, \ frama-c-only,extra-cpp-args:,frama-c-stdlib,full-mmodel,gmp,quiet,logfile:, ld-flags:,cpp-flags:,frama-c-extra:,memory-model:,production,no-stdlib, - debug-log:,frama-c:,gcc:" + debug-log:,frama-c:,gcc:,e-acsl-share:" SHORTOPTIONS="h,c,C,p,d:,o:,O:,v:,f,E:,L,M,l:,e:,g,q,s:,F:,m:,P,N,D:I:G:" # Prefix for an error message due to wrong arguments ERROR="ERROR parsing arguments:" @@ -106,6 +106,9 @@ Notes: exit 1 } +# Base dir of this script +BASEDIR=$(readlink -f `dirname $0`) + # See if pygmentize if available for color highlighting and default to plain # cat command otherwise if has_tool 'pygmentize'; then @@ -270,6 +273,13 @@ do OPTION_CC="$1" shift; ;; + # Specify EACAL_SHARE directory (where C runtime library lives) by hand + # rather than compute it + --e-acsl-share) + shift; + OPTION_EACSL_SHARE="$1" + shift; + ;; # A memory model to link against -m|--memory-model) shift; @@ -287,6 +297,11 @@ if [ -z "$1" ]; then error "no input files"; fi +# Check if this is `development' of installed version. +if [ -f "$BASEDIR/../E_ACSL.mli" ]; then + DEVELOPMENT=1 +fi + # Architecture-dependent flags. Since by default Frama-C uses 32-bit # architecture we need to make sure that same architecture is used for # instrumentation and for compilation. @@ -313,9 +328,23 @@ FRAMAC_CPP_EXTRA=" -D$EACSL_MACRO_ID -I$FRAMAC_SHARE/libc $CPPMACHDEP" -EACSL_SHARE="$FRAMAC_SHARE/e-acsl" EACSL_MMODEL="$OPTION_EACSL_MMODEL" +# E-ACSL share directory +# If specified explicitly via the --e-acsl-share option than use that ... +if [ -n "$OPTION_EACSL_SHARE" ]; then + EACSL_SHARE="$OPTION_EACSL_SHARE" +# ... otherwise compute it +else + # Installed version path + if [ -z "$DEVELOPMENT" ]; then + EACSL_SHARE="$BASEDIR/../share/frama-c/e-acsl/" + # Development version path + else + EACSL_SHARE="$BASEDIR/../share/e-acsl" + fi +fi + # Macro that identifies E-ACSL compilation. Passed to Frama-C # and GCC runs but not to the original compilation EACSL_MACRO_ID="__E_ACSL__" @@ -327,6 +356,7 @@ CFLAGS="$OPTION_CFLAGS -Wall \ -Wno-long-long \ -Wno-attributes \ + -Wno-undef \ -Wno-unused \ -Wno-unused-function \ -Wno-unused-result \ @@ -335,12 +365,17 @@ CFLAGS="$OPTION_CFLAGS -Wno-unused-variable \ -Wno-unused-but-set-variable \ -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" + +# Disable extra warning for a clang +if [ "`basename $CC`" = 'clang' ]; then + CFLAGS="-Wno-unknown-warning-option \ + -Wno-extra-semi \ + -Wno-tautological-compare \ + -Wno-gnu-empty-struct \ + -Wno-incompatible-pointer-types-discards-qualifiers" +fi + CPPFLAGS="$OPTION_CPPFLAGS" LDFLAGS="$OPTION_LDFLAGS"