Merge pull request #2907 from peterschrammel/remove-deprecated-options

Remove deprecated Java and string options [TG-4282]

Author: peterschrammel

jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

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

@@ -1,5 +1,5 @@
 CORE
 A.class
---function 'A.me2:()V' --lazy-methods --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me:()V' --lazy-methods --java-threading
+--function 'A.me:()V' --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

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

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

jbmc/regression/jbmc-concurrency/get-current-thread/test.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods
+--function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods
+--function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me5:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods
+--function 'A.me5:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me6:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods
+--function 'A.me6:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

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

@@ -1,5 +1,5 @@
 CORE
 A.class
---function 'A.me2:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^SIGNAL=0$
 ^VERIFICATION FAILED

jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me4:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me3:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me:()V'  --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me:()V'  --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

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

@@ -1,5 +1,5 @@
 CORE
 A.class
---function 'A.me2:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading --lazy-methods
+--function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading --lazy-methods
+--function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc-concurrency/several-threads/test.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function A.me --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function A.me --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

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

@@ -1,5 +1,5 @@
 CORE
 A.class
---function A.me2 --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function A.me2 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-concurrency/several-threads/test3.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function A.me3 --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading --unwind 3
+--function A.me3 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading --unwind 3
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Sync.class
---lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

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

@@ -1,6 +1,6 @@
 KNOWNBUG
 Sync.class
---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods --java-threading
+--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

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

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --lazy-methods
+--function 'A.me0:()V'
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions --java-threading
+--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions --java-threading
 ATOMIC_BEGIN
 ATOMIC_END
 --

jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods --java-threading
+--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-blocks/test4.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.aStatic' --lazy-methods
+--function 'A.aStatic'
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me2:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me1:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc

@@ -1,6 +1,6 @@
 CORE
 Sync.class
---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods --java-threading
+--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

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

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions --lazy-methods
+--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions
 ATOMIC_BEGIN
 ATOMIC_END
 --

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

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me1:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions
+--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions
 ATOMIC_BEGIN
 ATOMIC_END
 --

jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me1:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me3:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me3:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me2:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_static.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 A.class
---function 'A.me4:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc/NondetInit/test_lazy.desc

@@ -1,9 +1,9 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---function Test.check --lazy-methods
+--function Test.check
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)

jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc

@@ -9,4 +9,4 @@ annotations.class
 --
 --
 The purpose of the test is ensuring that annotations can be shown in the symbol
-table.
+table.

jbmc/regression/jbmc/class-literals/test_lazy.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---lazy-methods --function Test.main
+--function Test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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

@@ -1,6 +1,6 @@
 KNOWNBUG
 Test.class
---function Test.test --show-goto-functions --lazy-methods
+--function Test.test --show-goto-functions
 EXIT=0
 SIGNAL=0
 ObjectWithNondetInitialize\.cproverNondetInitialize\(\)

jbmc/regression/jbmc/enum_switch/test.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 com/diffblue/regression/Foo.class
---trace --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 10 --function "com.diffblue.regression.Foo.foo" --java-unwind-enum-static
+--trace --depth 1024 --java-max-vla-length 16 --max-nondet-string-length 20 --string-printable --unwind 10 --function "com.diffblue.regression.Foo.foo" --java-unwind-enum-static
 assertion at file com/diffblue/regression/Foo.java line 8 .*: FAILURE
 assertion at file com/diffblue/regression/Foo.java line 11 .*: FAILURE
 assertion at file com/diffblue/regression/Foo.java line 14 .*: FAILURE

jbmc/regression/jbmc/json_trace1/test.desc

@@ -6,4 +6,4 @@ Test.class
 --
 ^warning: ignoring
 --
-Tests that it doesn't crash.
+Tests that it doesn't crash.

jbmc/regression/jbmc/lazyloading1/test.desc

@@ -1,10 +1,10 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.main
+--verbosity 10 --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 elaborate java::A\.f:\(\)V
 --
 elaborate java::B\.g:\(\)V
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)

jbmc/regression/jbmc/lazyloading10/test.desc

@@ -1,9 +1,9 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point test.sety
+--verbosity 10 --function test.f --lazy-methods-extra-entry-point test.sety
 ^SIGNAL=0$
 CI lazy methods: elaborate java::test\.sety:\(I\)V
 CI lazy methods: elaborate java::test\.sety:\(F\)V
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)

jbmc/regression/jbmc/lazyloading11/test.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:\(I\)V' --lazy-methods-extra-entry-point 'test.sety:\(F\)V'
+--verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:\(I\)V' --lazy-methods-extra-entry-point 'test.sety:\(F\)V'
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
@@ -9,4 +9,4 @@ CI lazy methods: elaborate java::test\.sety:\(F\)V
 --
 CI lazy methods: elaborate java::test\.setx:\(I\)V
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)

jbmc/regression/jbmc/lazyloading2/test.desc

@@ -1,10 +1,10 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.main
+--verbosity 10 --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 elaborate java::A\.f:\(\)V
 --
 elaborate java::B\.g:\(\)V
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)

jbmc/regression/jbmc/lazyloading3/test.desc

@@ -1,10 +1,10 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.main
+--verbosity 10 --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 elaborate java::A\.f:\(\)V
 --
 elaborate java::B\.g:\(\)V
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)

jbmc/regression/jbmc/lazyloading4/test.desc

@@ -1,9 +1,9 @@
 CORE symex-driven-lazy-loading-expected-failure
 Main.class
---lazy-methods
+
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)