replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Add missing EXIT or SIGNAL specifications 

We should always check for these to avoid spuriously passing tests.
This commit is contained in:
Michael Tautschnig 2018-12-21 14:21:03 +00:00
parent 28f61dc2db
commit 8e013bc3f2
176 changed files with 332 additions and 216 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc
View File

@ -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$

1
jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc
View File

@ -1,5 +1,6 @@
CORE
A.class
--function 'A.me2:()V' --java-threading
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED

1
jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc
View File

@ -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

1
jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc
View File

@ -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$

1
jbmc/regression/jbmc-concurrency/several-threads/test2.desc
View File

@ -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$

2
jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc
View File

@ -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

2
jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc
View File

@ -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

2
jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc
View File

@ -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
--

2
jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc
View File

@ -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
--

2
jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc
View File

@ -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
--

4
jbmc/regression/jbmc-generics/type_erasure/test.desc
View File

@ -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

4
jbmc/regression/jbmc-generics/type_erasure/test_function_input.desc
View File

@ -1,8 +1,8 @@
CORE
TestClass.class
--function TestClass.testFunctionWithInput
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
VERIFICATION SUCCESSFUL
--
--

2
jbmc/regression/jbmc-strings/StartsWithConstantEvalution/constant_equals.desc
View File

@ -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*.
--

4
jbmc/regression/jbmc-strings/stub-string-length/test.desc
View File

@ -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
jbmc/regression/jbmc/JumpSimplification/test.desc
View File

@ -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*::

2
jbmc/regression/jbmc/NondetEnumArg/test_specific_constant1.desc
View File

@ -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.

2
jbmc/regression/jbmc/NondetEnumArg/test_specific_constant2.desc
View File

@ -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.

2
jbmc/regression/jbmc/NondetEnumArg/test_specific_constant3.desc
View File

@ -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
jbmc/regression/jbmc/NondetEnumArgField/test.desc
View File

@ -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

2
jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant1.desc
View File

@ -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.

2
jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant2.desc
View File

@ -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.

2
jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant3.desc
View File

@ -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.

2
jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-class.desc
View File

@ -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
--

2
jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-field.desc
View File

@ -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
--

2
jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-method.desc
View File

@ -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
--

2
jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-parameter.desc
View File

@ -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
--

2
jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-class.desc
View File

@ -1,6 +1,8 @@
CORE
ClassValueAnnotationOnClass.class
--verbosity 10
^EXIT=6$
^SIGNAL=0$
Getting class `MyClassA' from file \.[\\/]MyClassA\.class
--
MyClassB

2
jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-field.desc
View File

@ -1,6 +1,8 @@
CORE
ClassValueAnnotationOnField.class
--verbosity 10
^EXIT=6$
^SIGNAL=0$
Getting class `MyClassA' from file \.[\\/]MyClassA\.class
--
MyClassB

2
jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-method.desc
View File

@ -1,6 +1,8 @@
CORE
ClassValueAnnotationOnMethod.class
--verbosity 10
^EXIT=6$
^SIGNAL=0$
Getting class `MyClassA' from file \.[\\/]MyClassA\.class
--
MyClassB

2
jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-parameter.desc
View File

@ -1,6 +1,8 @@
CORE
ClassValueAnnotationOnParameter.class
--verbosity 10
^EXIT=6$
^SIGNAL=0$
Getting class `MyClassA' from file \.[\\/]MyClassA\.class
--
MyClassB

4
jbmc/regression/jbmc/class_hierarchy/test_json.desc
View File

@ -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
jbmc/regression/jbmc/class_hierarchy/test_plain.desc
View File

@ -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

1
jbmc/regression/jbmc/classpath-class-incorrect-package/test.desc
View File

@ -2,6 +2,7 @@ KNOWNBUG
Test.class
--classpath src
^EXIT=6$
^SIGNAL=0$
--
Java main class: Test
failed to open input file `Test.class'

1
jbmc/regression/jbmc/classpath-class-with-one-dir/test_prefix.desc
View File

@ -2,6 +2,7 @@ KNOWNBUG
src/Test.class
^EXIT=6$
^SIGNAL=0$
--
Parsing src/Test.class
--

4
jbmc/regression/jbmc/classpath-jar-entry-method/test.desc
View File

@ -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

1
jbmc/regression/jbmc/classpath-jar-incorrect-package/test_class.desc
View File

@ -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'

1
jbmc/regression/jbmc/classpath-jar-incorrect-package/test_jar_main_class.desc
View File

@ -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'

1
jbmc/regression/jbmc/classpath-two-classes/test.desc
View File

@ -2,6 +2,7 @@ CORE
Test.class
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
--

1
jbmc/regression/jbmc/classpath-two-classes/test_incorrect.desc
View File

@ -2,6 +2,7 @@ KNOWNBUG
Test.class
Test2.class
^EXIT=6$
^SIGNAL=0$
--
Invariant check failed
--

1
jbmc/regression/jbmc/classpath-two-jars/test.desc
View File

@ -2,6 +2,7 @@ CORE
libs/test.jar
--main-class Test --classpath lib/test2.jar
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
--

1
jbmc/regression/jbmc/classpath-two-jars/test2.desc
View File

@ -2,6 +2,7 @@ CORE
lib/test2.jar
--main-class Test --classpath libs/test.jar
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
--

1
jbmc/regression/jbmc/classpath-two-jars/test_incorrect.desc
View File

@ -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

1
jbmc/regression/jbmc/classpath-two-jars/test_incorrect2.desc
View File

@ -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.

4
jbmc/regression/jbmc/cprover-always-load-nondet-initialize/test.desc
View File

@ -1,8 +1,8 @@
KNOWNBUG
Test.class
--function Test.test --show-goto-functions
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
ObjectWithNondetInitialize\.cproverNondetInitialize\(\)
--
--

2
jbmc/regression/jbmc/destructors/block.desc
View File

@ -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:

2
jbmc/regression/jbmc/destructors/break.desc
View File

@ -3,6 +3,8 @@ DestructorStackTests.class
--show-goto-functions --function DestructorStackTests.mainTest --unwind 10
activate-multi-line-match
(?P<comment_block>\/\/ [0-9]+ file DestructorStackTests\.java line 34 function java::DestructorStackTests\.mainTest:\(Z\)V bytecode-index 84)[\s]*dead throwaway;[\s]*(?P>comment_block)[\s]*dead new_tmp[0-9]+;[\s]*(?P>comment_block)[\s]*dead val;[\s]*(?P>comment_block)[\s]*GOTO [0-9]+
^EXIT=0$
^SIGNAL=0$
--
--
Checks for:

2
jbmc/regression/jbmc/destructors/continue.desc
View File

@ -3,6 +3,8 @@ DestructorStackTests.class
--show-goto-functions --function DestructorStackTests.mainTest --unwind 10
activate-multi-line-match
(?P<comment_block>\/\/ [0-9]+ file DestructorStackTests\.java line 39 function java::DestructorStackTests\.mainTest:\(Z\)V bytecode-index 89)[\s]*dead throwaway;[\s]*(?P>comment_block)[\s]*dead new_tmp[0-9]+;[\s]*(?P>comment_block)[\s]*dead val;[\s]*(?P>comment_block)[\s]*GOTO [0-9]+
^EXIT=0$
^SIGNAL=0$
--
--
Checks for:

4
jbmc/regression/jbmc/destructors/decl.desc
View File

@ -3,6 +3,8 @@ DestructorStackTests.class
--show-goto-functions --function DestructorStackTests.mainTest --unwind 10
activate-multi-line-match
IF !\(\(int\)unknown == 0\) THEN GOTO [0-9]+[\s]*(?P<comment_block>\/\/ [0-9]+ file DestructorStackTests\.java line 24 function java::DestructorStackTests\.mainTest:\(Z\)V bytecode-index 50)[\s]*dead new_tmp[0-9]+;[\s]*(?P>comment_block)[\s]*GOTO [0-9]+[\s]*\/\/ [0-9]+ no location[\s]*[0-9]+: dead new_tmp[0-9]+;[\s]*
^EXIT=0$
^SIGNAL=0$
--
--
Checks for:
@ -16,4 +18,4 @@ Checks for:
1: dead new_tmp0;
Tests to make sure a declaration kills its temp variable before continuing.
Numbers vary between symex load / normal load.
Numbers vary between symex load / normal load.

2
jbmc/regression/jbmc/destructors/return.desc
View File

@ -3,6 +3,8 @@ DestructorStackTests.class
--show-goto-functions --function DestructorStackTests.mainTest --unwind 10
activate-multi-line-match
(?<comment_block>\/\/ [0-9]+ file DestructorStackTests\.java line 18 function java::DestructorStackTests.mainTest:\(Z\)V bytecode-index 40)[\s]*dead minor[0-9]+;[\s]*(?P>comment_block)[\s]*dead new_tmp[0-9]+;[\s]*(?P>comment_block)[\s]*dead anonlocal::[0-9a-zA-Z]+;[\s]*(?P>comment_block)[\s]*dead new_tmp[0-9]+;[\s]*(?P>comment_block)[\s]*dead ex;[\s]*(?P>comment_block)[\s]*dead minor2;[\s]*(?P>comment_block)[\s]*dead minor1;[\s]*(?P>comment_block)[\s]*dead anonlocal::[0-9a-zA-Z]+;[\s]*(?P>comment_block)[\s]*GOTO [0-9]+
^EXIT=0$
^SIGNAL=0$
--
--
Checks for:

4
jbmc/regression/jbmc/internal1/test.desc
View File

@ -2,8 +2,8 @@ CORE
com/diffblue/javatest/nestedobjects/subpackage/Order.class
--json-ui --function 'com.diffblue.javatest.nestedobjects.subpackage.Order.setItem:(Lcom/diffblue/javatest/nestedobjects/subpackage/Item;)Z' --trace
activate-multi-line-match
EXIT=10
SIGNAL=0
^EXIT=10$
^SIGNAL=0$
"identifier": "__CPROVER_initialize",\n *"sourceLocation": [{][}]\n *[}],\n *"hidden": false,\n *"internal": true,\n *"stepType": "function-call",
"internal": true,\n *"lhs": "tmp_object_factory[$][0-9]+",
"internal": false,\n *"sourceLocation": [{]\n *"file": "com/diffblue/javatest/nestedobjects/subpackage/Order.java",\n *"function": "java::com.diffblue.javatest.nestedobjects.subpackage.Order.setItem:[(]Lcom/diffblue/javatest/nestedobjects/subpackage/Item;[)]Z",\n *"line": "21"\n *[}],\n *"stepType": "function-call",

4
jbmc/regression/jbmc/json_trace3/test.desc
View File

@ -2,8 +2,8 @@ CORE
Test.class
--trace --json-ui --unwind 5 --function Test.main
activate-multi-line-match
EXIT=10
SIGNAL=0
^EXIT=10$
^SIGNAL=0$
"lhs": "dynamic_object3\[1L?\]",\n *"mode": "java",\n *"sourceLocation": \{\n *"bytecodeIndex": "18",\n *"file": "Test\.java",\n *"function": "java::Test\.main:\(\[J\)V",\n *"line": "8"\n *\},\n *"stepType": "assignment",\n *"thread": 0,\n *"value": \{\n *"binary": "0000000000000000000000000000000000000000000000000000000000000001",\n *"data": "1L",\n *"name": "integer",\n *"type": "long",\n *"width": 64
--
"name": "unknown"

4
jbmc/regression/jbmc/lambda2/test.desc
View File

@ -2,8 +2,8 @@ KNOWNBUG
SymStream.class
--show-goto-functions
lambda function reference org/symphonyoss/symphony/clients/model/SymUser\.toSymUser in class \"SymStream\"
^EXIT=0
^SIGNAL=0
^EXIT=0$
^SIGNAL=0$
--
--
lambda functions without "lambda$" prefix aren't recognized currently TG-2691

4
jbmc/regression/jbmc/lambda2/test_no_crash.desc
View File

@ -1,8 +1,8 @@
CORE symex-driven-lazy-loading-expected-failure
SymStream.class
--no-lazy-methods --show-goto-functions
^EXIT=0
^SIGNAL=0
^EXIT=0$
^SIGNAL=0$
--
--
just to test that it doesn't crash in this situation, cf. TG-2684

5
jbmc/regression/jbmc/lambda2/test_no_crash_ecj.desc
View File

@ -2,9 +2,8 @@ CORE
StaticMethodRef.class
--function StaticMethodRef.Smr
VERIFICATION FAILED
EXIT=10
SIGNAL=0
^SIGNAL=0
^EXIT=10$
^SIGNAL=0$
--
--
Tests that it doesn't crash when failing to read a `BootstrapMethods` entry and

1
jbmc/regression/jbmc/lazyloading10/test.desc
View File

@ -1,6 +1,7 @@
CORE symex-driven-lazy-loading-expected-failure
test.class
--verbosity 10 --function test.f --lazy-methods-extra-entry-point test.sety
^EXIT=0$
^SIGNAL=0$
CI lazy methods: elaborate java::test\.sety:\(I\)V
CI lazy methods: elaborate java::test\.sety:\(F\)V

2
jbmc/regression/jbmc/lazyloading_opaquereturn/test.desc
View File

@ -1,6 +1,8 @@
CORE symex-driven-lazy-loading-expected-failure
TestClass.class
--function TestClass.testFunction --verbosity 10
^EXIT=10$
^SIGNAL=0$
CI lazy methods: elaborate java::Foo\.cproverNondetInitialize:\(\)V
CI lazy methods: elaborate java::Bar\.cproverNondetInitialize:\(\)V
CI lazy methods: elaborate java::Baz\.cproverNondetInitialize:\(\)V

2
jbmc/regression/jbmc/reachability-slice/test.desc
View File

@ -1,6 +1,8 @@
CORE symex-driven-lazy-loading-expected-failure
A.class
--reachability-slice --function A.foo --show-goto-functions --property 'java::A.foo:(I)V.assertion.1'
^EXIT=0$
^SIGNAL=0$
= \(int\)\(short\)1001
= \(int\)\(short\)1002
= \(int\)\(short\)1003

2
jbmc/regression/jbmc/reachability-slice/test2.desc
View File

@ -1,6 +1,8 @@
CORE symex-driven-lazy-loading-expected-failure
A.class
--reachability-slice --function A.foo --show-goto-functions --property 'java::A.foo:(I)V.assertion.2'
^EXIT=0$
^SIGNAL=0$
= \(int\)\(short\)1001
= \(int\)\(short\)1004
--

2
jbmc/regression/jbmc/reachability-slice/test3.desc
View File

@ -1,6 +1,8 @@
CORE symex-driven-lazy-loading-expected-failure
A.class
--reachability-slice --function A.foo --show-goto-functions
^EXIT=0$
^SIGNAL=0$
= \(int\)\(short\)1001
= \(int\)\(short\)1002
= \(int\)\(short\)1003

2
jbmc/regression/jbmc/swap1/test.desc
View File

@ -1,7 +1,7 @@
CORE
Swap.class
^EXIT=0
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--

2
jbmc/regression/jbmc/swap2/test.desc
View File

@ -1,7 +1,7 @@
CORE
org/springframework/build/gradle/MergePlugin$1$_execute_closure1$_closure2.class
--function 'org.springframework.build.gradle.MergePlugin$1$_execute_closure1$_closure2.$getCallSiteArray:()[Lorg/codehaus/groovy/runtime/callsite/CallSite;'
^EXIT=0
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--

2
jbmc/regression/jbmc/temp_stack_variable_packing/test.desc
View File

@ -1,6 +1,8 @@
CORE
Primary.class
--function Primary.main
^EXIT=10$
^SIGNAL=0$
^\[java::Primary.Run:\(\)V\.assertion\.1\] line 6 assertion at file Primary\.java line 6 function java::Primary.Run:\(\)V bytecode-index 22: FAILURE$
^VERIFICATION FAILED$
--

4
jbmc/regression/jdiff/java-add-package/test.desc
View File

@ -3,8 +3,8 @@ new.jar
old.jar --json-ui
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
"deletedFunctions": \[\n \{\n "name": "java::Test\.<init>:\(\)V",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.<init>:\(\)\V",\n "line": "1"\n \}\n \},\n \{\n "name": "java::Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(I\)I",\n "line": "4"\n \}\n \},\n \{\n "name": "java::Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test.bar:\(I\)I",\n "line": "12"\n \}\n \}\n \],\n
"modifiedFunctions": \[ \],
"newFunctions": \[\n \{\n "name": "java::foo\.Test\.<init>:\(\)V",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.<init>:\(\)V",\n "line": "3"\n \}\n \},\n \{\n "name": "java::foo\.Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.foo:\(I\)I",\n "line": "5"\n \}\n \},\n \{\n "name": "java::foo\.Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.bar:\(I\)I",\n "line": "14"\n \}\n \}\n \],

4
jbmc/regression/jdiff/java-clinit-wrapper/test.desc
View File

@ -1,8 +1,8 @@
CORE
new.jar
old.jar
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
--
java::java\.nio\.charset\.StandardCharsets::clinit_wrapper$
java::org\.apache\.tika\.mime\.MediaType::clinit_wrapper$

4
jbmc/regression/jdiff/java-del-package/test.desc
View File

@ -3,8 +3,8 @@ new.jar
old.jar --json-ui
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
"deletedFunctions": \[\n \{\n "name": "java::foo\.Test\.<init>:\(\)V",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.<init>:\(\)V",\n "line": "3"\n \}\n \},\n \{\n "name": "java::foo\.Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.foo:\(I\)I",\n "line": "5"\n \}\n \},\n \{\n "name": "java::foo\.Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.bar:\(I\)I",\n "line": "14"\n \}\n \}\n \],
"modifiedFunctions": \[ \],
"newFunctions": \[\n \{\n "name": "java::Test\.<init>:\(\)V",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.<init>:\(\)\V",\n "line": "1"\n \}\n \},\n \{\n "name": "java::Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(I\)I",\n "line": "4"\n \}\n \},\n \{\n "name": "java::Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test.bar:\(I\)I",\n "line": "12"\n \}\n \}\n \],\n

4
jbmc/regression/jdiff/java-deleted-function/test.desc
View File

@ -3,8 +3,8 @@ new.jar
old.jar --json-ui
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
"deletedFunctions": \[\n \{\n "name": "java::Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(I\)I",\n "line": "4"\n \}\n \}\n \],
"modifiedFunctions": \[ \],
"newFunctions": \[ \],

4
jbmc/regression/jdiff/java-instanceof/test.desc
View File

@ -3,8 +3,8 @@ new.jar
old.jar
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
new functions:\nmodified functions:\ndeleted functions:
--
^warning: ignoring

4
jbmc/regression/jdiff/java-mod-comment/test.desc
View File

@ -3,8 +3,8 @@ new.jar
old.jar --json-ui
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
"deletedFunctions": \[ \],
"modifiedFunctions": \[ \],
"newFunctions": \[ \],

4
jbmc/regression/jdiff/java-mod-identifier/test.desc
View File

@ -3,8 +3,8 @@ new.jar
old.jar --json-ui
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
"deletedFunctions": \[ \],
"modifiedFunctions": \[ \],
"newFunctions": \[ \],

4
jbmc/regression/jdiff/java-mod-identifier2/test.desc
View File

@ -3,8 +3,8 @@ new.jar
old.jar --json-ui
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
"deletedFunctions": \[ \],
"modifiedFunctions": \[\n \{\n "name": "java::Test\.foo:\(II\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(II\)I",\n "line": "4"\n \}\n \}\n \],\n
"newFunctions": \[ \],

4
jbmc/regression/jdiff/java-mod-package/test.desc
View File

@ -3,8 +3,8 @@ new.jar
old.jar --json-ui
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
"deletedFunctions": \[\n \{\n "name": "java::foo\.Test\.<init>:\(\)V",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.<init>:\(\)V",\n "line": "3"\n \}\n \},\n \{\n "name": "java::foo\.Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.foo:\(I\)I",\n "line": "5"\n \}\n \},\n \{\n "name": "java::foo\.Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.bar:\(I\)I",\n "line": "14"\n \}\n \}\n \],
"modifiedFunctions": \[ \],
"newFunctions": \[\n \{\n "name": "java::com\.diffblue\.foo\.Test\.<init>:\(\)V",\n "sourceLocation": \{\n "file": "com/diffblue/foo/Test\.java",\n "function": "java::com\.diffblue\.foo\.Test\.<init>:\(\)\V",\n "line": "3"\n \}\n \},\n \{\n "name": "java::com\.diffblue\.foo\.Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "com/diffblue/foo/Test\.java",\n "function": "java::com\.diffblue\.foo\.Test\.foo:\(I\)I",\n "line": "6"\n \}\n \},\n \{\n "name": "java::com\.diffblue\.foo\.Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "com/diffblue/foo/Test\.java",\n "function": "java::com\.diffblue\.foo\.Test.bar:\(I\)I",\n "line": "14"\n \}\n \}\n \],\n

4
jbmc/regression/jdiff/java-new-function/test.desc
View File

@ -3,8 +3,8 @@ new.jar
old.jar --json-ui
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
"deletedFunctions": \[ \],
"modifiedFunctions": \[ \],
"newFunctions": \[\n \{\n "name": "java::Test\.foo:\(II\)I",\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test\.foo:\(II\)I",\n "line": "4"\n \}\n \}\n \],

4
jbmc/regression/jdiff/java-no-change/test.desc
View File

@ -3,8 +3,8 @@ new.jar
old.jar --json-ui
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
"deletedFunctions": \[ \],
"modifiedFunctions": \[ \],
"newFunctions": \[ \],

4
jbmc/regression/jdiff/java-properties/test.desc
View File

@ -3,8 +3,8 @@ new.jar
old.jar --json-ui --show-properties --cover location
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
"deletedFunctions": \[\n \{\n "name": "java::Test.obsolete:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "18",\n "description": "block 1 \(lines Test.java:java::Test.obsolete:\(\)V:18\)",\n "expression": "false",\n "name": "java::Test.obsolete:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "0",\n "file": "Test.java",\n "function": "java::Test.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "modifiedFunctions": \[\n \{\n "name": "java::Test.<init>:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "6",\n "description": "block 2 \(lines Test.java:java::Test.<init>:\(\)V:6\)",\n "expression": "false",\n "name": "java::Test.<init>:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "1",\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "6"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 3 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n "expression": "false",\n "name": "java::Test.<init>:\(\)V.coverage.2",\n "sourceLocation": \{\n "bytecodeIndex": "3",\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 4 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n "expression": "false",\n "name": "java::Test.<init>:\(\)V.coverage.3",\n "sourceLocation": \{\n "bytecodeIndex": "5",\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 5 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n "expression": "false",\n "name": "java::Test.<init>:\(\)V.coverage.4",\n "sourceLocation": \{\n "bytecodeIndex": "6",\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "7",\n "description": "block 6 \(lines Test.java:java::Test.<init>:\(\)V:7\)",\n "expression": "false",\n "name": "java::Test.<init>:\(\)V.coverage.5",\n "sourceLocation": \{\n "bytecodeIndex": "7",\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "7"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "6"\n }\n },\n \{\n "name": "java::Test.<clinit>:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "3",\n "description": "block 1 \(lines Test.java:java::Test.<clinit>:\(\)V:3\)",\n "expression": "false",\n "name": "java::Test.<clinit>:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "1",\n "file": "Test.java",\n "function": "java::Test.<clinit>:\(\)V",\n "line": "3"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.<clinit>:\(\)V",\n "line": "3"\n }\n }\n ],\n "newFunctions": \[\n \{\n "name": "java::Test.newfun:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "18",\n "description": "block 1 \(lines Test.java:java::Test.newfun:\(\)V:18\)",\n "expression": "false",\n "name": "java::Test.newfun:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "0",\n "file": "Test.java",\n "function": "java::Test.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n
--
^warning: ignoring

4
jbmc/regression/jdiff/java-scope-change/test.desc
View File

@ -3,8 +3,8 @@ new.jar
old.jar --json-ui
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
"deletedFunctions": \[ \],\n "modifiedFunctions": \[\n \{\n "name": "java::Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(I\)I",\n "line": "4"\n \}\n \},\n \{\n "name": "java::Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.bar:\(I\)I",\n "line": "12"\n \}\n \}\n \],\n "newFunctions": \[ \],
--
^warning: ignoring

4
jbmc/regression/jdiff/java-scope-change2/test.desc
View File

@ -3,8 +3,8 @@ new.jar
old.jar --json-ui
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
"deletedFunctions": \[ \],\n "modifiedFunctions": \[\n \{\n "name": "java::Test\.<init>:\(\)V",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.<init>:\(\)V",\n "line": "1"\n \}\n \},\n \{\n "name": "java::Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(I\)I",\n "line": "6"\n \}\n \},\n \{\n "name": "java::Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.bar:\(I\)I",\n "line": "14"\n \}\n \}\n \],\n "newFunctions": \[ \],
--
^warning: ignoring

4
jbmc/regression/jdiff/java-scope-change3/test.desc
View File

@ -3,8 +3,8 @@ new.jar
old.jar --json-ui
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
"deletedFunctions": \[ \],\n "modifiedFunctions": \[\n \{\n "name": "java::Test\.<init>:\(\)V",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.<init>:\(\)V",\n "line": "1"\n \}\n \},\n \{\n "name": "java::Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(I\)I",\n "line": "6"\n \}\n \},\n \{\n "name": "java::Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.bar:\(I\)I",\n "line": "14"\n \}\n \}\n \],\n "newFunctions": \[ \],
--
^warning: ignoring

4
jbmc/regression/jdiff/java-tmp-vars-array/test.desc
View File

@ -3,8 +3,8 @@ new.jar
old.jar
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
new functions:\nmodified functions:\n Test\.java: java::Test\.f00:\(\[I\)\[I\ndeleted functions:
--
^warning: ignoring

4
jbmc/regression/jdiff/java-tmp-vars-inc/test.desc
View File

@ -3,8 +3,8 @@ new.jar
old.jar
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
new functions:\nmodified functions:\n Test\.java: java::Test\.f00:\(I\)I\ndeleted functions:
--
^warning: ignoring

4
jbmc/regression/jdiff/java-tmp-vars-new/test.desc
View File

@ -3,8 +3,8 @@ new.jar
old.jar
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
new functions:\nmodified functions:\n Test\.java: java::Test\.f00:\(LA;\)LA;\ndeleted functions:
--
^warning: ignoring

4
jbmc/regression/jdiff/java-tmp-vars-string/test.desc
View File

@ -3,8 +3,8 @@ new.jar
old.jar
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
new functions:\nmodified functions:\n Test\.java: java::Test\.f00:\(Ljava/lang/String;\)Ljava/lang/String;\ndeleted functions:
--
^warning: ignoring

4
jbmc/regression/jdiff/java-virtual-methods/test.desc
View File

@ -3,8 +3,8 @@ new.jar
old.jar
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
new functions:\nmodified functions:\ndeleted functions:
--
^warning: ignoring

4
jbmc/regression/jdiff/syntactic-diff-java1/test.desc
View File

@ -3,8 +3,8 @@ old.jar
new.jar
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
new functions:\n Test\.java: java::Test\.foo:\(\)V\nmodified functions:\n Test\.java: java::Test\.run:\(\)I\ndeleted functions:\n Test\.java: java::Test\.bar:\(\)V
--
^warning: ignoring

2
regression/cbmc-cover/block-coverage-report1/test.desc
View File

@ -6,4 +6,6 @@ block 2 \(lines main.c:main:6\): SATISFIED
block 3 \(lines main.c:main:6,9\): FAILED
block 4 \(lines main.c:main:8\): SATISFIED
block 5 \(lines main.c:main:9\): SATISFIED
^EXIT=0$
^SIGNAL=0$
--

2
regression/cbmc-cover/block-coverage-report2/test.desc
View File

@ -9,4 +9,6 @@ block 5 \(lines main.c:main:20\): SATISFIED
block 6 \(lines main.c:main:15,21,22\): SATISFIED
block 7 \(lines main.c:main:24,25\): SATISFIED
block 1 \(lines main.c:foo:6-9\): SATISFIED
^EXIT=0$
^SIGNAL=0$
--

2
regression/cbmc-cover/block-coverage-report3/test.desc
View File

@ -5,4 +5,6 @@ block 1 \(lines main.c:main:3\): SATISFIED
block 2 \(lines main.c:main:4\): SATISFIED
block 3 \(lines main.c:main:4,6\): SATISFIED
block 4 \(lines main.c:main:8\): FAILED
^EXIT=0$
^SIGNAL=0$
--

2
regression/cbmc-cover/block-coverage-report4/test.desc
View File

@ -5,4 +5,6 @@ block 1 \(lines main.c:main:3\): SATISFIED
block 2 \(lines main.c:main:4\): SATISFIED
block 3 \(lines main.c:main:4,6\): SATISFIED
block 4 \(lines main.c:main:8\): SATISFIED
^EXIT=0$
^SIGNAL=0$
--

2
regression/cbmc/address_space_size_limit2/test.desc
View File

@ -1,5 +1,7 @@
KNOWNBUG
test.i
--32 --object-bits 31 --unwind 11 --no-simplify
^EXIT=10$
^SIGNAL=0$
dynamic object too large
--

2
regression/cbmc/array-function-parameters/test.desc
View File

@ -1,6 +1,8 @@
CORE broken-smt-backend
test.c
--function test --min-null-tree-depth 2 --max-nondet-tree-depth 2 --bounds-check
^EXIT=10$
^SIGNAL=0$
\[test.assertion.1\] line \d+ assertion Test.lists\[0\]->next: SUCCESS
\[test.assertion.2\] line \d+ assertion Test.lists\[1\]->next: SUCCESS
\[test.assertion.3\] line \d+ assertion Test.lists\[2\]->next: SUCCESS

2
regression/cbmc/destructors/compound_literal.desc
View File

@ -3,6 +3,8 @@ main.c
--unwind 10 --show-goto-functions
activate-multi-line-match
(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*dead newAlloc0;[\s]*(?P>comment_block)[\s]*dead pc;[\s]*(?P>comment_block)[\s]*dead literal;[\s]*(?P>comment_block)[\s]*9: END_FUNCTION
^EXIT=0$
^SIGNAL=0$
--
--
Checks for:

2
regression/cbmc/destructors/enter_lexical_block.desc
View File

@ -3,6 +3,8 @@ main.c
--unwind 10 --show-goto-functions
activate-multi-line-match
(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*6: test newAlloc4;[\s]*(?P>comment_block)[\s]*newAlloc4 = \{ \.id=4 \};[\s]*(?P>comment_block)[\s]*test newAlloc6;[\s]*(?P>comment_block)[\s]*newAlloc6 = \{ \.id=6 \};[\s]*(?P>comment_block)[\s]*test newAlloc7;[\s]*(?P>comment_block)[\s]*newAlloc7 = \{ \.id=7 \};[\s]*(?P>comment_block)[\s]*GOTO 3
^EXIT=0$
^SIGNAL=0$
--
--
Checks for:

4
regression/cbmc/json1/test.desc
View File

@ -2,8 +2,8 @@ CORE
main.c
--json-ui --stop-on-fail
activate-multi-line-match
EXIT=10
SIGNAL=0
^EXIT=10$
^SIGNAL=0$
\[\n \{\n "program": "CBMC .*"\n \},\n \{\n "messageText": "CBMC .*",\n "messageType": "STATUS-MESSAGE"\n \},\n \{\n "messageText": "Parsing main\.c",\n "messageType": "STATUS-MESSAGE"\n \},
\]\n \},\n \{\n "messageText": "VERIFICATION FAILED",\n "messageType": "STATUS-MESSAGE"\n \},\n \{\n "cProverStatus": "failure"\n \}\n\]
--

4
regression/cbmc/multiple-goto-traces/test.desc
View File

@ -2,8 +2,8 @@ CORE
main.c
--trace
activate-multi-line-match
EXIT=10
SIGNAL=0
^EXIT=10$
^SIGNAL=0$
VERIFICATION FAILED
Trace for main\.assertion\.1:(\n.*){16} assertion 4 \!= argc(\n.*){5}Trace for main\.assertion\.3:(\n.*){30} assertion argc != 4(\n.*){5}Trace for main\.assertion\.4:(\n.*){44} assertion argc \+ 1 != 5
\*\* 3 of 4 failed

2
regression/cbmc/reachability-slice-interproc/test.desc
View File

@ -1,6 +1,8 @@
CORE
test.c
--reachability-slice-fb --show-goto-functions
^EXIT=0$
^SIGNAL=0$
target_kept
reachable_before_target_caller_1_kept
reachable_after_target_caller_1_kept

2
regression/cbmc/reachability-slice/test.desc
View File

@ -1,6 +1,8 @@
CORE
test.c
--reachability-slice --show-goto-functions --cover location --property foo.coverage.2
^EXIT=0$
^SIGNAL=0$
= 1001
--
= 1004

2
regression/cbmc/reachability-slice/test2.desc
View File

@ -1,6 +1,8 @@
CORE
test.c
--reachability-slice-fb --show-goto-functions --cover location --property foo.coverage.2
^EXIT=0$
^SIGNAL=0$
= 1001
= 1002
= 1003

2
regression/cbmc/reachability-slice/test3.desc
View File

@ -1,6 +1,8 @@
CORE
test.c
--reachability-slice --show-goto-functions --cover location
^EXIT=0$
^SIGNAL=0$
= 1001
= 1002
= 1003

4
regression/cbmc/typedef-anon-struct1/test.desc
View File

@ -3,8 +3,8 @@ main.c
--show-symbol-table --function fun
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
Base name\.+: mystruct_var\nMode\.+: C\nType\.+: MYSTRUCT
--
warning: ignoring

4
regression/cbmc/typedef-anon-struct2/test.desc
View File

@ -3,8 +3,8 @@ main.c
--show-symbol-table --function fun
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
Base name\.+: mystruct_var\nMode\.+: C\nType\.+: MYSTRUCT
Base name\.+: another_mystruct_var\nMode\.+: C\nType\.+: MYSTRUCT
--

4
regression/cbmc/typedef-anon-union1/test.desc
View File

@ -3,8 +3,8 @@ main.c
--show-symbol-table --function fun
// Enable multi-line checking
activate-multi-line-match
EXIT=0
SIGNAL=0
^EXIT=0$
^SIGNAL=0$
Base name\.+: myunion_var\nMode\.+: C\nType\.+: MYUNION
--
warning: ignoring

Some files were not shown because too many files have changed in this diff Show More