Skip to content

Add missing EXIT or SIGNAL specifications [blocks: #3618] #4230

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 1 commit into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
CORE
A.class
--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
CORE
A.class
--function 'A.me2:()V' --java-threading
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
CORE
A.class
--function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
CORE
A.class
--function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
CORE
A.class
--function A.me2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
KNOWNBUG
Sync.class
--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
KNOWNBUG
Sync.class
--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
CORE
A.class
--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions --java-threading
^EXIT=0$
^SIGNAL=0$
ATOMIC_BEGIN
ATOMIC_END
--
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
CORE
A.class
--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions
^EXIT=0$
^SIGNAL=0$
ATOMIC_BEGIN
ATOMIC_END
--
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
CORE
A.class
--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions
^EXIT=0$
^SIGNAL=0$
ATOMIC_BEGIN
ATOMIC_END
--
Expand Down
4 changes: 2 additions & 2 deletions jbmc/regression/jbmc-generics/type_erasure/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
TestClass.class
--function TestClass.testFunction --classpath `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
VERIFICATION SUCCESSFUL
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
CORE
TestClass.class
--function TestClass.testFunctionWithInput
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
VERIFICATION SUCCESSFUL
--
--
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@ CORE
RefineStrings.class
--function string_refinement.RefineStrings.constantComparison --show-vcc --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
^EXIT=0$
^SIGNAL=0$
--
.*cprover_string_startswith_func*.
--
Expand Down
4 changes: 2 additions & 2 deletions jbmc/regression/jbmc-strings/stub-string-length/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@ CORE
Test.class
--function Test.main --max-nondet-string-length 10
VERIFICATION SUCCESSFUL
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
4 changes: 2 additions & 2 deletions jbmc/regression/jbmc/JumpSimplification/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@ CORE
Test.class
--show-goto-functions --function Test.foo
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
IF \w* <= 0 THEN GOTO 1\n\s*//.*\n\s*//.*\n\s*\w*::
--
IF !\(\w* <= 0\) THEN GOTO 1\n\s*//.*\n.*GOTO 2\n\s*//.*\n\s*//.*\n\s*1: \w*::
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@ CORE
NondetEnumArg.class
--function NondetEnumArg.canChooseRed --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^VERIFICATION FAILED$
^EXIT=10$
^SIGNAL=0$
--
--
Test 1 of 3 to check that any of the enum constants can be chosen.
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@ CORE
NondetEnumArg.class
--function NondetEnumArg.canChooseGreen --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^VERIFICATION FAILED$
^EXIT=10$
^SIGNAL=0$
--
--
Test 2 of 3 to check that any of the enum constants can be chosen.
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@ CORE
NondetEnumArg.class
--function NondetEnumArg.canChooseBlue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^VERIFICATION FAILED$
^EXIT=10$
^SIGNAL=0$
--
--
Test 3 of 3 to check that any of the enum constants can be chosen.
2 changes: 2 additions & 0 deletions jbmc/regression/jbmc/NondetEnumArgField/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@ CORE
NondetEnumArgField.class
--function NondetEnumArgField.test --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^VERIFICATION FAILED$
^EXIT=10$
^SIGNAL=0$
--
--
The test checks that even when none of the enum constants are referenced in user
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@ CORE
NondetEnumOpaqueReturn.class
--function NondetEnumOpaqueReturn.canChooseRed --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^VERIFICATION FAILED$
^EXIT=10$
^SIGNAL=0$
--
--
Test 1 of 3 to check that any of the enum constants can be chosen.
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@ CORE
NondetEnumOpaqueReturn.class
--function NondetEnumOpaqueReturn.canChooseGreen --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^VERIFICATION FAILED$
^EXIT=10$
^SIGNAL=0$
--
--
Test 2 of 3 to check that any of the enum constants can be chosen.
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@ CORE
NondetEnumOpaqueReturn.class
--function NondetEnumOpaqueReturn.canChooseBlue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^VERIFICATION FAILED$
^EXIT=10$
^SIGNAL=0$
--
--
Test 3 of 3 to check that any of the enum constants can be chosen.
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
CORE
ArrayValueAnnotationOnClass.class
--verbosity 10
^EXIT=6$
^SIGNAL=0$
Getting class `MyClassA' from file \.[\\/]MyClassA\.class
Getting class `MyClassB' from file \.[\\/]MyClassB\.class
--
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
CORE
ArrayValueAnnotationOnField.class
--verbosity 10
^EXIT=6$
^SIGNAL=0$
Getting class `MyClassA' from file \.[\\/]MyClassA\.class
Getting class `MyClassB' from file \.[\\/]MyClassB\.class
--
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
CORE
ArrayValueAnnotationOnMethod.class
--verbosity 10
^EXIT=6$
^SIGNAL=0$
Getting class `MyClassA' from file \.[\\/]MyClassA\.class
Getting class `MyClassB' from file \.[\\/]MyClassB\.class
--
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
CORE
ArrayValueAnnotationOnParameter.class
--verbosity 10
^EXIT=6$
^SIGNAL=0$
Getting class `MyClassA' from file \.[\\/]MyClassA\.class
Getting class `MyClassB' from file \.[\\/]MyClassB\.class
--
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
CORE
ClassValueAnnotationOnClass.class
--verbosity 10
^EXIT=6$
^SIGNAL=0$
Getting class `MyClassA' from file \.[\\/]MyClassA\.class
--
MyClassB
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
CORE
ClassValueAnnotationOnField.class
--verbosity 10
^EXIT=6$
^SIGNAL=0$
Getting class `MyClassA' from file \.[\\/]MyClassA\.class
--
MyClassB
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
CORE
ClassValueAnnotationOnMethod.class
--verbosity 10
^EXIT=6$
^SIGNAL=0$
Getting class `MyClassA' from file \.[\\/]MyClassA\.class
--
MyClassB
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
CORE
ClassValueAnnotationOnParameter.class
--verbosity 10
^EXIT=6$
^SIGNAL=0$
Getting class `MyClassA' from file \.[\\/]MyClassA\.class
--
MyClassB
Expand Down
4 changes: 2 additions & 2 deletions jbmc/regression/jbmc/class_hierarchy/test_json.desc
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,6 @@ CORE symex-driven-lazy-loading-expected-failure
HierarchyTest.class
--show-class-hierarchy --json-ui
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
\{\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 *\},
4 changes: 2 additions & 2 deletions jbmc/regression/jbmc/class_hierarchy/test_plain.desc
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,6 @@ CORE symex-driven-lazy-loading-expected-failure
HierarchyTest.class
--show-class-hierarchy
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
java::HierarchyTest \(abstract\):\n *parents:\n *java::java\.lang\.Object\n *children:\n *java::HierarchyTestChild(1|2)\n *java::HierarchyTestChild(1|2)\njava::HierarchyTestGrandchild:\n *parents:\n *java::HierarchyTestChild1\n *java::HierarchyTestInterface1\n *java::HierarchyTestInterface2\n *children:\njava::HierarchyTestChild2:\n *parents:\n *java::HierarchyTest\n *children:\njava::HierarchyTestChild1:\n *parents:\n *java::HierarchyTest\n *children:\n *java::HierarchyTestGrandchild\njava::HierarchyTestInterface1 \(abstract\):\n *parents:\n *java::java\.lang\.Object\n *children:\n *java::HierarchyTestGrandchild\njava::HierarchyTestInterface2 \(abstract\):\n *parents:\n *java::java\.lang\.Object\n *children:\n *java::HierarchyTestGrandchild
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ KNOWNBUG
Test.class
--classpath src
^EXIT=6$
^SIGNAL=0$
--
Java main class: Test
failed to open input file `Test.class'
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ KNOWNBUG
src/Test.class

^EXIT=6$
^SIGNAL=0$
--
Parsing src/Test.class
--
Expand Down
4 changes: 2 additions & 2 deletions jbmc/regression/jbmc/classpath-jar-entry-method/test.desc
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
CORE
jar_file.jar
--function RelevantClass.entry --verbosity 10
^EXIT=10
^SIGNAL=0
^EXIT=10$
^SIGNAL=0$
VERIFICATION FAILED
Getting class `RelevantClass' from JAR jar_file.jar
Getting class `RelatedClass' from JAR jar_file.jar
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ KNOWNBUG
Test.class
--classpath test.jar
^EXIT=6$
^SIGNAL=0$
--
Java main class: Test
failed to open input file `Test.class'
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ KNOWNBUG
test.jar
--main-class Test.class
^EXIT=6$
^SIGNAL=0$
--
Java main class: Test
failed to open input file `Test.class'
Expand Down
1 change: 1 addition & 0 deletions jbmc/regression/jbmc/classpath-two-classes/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ CORE
Test.class

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
--
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ KNOWNBUG
Test.class
Test2.class
^EXIT=6$
^SIGNAL=0$
--
Invariant check failed
--
Expand Down
1 change: 1 addition & 0 deletions jbmc/regression/jbmc/classpath-two-jars/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ CORE
libs/test.jar
--main-class Test --classpath lib/test2.jar
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
--
Expand Down
1 change: 1 addition & 0 deletions jbmc/regression/jbmc/classpath-two-jars/test2.desc
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ CORE
lib/test2.jar
--main-class Test --classpath libs/test.jar
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
--
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ KNOWNBUG
libs/test.jar
lib/test2.jar --main-class Test.class
^EXIT=6$
^SIGNAL=0$
--
Invariant check failed
the program has no entry point
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ KNOWNBUG
Test.class
--classpath `../../../../scripts/format_classpath.sh libs/test.jar lib/test2.jar`
^EXIT=6$
^SIGNAL=0$
--
--
This is incorrect as it would search for a Test.class file outside the jar files.
Expand Down
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
KNOWNBUG
Test.class
--function Test.test --show-goto-functions
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
ObjectWithNondetInitialize\.cproverNondetInitialize\(\)
--
--
Expand Down
2 changes: 2 additions & 0 deletions jbmc/regression/jbmc/destructors/block.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,8 @@ DestructorStackTests.class
--show-goto-functions --function DestructorStackTests.mainTest --unwind 10
activate-multi-line-match
[0-9]+: dead strings;[\s]*(?P<comment_block>(\/\/ [0-9]+ file DestructorStackTests\.java line 42 function java::DestructorStackTests\.mainTest:\(Z\)V bytecode-index 90)|(\/\/ [0-9]+ no location))[\s]*dead minor1;[\s]*(?P>comment_block)[\s]*dead anonlocal::[0-9a-zA-Z]+;[\s]*(?P>comment_block)[\s]*[0-9]+: END_FUNCTION
^EXIT=0$
^SIGNAL=0$
--
--
Checks for:
Expand Down
Loading