diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in index b878e8d36c0b3f8b514938cf797e27b5e8ce0994..74a0fbf809258e9993139a6ea8b8ca1d123a3111 100644 --- a/src/plugins/e-acsl/Makefile.in +++ b/src/plugins/e-acsl/Makefile.in @@ -3,7 +3,7 @@ # This file is part of the Frama-C's E-ACSL plug-in. # # # # Copyright (C) 2012-2016 # -# CEA (Commissariat à l'énergie atomique et aux énergies # +# CEA (Commissariat à l'énergie atomique et aux énergies # # alternatives) # # # # you can redistribute it and/or modify it under the terms of the GNU # @@ -113,11 +113,11 @@ $(PLUGIN_DIR)/local_config.ml: $(PLUGIN_DIR)/Makefile.in VERSION ifeq (@MAY_RUN_TESTS@,yes) PLUGIN_TESTS_DIRS := reject runtime bts gmp no-main -PLUGIN_TESTS_LIB:=$(PLUGIN_DIR)/tests/print.ml - +PLUGIN_TESTS_LIB := $(PLUGIN_DIR)/tests/print.ml E_ACSL_TESTS: $(PLUGIN_DIR)/tests/test_config -$(PLUGIN_DIR)/tests/ptests_config: \ +E_ACSL_DEFAULT_TESTS: \ + $(PLUGIN_DIR)/tests/test_config \ $(PLUGIN_DIR)/tests/print.cmxs \ $(PLUGIN_DIR)/tests/print.cmo diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh index aeea5a51d0e1e27152219ad4e7686f8b737a6e66..c5e3bb3ad05178a0f9e02e590387bf24e344938f 100755 --- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh +++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh @@ -383,8 +383,8 @@ check_tool "$OPTION_CC" # Frama-C directories FRAMAC="$OPTION_FRAMAC" -FRAMAC_SHARE="`$FRAMAC -print-share-path`" -FRAMAC_PLUGIN="`$FRAMAC -print-plugin-path`" +: ${FRAMAC_SHARE:="`$FRAMAC -print-share-path`"} +: ${FRAMAC_PLUGIN:="`$FRAMAC -print-plugin-path`"} # Check if this is a development or an installed version if [ -f "$BASEDIR/../E_ACSL.mli" ]; then @@ -399,7 +399,9 @@ if [ -f "$BASEDIR/../E_ACSL.mli" ]; then EACSL_SHARE="$DEVELOPMENT/share/e-acsl" # Add the project directory to FRAMAC_PLUGINS, # otherwise Frama-C uses an installed version - FRAMAC_FLAGS="-add-path=$DEVELOPMENT/top -add-path=$DEVELOPMENT $FRAMAC_FLAGS" + if test -f "$DEVELOPMENT/META.frama-c-e_acsl"; then + FRAMAC_FLAGS="-add-path=$DEVELOPMENT/top -add-path=$DEVELOPMENT $FRAMAC_FLAGS"; + fi else # Installed version. FRAMAC_SHARE should not be used here as Frama-C # and E-ACSL may not be installed to the same location diff --git a/src/plugins/e-acsl/scripts/testrun.sh b/src/plugins/e-acsl/scripts/testrun.sh index a0167572cd3e8d9d4933ed0b5a2b81dfc3ba24b6..3158d01f55993e95b4fad7c92741c86b12f19fac 100755 --- a/src/plugins/e-acsl/scripts/testrun.sh +++ b/src/plugins/e-acsl/scripts/testrun.sh @@ -52,8 +52,7 @@ GMP="$3" # Whether to issue an additional run with -e-acsl-gmp-only EXTRA="$4" # Extra e-acsl-gcc.sh flags DEBUG="$5" # Debug option -EACSLGCC="$(dirname $0)/e-acsl-gcc.sh" # E-ACSL wrapper script -MODELS="$($EACSLGCC --print-mmodels)" # Supported memory models +EACSLGCC="$(dirname $0)/e-acsl-gcc.sh $EXTRA" # E-ACSL wrapper script ROOTDIR="`readlink -f $(dirname $0)/../`" # Root directory of the repository TESTDIR="$ROOTDIR/tests/$PREFIX" # Test suite directory @@ -118,8 +117,8 @@ run_test() { local logfile=$LOG.$RUNS.elog # Log file for e-acsl-gcc.sh output local oexec=$OUT.$RUNS.out # Generated executable name local oexeclog=$LOG.$RUNS.rlog # Log for executable output - local model="$1" # Memory model to link against - local extra="$2" # Additional arguments to e-acsl-gcc.sh + local extra="$1" # Additional arguments to e-acsl-gcc.sh + MODELS="$($EACSLGCC $extra --print-mmodels)" # Supported memory models # e-acsl-gcc.sh reports models as space-separated string. Make a # comma-separated one otherwise the following does not work @@ -144,10 +143,10 @@ run_test() { RUNS=$((RUNS+1)) } -run_test $model "$EXTRA" +run_test "" # Run GMP tests if specified if [ -n "$GMP" ]; then - run_test $model "--gmp $EXTRA" + run_test "--gmp" fi exit 0