Merge branch 'feature/virgile/fix-tests-env' into 'master'

Feature/virgile/fix tests env

Seems to fix testing issues when running in internal mode

See merge request !68

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
 

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

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