Skip to content

Commit bb79432

Browse files
tautschnigtautschnig
committed
test.pl: check for EXIT and SIGNAL patterns if -e is set
Using EXIT and SIGNAL patterns avoids spurious test successes despite, e.g., failing an invariant.
1 parent 8e013bc commit bb79432

File tree

35 files changed

+103
-96
lines changed

35 files changed

+103
-96
lines changed

‎jbmc/regression/janalyzer-taint/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/janalyzer/janalyzer
6+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c ../../../src/janalyzer/janalyzer
77

88
tests.log: ../$(CPROVER_DIR)/regression/test.pl
9-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/janalyzer/janalyzer
9+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c ../../../src/janalyzer/janalyzer
1010

1111
show:
1212
@for dir in *; do \

‎jbmc/regression/janalyzer/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/janalyzer/janalyzer
6+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c ../../../src/janalyzer/janalyzer
77

88
tests.log: ../$(CPROVER_DIR)/regression/test.pl
9-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/janalyzer/janalyzer
9+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c ../../../src/janalyzer/janalyzer
1010

1111
show:
1212
@for dir in *; do \

‎jbmc/regression/jbmc-concurrency/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
6+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
77

88
tests.log: ../$(CPROVER_DIR)/regression/test.pl
9-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
9+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
1010

1111
show:
1212
@for dir in *; do \

‎jbmc/regression/jbmc-generics/Makefile

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
7-
@../$(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
6+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
7+
@../$(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
88

99
tests.log: ../$(CPROVER_DIR)/regression/test.pl
10-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
11-
@../$(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
10+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
11+
@../$(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
1212

1313
show:
1414
@for dir in *; do \

‎jbmc/regression/jbmc-inheritance/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
6+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
77

88
tests.log: ../$(CPROVER_DIR)/regression/test.pl
9-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
9+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
1010

1111
show:
1212
@for dir in *; do \

‎jbmc/regression/jbmc-json-ui/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ test:
66
ifeq (, $(shell which jq))
77
echo "JBMC JSON-UI tests skipped (can't find 'jq' in your path)"
88
else
9-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../chain.sh ../../../src/jbmc/jbmc"
9+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../chain.sh ../../../src/jbmc/jbmc"
1010
endif
1111

1212
tests.log: ../$(CPROVER_DIR)/regression/test.pl test

‎jbmc/regression/jbmc-strings/Makefile

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,20 +3,20 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
7-
@../$(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
6+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
7+
@../$(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
88

99
testfuture:
10-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF
11-
@../$(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
10+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF
11+
@../$(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
1212

1313
testall:
14-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK
15-
@../$(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
14+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK
15+
@../$(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
1616

1717
tests.log: ../$(CPROVER_DIR)/regression/test.pl
18-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
19-
@../$(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
18+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
19+
@../$(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
2020

2121
show:
2222
@for dir in *; do \

‎jbmc/regression/jbmc/Makefile

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
7-
@../$(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
6+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
7+
@../$(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
88

99
tests.log: ../$(CPROVER_DIR)/regression/test.pl
10-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
11-
@../$(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
10+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
11+
@../$(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
1212

1313
show:
1414
@for dir in *; do \

‎jbmc/regression/jdiff/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jdiff/jdiff
6+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c ../../../src/jdiff/jdiff
77

88
tests.log: ../$(CPROVER_DIR)/regression/test.pl
9-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jdiff/jdiff
9+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c ../../../src/jdiff/jdiff
1010

1111
show:
1212
@for dir in *; do \

‎jbmc/regression/strings-smoke-tests/Makefile

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,20 +3,20 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
7-
@../$(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
6+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
7+
@../$(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
88

99
testfuture:
10-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF
11-
@../$(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
10+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF
11+
@../$(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
1212

1313
testall:
14-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK
15-
@../$(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
14+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK
15+
@../$(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
1616

1717
tests.log: ../$(CPROVER_DIR)/regression/test.pl
18-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
19-
@../$(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
18+
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
19+
@../$(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
2020

2121
show:
2222
@for dir in *; do \

‎regression/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl")
33
macro(add_test_pl_profile name cmdline flag profile)
44
add_test(
55
NAME "${name}-${profile}"
6-
COMMAND ${test_pl_path} -p -c ${cmdline} ${flag} ${ARGN}
6+
COMMAND ${test_pl_path} -e -p -c ${cmdline} ${flag} ${ARGN}
77
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
88
)
99
set_tests_properties("${name}-${profile}" PROPERTIES

‎regression/ansi-c/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,10 @@ else
1010
endif
1111

1212
test:
13-
@../test.pl -p -c $(exe)
13+
@../test.pl -e -p -c $(exe)
1414

1515
tests.log: ../test.pl
16-
@../test.pl -p -c $(exe)
16+
@../test.pl -e -p -c $(exe)
1717

1818
show:
1919
@for dir in *; do \

‎regression/cbmc-cover/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
default: tests.log
22

33
test:
4-
@../test.pl -p -c ../../../src/cbmc/cbmc
4+
@../test.pl -e -p -c ../../../src/cbmc/cbmc
55

66
tests.log: ../test.pl
7-
@../test.pl -p -c ../../../src/cbmc/cbmc
7+
@../test.pl -e -p -c ../../../src/cbmc/cbmc
88

99
show:
1010
@for dir in *; do \

‎regression/cbmc-cpp/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
default: tests.log
22

33
test:
4-
@../test.pl -p -c ../../../src/cbmc/cbmc
4+
@../test.pl -e -p -c ../../../src/cbmc/cbmc
55

66
tests.log: ../test.pl
7-
@../test.pl -p -c ../../../src/cbmc/cbmc
7+
@../test.pl -e -p -c ../../../src/cbmc/cbmc
88

99
show:
1010
@for dir in *; do \

‎regression/cbmc-library/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
default: tests.log
22

33
test:
4-
@../test.pl -p -c ../../../src/cbmc/cbmc
4+
@../test.pl -e -p -c ../../../src/cbmc/cbmc
55

66
tests.log: ../test.pl
7-
@../test.pl -p -c ../../../src/cbmc/cbmc
7+
@../test.pl -e -p -c ../../../src/cbmc/cbmc
88

99
show:
1010
@for dir in *; do \

‎regression/cbmc/Makefile

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
11
default: test
22

33
test:
4-
@../test.pl -p -c "../../../src/cbmc/cbmc --validate-goto-model" -X smt-backend
4+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model" -X smt-backend
55

66
test-cprover-smt2:
7-
@../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2" -X broken-smt-backend
7+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" -X broken-smt-backend
88

99
test-paths-lifo:
10-
@../test.pl -p -c "../../../src/cbmc/cbmc --paths lifo" -X thorough-paths -X smt-backend
10+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" -X thorough-paths -X smt-backend
1111

1212
tests.log: ../test.pl test
1313

‎regression/contracts/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,10 @@ else
1212
endif
1313

1414
test:
15-
@../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)'
15+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)'
1616

1717
tests.log:
18-
@../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)'
18+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)'
1919

2020
show:
2121
@for dir in *; do \

‎regression/cpp/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,10 @@ else
1010
endif
1111

1212
test:
13-
@../test.pl -p -c $(exe)
13+
@../test.pl -e -p -c $(exe)
1414

1515
tests.log: ../test.pl
16-
@../test.pl -p -c $(exe)
16+
@../test.pl -e -p -c $(exe)
1717

1818
show:
1919
@for dir in *; do \

‎regression/goto-analyzer-taint/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
default: tests.log
22

33
test:
4-
@../test.pl -p -c ../../../src/goto-analyzer/goto-analyzer
4+
@../test.pl -e -p -c ../../../src/goto-analyzer/goto-analyzer
55

66
tests.log: ../test.pl
7-
@../test.pl -p -c ../../../src/goto-analyzer/goto-analyzer
7+
@../test.pl -e -p -c ../../../src/goto-analyzer/goto-analyzer
88

99
show:
1010
@for dir in *; do \

‎regression/goto-analyzer/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
default: tests.log
22

33
test:
4-
@../test.pl -p -c ../../../src/goto-analyzer/goto-analyzer
4+
@../test.pl -e -p -c ../../../src/goto-analyzer/goto-analyzer
55

66
tests.log: ../test.pl
7-
@../test.pl -p -c ../../../src/goto-analyzer/goto-analyzer
7+
@../test.pl -e -p -c ../../../src/goto-analyzer/goto-analyzer
88

99
show:
1010
@for dir in *; do \

‎regression/goto-cc-cbmc/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,10 @@ else
1212
endif
1313

1414
test:
15-
@../test.pl -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)'
15+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)'
1616

1717
tests.log:
18-
@../test.pl -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)'
18+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)'
1919

2020
show:
2121
@for dir in *; do \

‎regression/goto-cc-goto-analyzer/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,11 +12,11 @@ else
1212
endif
1313

1414
test:
15-
@../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-analyzer/goto-analyzer $(is_windows)'
15+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-analyzer/goto-analyzer $(is_windows)'
1616

1717
tests.log:
1818
pwd
19-
@../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-analyzer/goto-analyzer $(is_windows)'
19+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-analyzer/goto-analyzer $(is_windows)'
2020

2121
show:
2222
@for dir in *; do \

‎regression/goto-cl/Makefile

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,16 +5,16 @@ include ../../src/common
55

66
ifeq ($(BUILD_ENV_),MSVC)
77
test:
8-
@../test.pl -p -c ../../../src/goto-cc/goto-cl -X goto-link
8+
@../test.pl -e -p -c ../../../src/goto-cc/goto-cl -X goto-link
99
@cp ../../src/goto-cc/goto-cl.exe ../../src/goto-cc/goto-link.exe
1010
@chmod a+x ../../src/goto-cc/goto-link.exe
11-
@../test.pl -p -c ../../../src/goto-cc/goto-link -I goto-link
11+
@../test.pl -e -p -c ../../../src/goto-cc/goto-link -I goto-link
1212

1313
tests.log: ../test.pl
14-
@../test.pl -p -c ../../../src/goto-cc/goto-cl -X goto-link
14+
@../test.pl -e -p -c ../../../src/goto-cc/goto-cl -X goto-link
1515
@cp ../../src/goto-cc/goto-cl.exe ../../src/goto-cc/goto-link.exe
1616
@chmod a+x ../../src/goto-cc/goto-link.exe
17-
@../test.pl -p -c ../../../src/goto-cc/goto-link -I goto-link
17+
@../test.pl -e -p -c ../../../src/goto-cc/goto-link -I goto-link
1818

1919
else
2020
test:

‎regression/goto-diff/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
default: tests.log
22

33
test:
4-
@../test.pl -p -c ../../../src/goto-diff/goto-diff
4+
@../test.pl -e -p -c ../../../src/goto-diff/goto-diff
55

66
tests.log: ../test.pl
7-
@../test.pl -p -c ../../../src/goto-diff/goto-diff
7+
@../test.pl -e -p -c ../../../src/goto-diff/goto-diff
88

99
show:
1010
@for dir in *; do \

‎regression/goto-gcc/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,11 +11,11 @@ tests.log: ../test.pl
1111
else
1212
test:
1313
-@ln -s goto-cc ../../src/goto-cc/goto-gcc
14-
@../test.pl -p -c ../../../src/goto-cc/goto-gcc
14+
@../test.pl -e -p -c ../../../src/goto-cc/goto-gcc
1515

1616
tests.log: ../test.pl
1717
-@ln -s goto-cc ../../src/goto-cc/goto-gcc
18-
@../test.pl -p -c ../../../src/goto-cc/goto-gcc
18+
@../test.pl -e -p -c ../../../src/goto-cc/goto-gcc
1919

2020
endif
2121

‎regression/goto-harness/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,10 +15,10 @@ else
1515
endif
1616

1717
test:
18-
@../test.pl -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(CBMC_EXE) $(is_windows)"
18+
@../test.pl -e -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(CBMC_EXE) $(is_windows)"
1919

2020
tests.log: ../test.pl
21-
@../test.pl -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(CBMC_EXE) $(is_windows)"
21+
@../test.pl -e -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(CBMC_EXE) $(is_windows)"
2222

2323
show:
2424
@for dir in *; do \

‎regression/goto-instrument-typedef/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,10 @@ else
1212
endif
1313

1414
test:
15-
@../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)'
15+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)'
1616

1717
tests.log:
18-
@../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)'
18+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)'
1919

2020
show:
2121
@for dir in *; do \

0 commit comments

Comments
 (0)