Skip to content
Snippets Groups Projects
Commit 1cf7002d authored by Virgile Prevosto's avatar Virgile Prevosto Committed by Kostyantyn Vorobyov
Browse files

[scripts] always use EXTRA args for running e-acsl-gcc.sh in runtest

parent 42f26ab9
No related branches found
No related tags found
No related merge requests found
......@@ -52,7 +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
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
......@@ -143,10 +143,10 @@ run_test() {
RUNS=$((RUNS+1))
}
run_test "$EXTRA"
run_test ""
# Run GMP tests if specified
if [ -n "$GMP" ]; then
run_test "--gmp $EXTRA"
run_test "--gmp"
fi
exit 0
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment