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

‎jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
CORE
22
A.class
33
--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions --java-threading
4+
^EXIT=0$
5+
^SIGNAL=0$
46
ATOMIC_BEGIN
57
ATOMIC_END
68
--

‎jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
CORE
22
A.class
33
--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions
4+
^EXIT=0$
5+
^SIGNAL=0$
46
ATOMIC_BEGIN
57
ATOMIC_END
68
--

‎jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
CORE
22
A.class
33
--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions
4+
^EXIT=0$
5+
^SIGNAL=0$
46
ATOMIC_BEGIN
57
ATOMIC_END
68
--

‎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-generics/type_erasure/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
TestClass.class
33
--function TestClass.testFunction --classpath `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4-
EXIT=0
5-
SIGNAL=0
4+
^EXIT=0$
5+
^SIGNAL=0$
66
VERIFICATION SUCCESSFUL

‎jbmc/regression/jbmc-generics/type_erasure/test_function_input.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
TestClass.class
33
--function TestClass.testFunctionWithInput
4-
EXIT=0
5-
SIGNAL=0
4+
^EXIT=0$
5+
^SIGNAL=0$
66
VERIFICATION SUCCESSFUL
77
--
88
--

‎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-strings/StartsWithConstantEvalution/constant_equals.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@ CORE
22
RefineStrings.class
33
--function string_refinement.RefineStrings.constantComparison --show-vcc --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
5+
^EXIT=0$
6+
^SIGNAL=0$
57
--
68
.*cprover_string_startswith_func*.
79
--

‎jbmc/regression/jbmc-strings/stub-string-length/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@ CORE
22
Test.class
33
--function Test.main --max-nondet-string-length 10
44
VERIFICATION SUCCESSFUL
5-
EXIT=0
6-
SIGNAL=0
5+
^EXIT=0$
6+
^SIGNAL=0$

‎jbmc/regression/jbmc/JumpSimplification/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@ CORE
22
Test.class
33
--show-goto-functions --function Test.foo
44
activate-multi-line-match
5-
EXIT=0
6-
SIGNAL=0
5+
^EXIT=0$
6+
^SIGNAL=0$
77
IF \w* <= 0 THEN GOTO 1\n\s*//.*\n\s*//.*\n\s*\w*::
88
--
99
IF !\(\w* <= 0\) THEN GOTO 1\n\s*//.*\n.*GOTO 2\n\s*//.*\n\s*//.*\n\s*1: \w*::

‎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/jbmc/NondetEnumArg/test_specific_constant1.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@ CORE
22
NondetEnumArg.class
33
--function NondetEnumArg.canChooseRed --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
57
--
68
--
79
Test 1 of 3 to check that any of the enum constants can be chosen.

‎jbmc/regression/jbmc/NondetEnumArg/test_specific_constant2.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@ CORE
22
NondetEnumArg.class
33
--function NondetEnumArg.canChooseGreen --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
57
--
68
--
79
Test 2 of 3 to check that any of the enum constants can be chosen.

‎jbmc/regression/jbmc/NondetEnumArg/test_specific_constant3.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@ CORE
22
NondetEnumArg.class
33
--function NondetEnumArg.canChooseBlue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
57
--
68
--
79
Test 3 of 3 to check that any of the enum constants can be chosen.

‎jbmc/regression/jbmc/NondetEnumArgField/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@ CORE
22
NondetEnumArgField.class
33
--function NondetEnumArgField.test --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
57
--
68
--
79
The test checks that even when none of the enum constants are referenced in user

‎jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant1.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@ CORE
22
NondetEnumOpaqueReturn.class
33
--function NondetEnumOpaqueReturn.canChooseRed --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
57
--
68
--
79
Test 1 of 3 to check that any of the enum constants can be chosen.

‎jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant2.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@ CORE
22
NondetEnumOpaqueReturn.class
33
--function NondetEnumOpaqueReturn.canChooseGreen --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
57
--
68
--
79
Test 2 of 3 to check that any of the enum constants can be chosen.

‎jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant3.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@ CORE
22
NondetEnumOpaqueReturn.class
33
--function NondetEnumOpaqueReturn.canChooseBlue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
57
--
68
--
79
Test 3 of 3 to check that any of the enum constants can be chosen.

‎jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-class.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
CORE
22
ArrayValueAnnotationOnClass.class
33
--verbosity 10
4+
^EXIT=6$
5+
^SIGNAL=0$
46
Getting class `MyClassA' from file \.[\\/]MyClassA\.class
57
Getting class `MyClassB' from file \.[\\/]MyClassB\.class
68
--

‎jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-field.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
CORE
22
ArrayValueAnnotationOnField.class
33
--verbosity 10
4+
^EXIT=6$
5+
^SIGNAL=0$
46
Getting class `MyClassA' from file \.[\\/]MyClassA\.class
57
Getting class `MyClassB' from file \.[\\/]MyClassB\.class
68
--

‎jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-method.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
CORE
22
ArrayValueAnnotationOnMethod.class
33
--verbosity 10
4+
^EXIT=6$
5+
^SIGNAL=0$
46
Getting class `MyClassA' from file \.[\\/]MyClassA\.class
57
Getting class `MyClassB' from file \.[\\/]MyClassB\.class
68
--

‎jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-parameter.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
CORE
22
ArrayValueAnnotationOnParameter.class
33
--verbosity 10
4+
^EXIT=6$
5+
^SIGNAL=0$
46
Getting class `MyClassA' from file \.[\\/]MyClassA\.class
57
Getting class `MyClassB' from file \.[\\/]MyClassB\.class
68
--

‎jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-class.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
CORE
22
ClassValueAnnotationOnClass.class
33
--verbosity 10
4+
^EXIT=6$
5+
^SIGNAL=0$
46
Getting class `MyClassA' from file \.[\\/]MyClassA\.class
57
--
68
MyClassB

‎jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-field.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
CORE
22
ClassValueAnnotationOnField.class
33
--verbosity 10
4+
^EXIT=6$
5+
^SIGNAL=0$
46
Getting class `MyClassA' from file \.[\\/]MyClassA\.class
57
--
68
MyClassB

‎jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-method.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
CORE
22
ClassValueAnnotationOnMethod.class
33
--verbosity 10
4+
^EXIT=6$
5+
^SIGNAL=0$
46
Getting class `MyClassA' from file \.[\\/]MyClassA\.class
57
--
68
MyClassB

‎jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-parameter.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
CORE
22
ClassValueAnnotationOnParameter.class
33
--verbosity 10
4+
^EXIT=6$
5+
^SIGNAL=0$
46
Getting class `MyClassA' from file \.[\\/]MyClassA\.class
57
--
68
MyClassB

‎jbmc/regression/jbmc/class_hierarchy/test_json.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,6 @@ CORE symex-driven-lazy-loading-expected-failure
22
HierarchyTest.class
33
--show-class-hierarchy --json-ui
44
activate-multi-line-match
5-
EXIT=0
6-
SIGNAL=0
5+
^EXIT=0$
6+
^SIGNAL=0$
77
\{\n *"isAbstract": true,\n *"name": "java::HierarchyTest",\n *"parents": \[\n *"java::java.lang.Object"\n *\],\n *"children": \[\n *"java::HierarchyTestChild(1|2)",\n *"java::HierarchyTestChild(1|2)"\n *\]\n *\},\n *\{\n *"isAbstract": false,\n *"name": "java::HierarchyTestGrandchild",\n *"parents": \[\n *"java::HierarchyTestChild1",\n *"java::HierarchyTestInterface1",\n *"java::HierarchyTestInterface2"\n *\],\n *"children": \[\n *\]\n *\},\n *\{\n *"isAbstract": false,\n *"name": "java::HierarchyTestChild2",\n *"parents": \[\n *"java::HierarchyTest"\n *\],\n *"children": \[\n *\]\n *\},\n *\{\n *"isAbstract": false,\n *"name": "java::HierarchyTestChild1",\n *"parents": \[\n *"java::HierarchyTest"\n *\],\n *"children": \[\n *"java::HierarchyTestGrandchild"\n *\]\n *\},\n *\{\n *"isAbstract": true,\n *"name": "java::HierarchyTestInterface1",\n *"parents": \[\n *"java::java.lang.Object"\n *\],\n *"children": \[\n *"java::HierarchyTestGrandchild"\n *\]\n *\},\n *\{\n *"isAbstract": true,\n *"name": "java::HierarchyTestInterface2",\n *"parents": \[\n *"java::java.lang.Object"\n *\],\n *"children": \[\n *"java::HierarchyTestGrandchild"\n *\]\n *\},

0 commit comments

Comments
 (0)