Skip to content

Commit e3ed7a5

Browse files
tautschnigtautschnig
authored
Merge pull request #3618 from tautschnig/exit-signal-mandatory
Make EXIT and SIGNAL patterns a requirement in test specifications
2 parents 28f61dc + bb79432 commit e3ed7a5

File tree

211 files changed

+435
-312
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

211 files changed

+435
-312
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-concurrency/anonymous-java.lang.thread/test2.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
CORE
22
A.class
33
--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=10$
45
^SIGNAL=0$
56
^VERIFICATION FAILED$

‎jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
CORE
22
A.class
33
--function 'A.me2:()V' --java-threading
4+
^EXIT=10$
45
^SIGNAL=0$
56
^VERIFICATION FAILED

‎jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
CORE
22
A.class
33
--function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
4+
^EXIT=10$
45
^SIGNAL=0$
56
^VERIFICATION FAILED

‎jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
CORE
22
A.class
33
--function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
4+
^EXIT=10$
45
^SIGNAL=0$
56
^VERIFICATION FAILED$

‎jbmc/regression/jbmc-concurrency/several-threads/test2.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
CORE
22
A.class
33
--function A.me2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
4+
^EXIT=10$
45
^SIGNAL=0$
56
^VERIFICATION FAILED$

‎jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
KNOWNBUG
22
Sync.class
33
--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
4+
^EXIT=0$
5+
^SIGNAL=0$
46
^VERIFICATION SUCCESSFUL$
57
--
68
^warning: ignoring

‎jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
KNOWNBUG
22
Sync.class
33
--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
4+
^EXIT=0$
5+
^SIGNAL=0$
46
^VERIFICATION SUCCESSFUL$
57
--
68
^warning: ignoring

0 commit comments

Comments
 (0)