Merge pull request diffblue#4073 from tautschnig/verbosity-10

Remove unnecessary "--verbosity 10" from regression tests

Author: tautschnig

jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_det.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.det --verbosity 10
+--function Test.det
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 22 .*: FAILURE

jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_nondet.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.nonDet --verbosity 10 --max-nondet-string-length 1000
+--function Test.nonDet --max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 48 .*: FAILURE

jbmc/regression/jbmc-strings/StringConcat/test_buffer_det.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---max-nondet-string-length 100 --function Test.bufferDet --depth 10000  --verbosity 10
+--max-nondet-string-length 100 --function Test.bufferDet --depth 10000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---max-nondet-string-length 100 --function Test.bufferNonDetLoop --depth 10000 --unwind 5  --verbosity 10  --property 'java::Test.bufferNonDetLoop:(ILjava/lang/String;)Ljava/lang/String;.assertion.1'
+--max-nondet-string-length 100 --function Test.bufferNonDetLoop --depth 10000 --unwind 5   --property 'java::Test.bufferNonDetLoop:(ILjava/lang/String;)Ljava/lang/String;.assertion.1'
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop2.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---max-nondet-string-length 100 --function Test.bufferNonDetLoop2 --depth 10000 --unwind 5  --verbosity 10
+--max-nondet-string-length 100 --function Test.bufferNonDetLoop2 --depth 10000 --unwind 5
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop3.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---max-nondet-string-length 100 --function Test.bufferNonDetLoop3 --depth 10000 --unwind 5  --verbosity 10
+--max-nondet-string-length 100 --function Test.bufferNonDetLoop3 --depth 10000 --unwind 5
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop4.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---max-nondet-string-length 100 --function Test.bufferNonDetLoop4 --depth 10000 --unwind 5  --verbosity 10 --property 'java::Test.bufferNonDetLoop4:(IILjava/lang/String;)Ljava/lang/String;.assertion.1'
+--max-nondet-string-length 100 --function Test.bufferNonDetLoop4 --depth 10000 --unwind 5  --property 'java::Test.bufferNonDetLoop4:(IILjava/lang/String;)Ljava/lang/String;.assertion.1'
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---max-nondet-string-length 100 --function Test.bufferNonDetLoop5 --depth 10000 --unwind 3 --verbosity 10
+--max-nondet-string-length 100 --function Test.bufferNonDetLoop5 --depth 10000 --unwind 3
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringConcat/test_char_buffer_det.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---max-nondet-string-length 100 --function Test.charBufferDet --depth 10000  --verbosity 10
+--max-nondet-string-length 100 --function Test.charBufferDet --depth 10000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringConcat/test_char_buffer_det_loop.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---max-nondet-string-length 100 --function Test.charBufferDetLoop --depth 10000 --unwind 5  --verbosity 10
+--max-nondet-string-length 100 --function Test.charBufferDetLoop --depth 10000 --unwind 5
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringConcat/test_char_buffer_det_loop2.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---max-nondet-string-length 100 --function Test.charBufferDetLoop2 --depth 10000 --unwind 5  --verbosity 10
+--max-nondet-string-length 100 --function Test.charBufferDetLoop2 --depth 10000 --unwind 5
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringConcat/test_string_det.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---max-nondet-string-length 100 --function Test.stringDet --depth 10000  --verbosity 10
+--max-nondet-string-length 100 --function Test.stringDet --depth 10000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringConcat/test_string_nondet.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---max-nondet-string-length 100 --function Test.stringNonDet --depth 10000 --unwind 5 --verbosity 10
+--max-nondet-string-length 100 --function Test.stringNonDet --depth 10000 --unwind 5
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringConcat_StringII/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---max-nondet-string-length 4 --verbosity 10 --unwind 5 --function Test.testSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+--max-nondet-string-length 4 --unwind 5 --function Test.testSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 assertion at file Test.java line 23 .*: SUCCESS

jbmc/regression/jbmc-strings/StringConcat_StringII/test_fail.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---max-nondet-string-length 10000 --verbosity 10 --function Test.testFail
+--max-nondet-string-length 10000 --function Test.testFail
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 38 .*: FAILURE

jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.withDependency  --verbosity 10 --max-nondet-string-length 10000
+--function Test.withDependency  --max-nondet-string-length 10000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 48 .*: SUCCESS

jbmc/regression/jbmc-strings/StringToLowerCase/test_det.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.det  --verbosity 10
+--function Test.det 
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 11 .*: FAILURE

jbmc/regression/jbmc-strings/StringToLowerCase/test_nondet.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.nonDet  --verbosity 10 --max-nondet-string-length 1000
+--function Test.nonDet  --max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 31 .*: FAILURE

jbmc/regression/jbmc-strings/StringToUpperCase/test_dependency.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.withDependency --verbosity 10 --max-nondet-string-length 10000
+--function Test.withDependency --max-nondet-string-length 10000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 48 .*: SUCCESS

jbmc/regression/jbmc-strings/StringToUpperCase/test_det.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.det  --verbosity 10
+--function Test.det
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 11 .*: FAILURE

jbmc/regression/jbmc-strings/StringToUpperCase/test_nondet.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.nonDet --verbosity 10 --max-nondet-string-length 1000
+--function Test.nonDet --max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 31 .*: FAILURE

jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.checkDet --verbosity 10
+--function Test.checkDet
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 26 .*: FAILURE

jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.checkNonDet --verbosity 10
+--function Test.checkNonDet
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 55 .*: FAILURE

jbmc/regression/jbmc-strings/max-length/test1.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---verbosity 10 --max-nondet-string-length 499999 --function Test.checkMaxInputLength
+--max-nondet-string-length 499999 --function Test.checkMaxInputLength
 ^EXIT=0$
 ^SIGNAL=0$
 assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 17: SUCCESS

jbmc/regression/jbmc-strings/max-length/test2.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---verbosity 10 --max-nondet-string-length 500000 --function Test.checkMaxInputLength
+--max-nondet-string-length 500000 --function Test.checkMaxInputLength
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 17: FAILURE

jbmc/regression/jbmc-strings/max-length/test3.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---verbosity 10 --max-nondet-string-length 4001 --function Test.checkMaxLength
+--max-nondet-string-length 4001 --function Test.checkMaxLength
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 27: FAILURE

jbmc/regression/jbmc-strings/max-length/test4.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---verbosity 10 --max-nondet-string-length 4000 --function Test.checkMaxLength
+--max-nondet-string-length 4000 --function Test.checkMaxLength
 ^SIGNAL=0$
 --
 ^EXIT=0$

jbmc/regression/jbmc-strings/string-input-value/test1.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---verbosity 10 --string-input-value fo --string-input-value barr --function Test.checkStringInputValue --string-input-value "" --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+--string-input-value fo --string-input-value barr --function Test.checkStringInputValue --string-input-value "" --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.1.*FAILURE

jbmc/regression/jbmc-strings/string-input-value/test2.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---verbosity 10 --function Test.checkStringInputValue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+--function Test.checkStringInputValue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.1.*FAILURE

jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc

@@ -1,6 +1,6 @@
 CORE
 annotations.class
---no-lazy-methods --verbosity 10 --show-symbol-table --function annotations.main
+--no-lazy-methods --show-symbol-table --function annotations.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^Type\.\.\.\.\.\.\.\.: @java::ClassAnnotation struct annotations

jbmc/regression/jbmc/lambda2/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 SymStream.class
---verbosity 10 --show-goto-functions
+--show-goto-functions
 lambda function reference org/symphonyoss/symphony/clients/model/SymUser\.toSymUser in class \"SymStream\"
 ^EXIT=0
 ^SIGNAL=0

jbmc/regression/jbmc/lambda2/test_no_crash.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 SymStream.class
---no-lazy-methods --verbosity 10 --show-goto-functions
+--no-lazy-methods --show-goto-functions
 ^EXIT=0
 ^SIGNAL=0
 --

jbmc/regression/jbmc/lvt-unexpected/test.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 unexpected.class
---verbosity 10 --show-symbol-table
+--show-symbol-table
 ^EXIT=0$
 ^SIGNAL=0$
 --

jbmc/regression/jbmc/method_parameters1/test.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 method_parameters.class
---verbosity 10 --show-symbol-table
+--show-symbol-table
 ^EXIT=0$
 ^SIGNAL=0$
 --

jbmc/regression/jbmc/method_parameters2/test.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 method_parameters.class
---verbosity 10 --show-symbol-table
+--show-symbol-table
 ^EXIT=0$
 ^SIGNAL=0$
 --

jbmc/regression/strings-smoke-tests/java_append_char/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_append_char.class
---verbosity 10 --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_append_char.java line 23 .* SUCCESS

jbmc/regression/strings-smoke-tests/java_append_int/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 test_append_int.class
---verbosity 10 --max-nondet-string-length 1000
+--max-nondet-string-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/strings-smoke-tests/java_append_string/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_append_string.class
---verbosity 10 --max-nondet-string-length 1000 --function test_append_string.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+--max-nondet-string-length 1000 --function test_append_string.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/strings-smoke-tests/java_case/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_case.class
---verbosity 10 --max-nondet-string-length 1000 --function test_case.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+--max-nondet-string-length 1000 --function test_case.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_case.java line 10 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_char_array/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_char_array.class
---verbosity 10 --max-nondet-string-length 1000 --function test_char_array.main
+--max-nondet-string-length 1000 --function test_char_array.main
 ^EXIT=10$
 ^SIGNAL=0$
 .*assertion.* test_char_array.java line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_char_at/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_char_at.class
---verbosity 10 --max-nondet-string-length 1000 --function test_char_at.main
+--max-nondet-string-length 1000 --function test_char_at.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/strings-smoke-tests/java_code_point/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_code_point.class
---verbosity 10 --max-nondet-string-length 1000 --function test_code_point.main
+--max-nondet-string-length 1000 --function test_code_point.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/strings-smoke-tests/java_contains/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_contains.class
---verbosity 10 --max-nondet-string-length 100 --function test_contains.main
+--max-nondet-string-length 100 --function test_contains.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$

jbmc/regression/strings-smoke-tests/java_contains/test_string_printable.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 test_contains.class
---verbosity 10 --max-nondet-string-length 100 --string-printable --function test_contains.main
+--max-nondet-string-length 100 --string-printable --function test_contains.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$

jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_delete_char_at.class
---verbosity 10 --max-nondet-string-length 1000 --function test_delete_char_at.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+--max-nondet-string-length 1000 --function test_delete_char_at.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/strings-smoke-tests/java_endswith/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_endswith.class
---verbosity 10 --max-nondet-string-length 100 --function test_endswith.main
+--max-nondet-string-length 100 --function test_endswith.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$

jbmc/regression/strings-smoke-tests/java_equal/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_equal.class
---verbosity 10 --max-nondet-string-length 100 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+--max-nondet-string-length 100 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* FAILURE$

jbmc/regression/strings-smoke-tests/java_equal/test_2.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 test_equal_2.class
---verbosity 10 --max-nondet-string-length 100
+--max-nondet-string-length 100
 ^EXIT=0$
 ^SIGNAL=0$
 --

jbmc/regression/strings-smoke-tests/java_float/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 test_float.class
---verbosity 10 --max-nondet-string-length 1000 --function test_float.main
+--max-nondet-string-length 1000 --function test_float.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/strings-smoke-tests/java_format/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---verbosity 10 --max-nondet-string-length 20 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+--max-nondet-string-length 20 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 6.* SUCCESS$