test.pl: check for EXIT and SIGNAL patterns if -e is set

tautschnig · tautschnig · commit bb79432791ea · 2019-02-21T15:04:42.000Z
Using EXIT and SIGNAL patterns avoids spurious test successes despite, e.g.,
failing an invariant.
diff --git a/jbmc/regression/janalyzer-taint/Makefile b/jbmc/regression/janalyzer-taint/Makefile
@@ -3,10 +3,10 @@ default: tests.log
 include ../../src/config.inc
 
 test:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/janalyzer/janalyzer
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c ../../../src/janalyzer/janalyzer
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/janalyzer/janalyzer
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c ../../../src/janalyzer/janalyzer
 
 show:
 	@for dir in *; do \
diff --git a/jbmc/regression/janalyzer/Makefile b/jbmc/regression/janalyzer/Makefile
@@ -3,10 +3,10 @@ default: tests.log
 include ../../src/config.inc
 
 test:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/janalyzer/janalyzer
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c ../../../src/janalyzer/janalyzer
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/janalyzer/janalyzer
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c ../../../src/janalyzer/janalyzer
 
 show:
 	@for dir in *; do \
diff --git a/jbmc/regression/jbmc-concurrency/Makefile b/jbmc/regression/jbmc-concurrency/Makefile
@@ -3,10 +3,10 @@ default: tests.log
 include ../../src/config.inc
 
 test:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
 
 show:
 	@for dir in *; do \
diff --git a/jbmc/regression/jbmc-generics/Makefile b/jbmc/regression/jbmc-generics/Makefile
@@ -3,12 +3,12 @@ default: tests.log
 include ../../src/config.inc
 
 test:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 show:
 	@for dir in *; do \
diff --git a/jbmc/regression/jbmc-inheritance/Makefile b/jbmc/regression/jbmc-inheritance/Makefile
@@ -3,10 +3,10 @@ default: tests.log
 include ../../src/config.inc
 
 test:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
 
 show:
 	@for dir in *; do \
diff --git a/jbmc/regression/jbmc-json-ui/Makefile b/jbmc/regression/jbmc-json-ui/Makefile
@@ -6,7 +6,7 @@ test:
 ifeq (, $(shell which jq))
 	echo "JBMC JSON-UI tests skipped (can't find 'jq' in your path)"
 else
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../chain.sh ../../../src/jbmc/jbmc"
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../chain.sh ../../../src/jbmc/jbmc"
 endif
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl test
diff --git a/jbmc/regression/jbmc-strings/Makefile b/jbmc/regression/jbmc-strings/Makefile
@@ -3,20 +3,20 @@ default: tests.log
 include ../../src/config.inc
 
 test:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 testfuture:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
 
 testall:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 show:
 	@for dir in *; do \
diff --git a/jbmc/regression/jbmc/Makefile b/jbmc/regression/jbmc/Makefile
@@ -3,12 +3,12 @@ default: tests.log
 include ../../src/config.inc
 
 test:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 show:
 	@for dir in *; do \
diff --git a/jbmc/regression/jdiff/Makefile b/jbmc/regression/jdiff/Makefile
@@ -3,10 +3,10 @@ default: tests.log
 include ../../src/config.inc
 
 test:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jdiff/jdiff
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c ../../../src/jdiff/jdiff
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jdiff/jdiff
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c ../../../src/jdiff/jdiff
 
 show:
 	@for dir in *; do \
diff --git a/jbmc/regression/strings-smoke-tests/Makefile b/jbmc/regression/strings-smoke-tests/Makefile
@@ -3,20 +3,20 @@ default: tests.log
 include ../../src/config.inc
 
 test:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 testfuture:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
 
 testall:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 show:
 	@for dir in *; do \
diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt
@@ -3,7 +3,7 @@ set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl")
 macro(add_test_pl_profile name cmdline flag profile)
     add_test(
         NAME "${name}-${profile}"
-        COMMAND ${test_pl_path} -p -c ${cmdline} ${flag} ${ARGN}
+        COMMAND ${test_pl_path} -e -p -c ${cmdline} ${flag} ${ARGN}
         WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
     )
     set_tests_properties("${name}-${profile}" PROPERTIES
diff --git a/regression/ansi-c/Makefile b/regression/ansi-c/Makefile
@@ -10,10 +10,10 @@ else
 endif
 
 test:
-	@../test.pl -p -c $(exe)
+	@../test.pl -e -p -c $(exe)
 
 tests.log: ../test.pl
-	@../test.pl -p -c $(exe)
+	@../test.pl -e -p -c $(exe)
 
 show:
 	@for dir in *; do \
diff --git a/regression/cbmc-cover/Makefile b/regression/cbmc-cover/Makefile
@@ -1,10 +1,10 @@
 default: tests.log
 
 test:
-	@../test.pl -p -c ../../../src/cbmc/cbmc
+	@../test.pl -e -p -c ../../../src/cbmc/cbmc
 
 tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/cbmc/cbmc
+	@../test.pl -e -p -c ../../../src/cbmc/cbmc
 
 show:
 	@for dir in *; do \
diff --git a/regression/cbmc-cpp/Makefile b/regression/cbmc-cpp/Makefile
@@ -1,10 +1,10 @@
 default: tests.log
 
 test:
-	@../test.pl -p -c ../../../src/cbmc/cbmc
+	@../test.pl -e -p -c ../../../src/cbmc/cbmc
 
 tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/cbmc/cbmc
+	@../test.pl -e -p -c ../../../src/cbmc/cbmc
 
 show:
 	@for dir in *; do \
diff --git a/regression/cbmc-library/Makefile b/regression/cbmc-library/Makefile
@@ -1,10 +1,10 @@
 default: tests.log
 
 test:
-	@../test.pl -p -c ../../../src/cbmc/cbmc
+	@../test.pl -e -p -c ../../../src/cbmc/cbmc
 
 tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/cbmc/cbmc
+	@../test.pl -e -p -c ../../../src/cbmc/cbmc
 
 show:
 	@for dir in *; do \
diff --git a/regression/cbmc/Makefile b/regression/cbmc/Makefile
@@ -1,13 +1,13 @@
 default: test
 
 test:
-	@../test.pl -p -c "../../../src/cbmc/cbmc --validate-goto-model" -X smt-backend
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model" -X smt-backend
 
 test-cprover-smt2:
-	@../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2" -X broken-smt-backend
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" -X broken-smt-backend
 
 test-paths-lifo:
-	@../test.pl -p -c "../../../src/cbmc/cbmc --paths lifo" -X thorough-paths -X smt-backend
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" -X thorough-paths -X smt-backend
 
 tests.log: ../test.pl test
 
diff --git a/regression/contracts/Makefile b/regression/contracts/Makefile
@@ -12,10 +12,10 @@ else
 endif
 
 test:
-	@../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)'
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)'
 
 tests.log:
-	@../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)'
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)'
 
 show:
 	@for dir in *; do \
diff --git a/regression/cpp/Makefile b/regression/cpp/Makefile
@@ -10,10 +10,10 @@ else
 endif
 
 test:
-	@../test.pl -p -c $(exe)
+	@../test.pl -e -p -c $(exe)
 
 tests.log: ../test.pl
-	@../test.pl -p -c $(exe)
+	@../test.pl -e -p -c $(exe)
 
 show:
 	@for dir in *; do \
diff --git a/regression/goto-analyzer-taint/Makefile b/regression/goto-analyzer-taint/Makefile
@@ -1,10 +1,10 @@
 default: tests.log
 
 test:
-	@../test.pl -p -c ../../../src/goto-analyzer/goto-analyzer
+	@../test.pl -e -p -c ../../../src/goto-analyzer/goto-analyzer
 
 tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/goto-analyzer/goto-analyzer
+	@../test.pl -e -p -c ../../../src/goto-analyzer/goto-analyzer
 
 show:
 	@for dir in *; do \
diff --git a/regression/goto-analyzer/Makefile b/regression/goto-analyzer/Makefile
@@ -1,10 +1,10 @@
 default: tests.log
 
 test:
-	@../test.pl -p -c ../../../src/goto-analyzer/goto-analyzer
+	@../test.pl -e -p -c ../../../src/goto-analyzer/goto-analyzer
 
 tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/goto-analyzer/goto-analyzer
+	@../test.pl -e -p -c ../../../src/goto-analyzer/goto-analyzer
 
 show:
 	@for dir in *; do \
diff --git a/regression/goto-cc-cbmc/Makefile b/regression/goto-cc-cbmc/Makefile
@@ -12,10 +12,10 @@ else
 endif
 
 test:
-	@../test.pl -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)'
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)'
 
 tests.log:
-	@../test.pl -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)'
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)'
 
 show:
 	@for dir in *; do \
diff --git a/regression/goto-cc-goto-analyzer/Makefile b/regression/goto-cc-goto-analyzer/Makefile
@@ -12,11 +12,11 @@ else
 endif
 
 test:
-	@../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-analyzer/goto-analyzer $(is_windows)'
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-analyzer/goto-analyzer $(is_windows)'
 
 tests.log:
 	pwd
-	@../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-analyzer/goto-analyzer $(is_windows)'
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-analyzer/goto-analyzer $(is_windows)'
 
 show:
 	@for dir in *; do \
diff --git a/regression/goto-cl/Makefile b/regression/goto-cl/Makefile
@@ -5,16 +5,16 @@ include ../../src/common
 
 ifeq ($(BUILD_ENV_),MSVC)
 test:
-	@../test.pl -p -c ../../../src/goto-cc/goto-cl -X goto-link
+	@../test.pl -e -p -c ../../../src/goto-cc/goto-cl -X goto-link
 	@cp ../../src/goto-cc/goto-cl.exe ../../src/goto-cc/goto-link.exe
 	@chmod a+x ../../src/goto-cc/goto-link.exe
-	@../test.pl -p -c ../../../src/goto-cc/goto-link -I goto-link
+	@../test.pl -e -p -c ../../../src/goto-cc/goto-link -I goto-link
 
 tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/goto-cc/goto-cl -X goto-link
+	@../test.pl -e -p -c ../../../src/goto-cc/goto-cl -X goto-link
 	@cp ../../src/goto-cc/goto-cl.exe ../../src/goto-cc/goto-link.exe
 	@chmod a+x ../../src/goto-cc/goto-link.exe
-	@../test.pl -p -c ../../../src/goto-cc/goto-link -I goto-link
+	@../test.pl -e -p -c ../../../src/goto-cc/goto-link -I goto-link
 
 else
 test:
diff --git a/regression/goto-diff/Makefile b/regression/goto-diff/Makefile
@@ -1,10 +1,10 @@
 default: tests.log
 
 test:
-	@../test.pl -p -c ../../../src/goto-diff/goto-diff
+	@../test.pl -e -p -c ../../../src/goto-diff/goto-diff
 
 tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/goto-diff/goto-diff
+	@../test.pl -e -p -c ../../../src/goto-diff/goto-diff
 
 show:
 	@for dir in *; do \
diff --git a/regression/goto-gcc/Makefile b/regression/goto-gcc/Makefile
@@ -11,11 +11,11 @@ tests.log: ../test.pl
 else
 test:
 	-@ln -s goto-cc ../../src/goto-cc/goto-gcc
-	@../test.pl -p -c ../../../src/goto-cc/goto-gcc
+	@../test.pl -e -p -c ../../../src/goto-cc/goto-gcc
 
 tests.log: ../test.pl
 	-@ln -s goto-cc ../../src/goto-cc/goto-gcc
-	@../test.pl -p -c ../../../src/goto-cc/goto-gcc
+	@../test.pl -e -p -c ../../../src/goto-cc/goto-gcc
 
 endif
 
diff --git a/regression/goto-harness/Makefile b/regression/goto-harness/Makefile
@@ -15,10 +15,10 @@ else
 endif
 
 test:
-	@../test.pl -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(CBMC_EXE) $(is_windows)"
+	@../test.pl -e -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(CBMC_EXE) $(is_windows)"
 
 tests.log: ../test.pl
-	@../test.pl -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(CBMC_EXE) $(is_windows)"
+	@../test.pl -e -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(CBMC_EXE) $(is_windows)"
 
 show:
 	@for dir in *; do \
diff --git a/regression/goto-instrument-typedef/Makefile b/regression/goto-instrument-typedef/Makefile
@@ -12,10 +12,10 @@ else
 endif
 
 test:
-	@../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)'
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)'
 
 tests.log:
-	@../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)'
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)'
 
 show:
 	@for dir in *; do \
diff --git a/regression/goto-instrument/Makefile b/regression/goto-instrument/Makefile
diff --git a/regression/invariants/Makefile b/regression/invariants/Makefile
diff --git a/regression/smt2_solver/Makefile b/regression/smt2_solver/Makefile
diff --git a/regression/smt2_strings/Makefile b/regression/smt2_strings/Makefile
diff --git a/regression/strings/Makefile b/regression/strings/Makefile
diff --git a/regression/systemc/Makefile b/regression/systemc/Makefile
diff --git a/regression/test-script/Makefile b/regression/test-script/Makefile
diff --git a/regression/test.pl b/regression/test.pl
