Cbmc merge 2018-07-12 (diffblue#499)

* Squashed 'cbmc/' changes from 6409eae..2af8433

2af8433 Merge pull request diffblue#2566 from tautschnig/vs-sparse-array
de65ec6 Merge pull request diffblue#2541 from tautschnig/vs-string-static
7c4b5aa Merge pull request diffblue#2568 from tautschnig/vs-parameter-names
ef3eb4f Merge pull request diffblue#2567 from peterschrammel/fix-mcdc
53baae6 Merge pull request diffblue#2460 from tautschnig/vs-local-unused
6acabcb Merge pull request diffblue#2563 from tautschnig/vs-rm-interface
3c2e55e Merge pull request diffblue#2426 from peterschrammel/java-models-library-submodule
440ceb6 Document proposed best practice for unused parameters
370d4c6 Convert /* */ comments into //
1abbf1e Clean up commented code
b34e951 Use submodule to download java-models-library
3f255b2 Merge pull request diffblue#2388 from peterschrammel/improve-jbmc-options
15f44c7 Revert "Mark tests which fail due to invariant violations"
dce4afd Make local-assigned-but-not-used annotation applicable to all compilers
86d057d (interval_)sparse_arrayt: Remove unnecessary use of "virtual" and further cleanup
0d7a943 Merge pull request diffblue#2558 from tautschnig/linking-xen
5acc0b0 Merge pull request diffblue#2392 from NathanJPhillips/cleanup/small_map_layout
ee4d802 Merge pull request diffblue#2565 from tautschnig/vs-float-bvt
754b36d Accept more mismatching function definition/declaration pairs
d1a4169 Merge pull request diffblue#2542 from tautschnig/vs-string-refinement
b2cd358 Cleanup of float_bvt
0a39f40 Remove unused interface
c749b8f Merge pull request diffblue#2429 from tautschnig/vs-endian
0a10bf3 Drop java prefix from throw-runtime-exceptions option
548baea Improve naming of command line options
39bc7ea Make --lazy-methods and --refine-strings default
eb9e3bb Merge pull request diffblue#2561 from Degiorgio/get-current-thread-id-fix
d98a39b Merge pull request diffblue#2556 from peterschrammel/run-string-smoke-tests
34404f0 Set little_endian in the same way that boolbv_byte_extract already does
4a8dc96 JBMC: removed camel-casing from function identifiers
9059be7 JBMC: CProver.getCurrentThreadID:()I conversion fix
d393d1c Merge pull request diffblue#2435 from tautschnig/vs-ranged-for
be7159a Merge pull request diffblue#2425 from tautschnig/vs-virtual
44cc033 Change index variable name, simplify code
0c9658f Add missing virtual destructor
c6f9231 Merge pull request diffblue#2553 from tautschnig/always-inline-partial-revert
fa94bc0 Merge pull request diffblue#2531 from tautschnig/debian4
41863e7 Merge pull request diffblue#2539 from tautschnig/vs-unsigned-constant
f1afbff Remove unnecessary PLATFORM_DIRS
0c75b47 Run strings-smoke-tests and janalyzer tests
0acae08 Merge pull request diffblue#2535 from tautschnig/debian7
35ddf0b Merge pull request diffblue#2533 from tautschnig/debian5
580f539 Merge pull request diffblue#2534 from tautschnig/debian6
b73a9e3 Merge pull request diffblue#2420 from tautschnig/vs-invariant
9b087dc Merge pull request diffblue#2550 from tautschnig/vs-return
dc35270 Merge pull request diffblue#2547 from tautschnig/vs-dummy-init
ff88c16 Merge pull request diffblue#2554 from tautschnig/ld-options
3209628 Merge pull request diffblue#2450 from tautschnig/c++-name-resolution
61a6acd Name resolution may require further template instantiation
0f15d47 goto-ld: accept (but do not process) further ld options
4c6cfc0 Merge pull request diffblue#2448 from tautschnig/c++-delayed-body
c46d46d Merge pull request diffblue#2439 from tautschnig/vs-pointer
7e4dd05 Merge pull request diffblue#2440 from tautschnig/vs-list
1f237ff Merge pull request diffblue#2464 from tautschnig/vs-unused1
7be54b8 Merge pull request diffblue#2544 from tautschnig/vs-value-set
7f373c8 Merge pull request diffblue#2549 from tautschnig/vs-unsigned-option
b17fefa Merge pull request diffblue#2540 from tautschnig/vs-explicit-cast
425db26 Merge pull request diffblue#2530 from tautschnig/debian3
2598141 Mark integer constants as unsigned when lhs is unsigned
0da9766 Merge pull request diffblue#2538 from tautschnig/vs-use-to_ulong
e501317 Additional regression tests for always_inline
17a50c5 Revert "Apply symbol replacement in type_arg members"
016ad92 Revert "Fully interpret __attribute__((always_inline))"
ee9444f Merge pull request diffblue#2532 from tautschnig/debian2
c8725cb Merge pull request diffblue#2536 from tautschnig/debian8
d6565ec Merge pull request diffblue#2537 from tautschnig/vs-non-deprecated
16e6a99 Use type-consistent unsigned value for unreachable return statement
a746a2c Extract unsigned value from options
681ec22 Add dummy initialisation to avoid Visual Studio warning
c789088 Remove unused parameter from value_set_fivrt::flatten_rec
4d8aa45 Use std::string(N, ' ') instead of static locals
18faa5a String refinement: remove unused parameters
96a7014 Explicit type cast to avoid signed/unsigned warning
2aa6a2f Use non-deprecated to_integer(constant_expr)
13f83d5 Use to_ulong instead of the deprecated integer2ulong
26803f7 Test only works with simplification enabled
be5f2ff Use architecture-specific compiler flags to configure bit width during preprocessing
60ad26c kfreebsd also uses ELF, and hybrid binaries are thus supported
c6c1938 utf8 to utf16 conversion must use native endianness
bc7a527 Fix copy&paste error in C library
cd6127a Regression test should succeed even if char is an unsigned type
dab6a6e Fix tests that are only correct on little-endian architectures
8187bdd Merge pull request diffblue#2526 from jeannielynnmoulton/jeannie/AnonymousInnerClasses
af0ce5a Captures anonymous inner class information.
d20a12e Merge pull request diffblue#2517 from jeannielynnmoulton/jeannie/InnerStaticClasses
fe73955 Captures information for static inner classes.
4193f02 Remove unused parameters message_handler, ns
02e3840 Fix delayed method body conversion for templates
d0c2a49 Remove unused parameter from list_calls_and_arguments
0e9aa90 Remove unused and inconsistent pointer_object_has_type
497d296 Fix invariant: value must be strictly positive
3aa9b72 Add comment explaining unusual layout

git-subtree-dir: cbmc
git-subtree-split: 2af8433

* Add .gitmodules with details of java-models-library

* Small changes to jbmc command line arguments

* Add --no-refine-strings to cmdline, always set

Author: owen-jones-diffblue

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "cbmc/jbmc/lib/java-models-library"]
+	path = cbmc/jbmc/lib/java-models-library
+	url = https://github.com/diffblue/java-models-library.git

cbmc/.gitmodules

@@ -0,0 +1,3 @@
+[submodule "jbmc/lib/java-models-library"]
+	path = jbmc/lib/java-models-library
+	url = https://github.com/diffblue/java-models-library.git

cbmc/.travis.yml

@@ -229,6 +229,7 @@ jobs:
         - ccache -z
         - ccache --max-size=1G
         - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-5'
+        - git submodule update --init --recursive
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE -j2)
 
@@ -254,6 +255,7 @@ jobs:
         - ccache -z
         - ccache --max-size=1G
         - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7'
+        - git submodule update --init --recursive
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE -j2)
 
@@ -287,6 +289,7 @@ jobs:
         - ccache -z
         - ccache --max-size=1G
         - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/clang++-6.0' '-DCMAKE_CXX_FLAGS=-Qunused-arguments'
+        - git submodule update --init --recursive
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE -j2)
 
@@ -305,6 +308,7 @@ jobs:
         - ccache -z
         - ccache --max-size=1G
         - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64'
+        - git submodule update --init --recursive
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE -j2)
 
@@ -328,7 +332,7 @@ jobs:
             name: "diffblue/cbmc"
             description: "Travis build of ${TRAVIS_COMMIT}"
           notification_email: "[email protected]"
-          build_command_prepend: "make -C jbmc/src java-models-library-download"
+          build_command_prepend: "make -C jbmc/src setup-submodules"
           build_command_prepend: "make -C src minisat2-download"
           build_command: "make -C src -j2; make -C jbmc/src -j2"
           branch_pattern: "develop"
@@ -349,7 +353,7 @@ jobs:
 install:
   - ccache -z
   - ccache --max-size=1G
-  - make -C jbmc/src java-models-library-download
+  - make -C jbmc/src setup-submodules
   - make -C src minisat2-download
   - make -C src boost-download
   - make -C src/ansi-c library_check

cbmc/CMakeLists.txt

@@ -84,6 +84,7 @@ set_target_properties(
     xml
 
     java_bytecode
+    java-models-library
     jbmc
     jbmc-lib
     janalyzer

cbmc/CODING_STANDARD.md

@@ -95,6 +95,9 @@ Formatting is enforced using clang-format. For more information about this, see
 # Naming
 - Identifiers may use the characters `[a-z0-9_]` and should start with a
   lower-case letter (parameters in constructors may start with `_`).
+- Omit names of parameters or exception objects when they are not used. If
+  parameter names help documenting an interface, keep the name and use
+  `(void)parameter_name;` in the body of the method.
 - Use American spelling for identifiers.
 - Separate basic words by `_`
 - Avoid abbreviations (e.g. prefer `symbol_table` to `st`).

cbmc/appveyor.yml

@@ -42,17 +42,13 @@ install:
      & 7z x minisat2_2.2.1.orig.tar.gz
      &7z x minisat2_2.2.1.orig.tar
     }
-    if (!(Test-Path java-models-library-master\.gitignore)) {
-     & appveyor downloadfile https://github.com/diffblue/java-models-library/archive/master.zip -FileName jml.zip
-     & 7z x jml.zip
-    }
     cd ..
 
 cache: deps
 
 build_script:
 - cmd: |
-    cp -r deps/java-models-library-master/src jbmc/src/java_bytecode/library
+    make -C jbmc/src setup-submodules
     cp -r deps/minisat2-2.2.1 minisat-2.2.1
     patch -d minisat-2.2.1 -p1 < scripts/minisat-2.2.1-patch
     call "C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC\vcvarsall.bat" x64

cbmc/buildspec-windows.yml

@@ -19,7 +19,7 @@ phases:
 
       - |
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
-        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C jbmc/src BUILD_ENV=MSVC" '
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C jbmc/src setup-submodules" && bash -c "make -j4 -C jbmc/src BUILD_ENV=MSVC" '
         cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C jbmc/unit all BUILD_ENV=MSVC ; exit 0" '
 
   post_build:

cbmc/buildspec.yml

@@ -15,7 +15,7 @@ phases:
     commands:
       - echo Build started on `date`
       - make -C src minisat2-download
-      - make -C jbmc/src java-models-library-download
+      - make -C jbmc/src setup-submodules
       - make -C src CXX="ccache g++" -j2
       - make -C unit CXX="ccache g++" -j2
       - make -C jbmc/src CXX="ccache g++" -j2

cbmc/jbmc/CMakeLists.txt

@@ -1,3 +1,9 @@
 add_subdirectory(regression)
 add_subdirectory(src)
 add_subdirectory(unit)
+
+add_custom_target(java-models-library ALL
+    COMMAND mvn package
+    COMMAND cp target/core-models.jar ${CMAKE_CURRENT_SOURCE_DIR}/src/java_bytecode/library/
+    WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/lib/java-models-library
+)

cbmc/jbmc/lib/java-models-library

@@ -1,32 +1,27 @@
 # For the best possible utilisation of multiple cores when
 # running tests in parallel, it is important that these directories are
 # listed with decreasing runtimes (i.e. longest running at the top)
-DIRS = janalzyer-taint \
+DIRS = janalyzer-taint \
        jbmc \
        jbmc-concurrency \
        jbmc-cover \
        jbmc-inheritance \
        jbmc-strings \
        jdiff \
-       string-smoke-tests \
+       strings-smoke-tests \
        jbmc-generics \
        # Empty last line
 
-# Tests under goto-gcc cannot be run on Windows, so appveyor.yml unlinks
-# the entire directory under Windows. This variable will contain the list
-# of directories that actually exist on the current platform.
-PLATFORM_DIRS = $(wildcard $(DIRS))
-
 # Run all test directories in sequence
 .PHONY: test
 test:
-	@for dir in $(PLATFORM_DIRS); do \
+	@for dir in $(DIRS); do \
 		$(MAKE) "$$dir" || exit 1; \
 	done;
 
 # Pattern to execute a single test suite directory
-.PHONY: $(PLATFORM_DIRS)
-$(PLATFORM_DIRS):
+.PHONY: $(DIRS)
+$(DIRS):
 	@echo "Running $@..." ;
 	$(MAKE) -C "$@" test || exit 1;
 
@@ -42,7 +37,7 @@ test-parallel:
 		--linebuffer \
 		--jobs $(JOBS) \
 		$(MAKE) "{}" \
-		::: $(PLATFORM_DIRS)
+		::: $(DIRS)
 
 
 .PHONY: clean

cbmc/jbmc/regression/Makefile

@@ -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`
+--function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

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

@@ -1,6 +1,6 @@
 CORE
 TestClass.class
---function TestClass.testFunction --classpath ../../../src/java_bytecode/library/core-models.jar:.
+--function TestClass.testFunction --classpath `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 EXIT=0
 SIGNAL=0
 VERIFICATION SUCCESSFUL

cbmc/jbmc/regression/jbmc-generics/type_erasure/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Test.class
---refine-strings --string-max-input-length 5 --string-max-length 100 --unwind 10 --function Test.verify --java-throw-runtime-exceptions
+--refine-strings --string-max-input-length 5 --string-max-length 100 --unwind 10 --function Test.verify --throw-runtime-exceptions
 ^EXIT=0$
 ^SIGNAL=0$
 assertion at file Test.java line 60 .* SUCCESS

cbmc/jbmc/regression/jbmc-strings/StringEquals/test_verify.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.check --refine-strings --string-max-length 100
+--function Test.check --refine-strings --string-max-input-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 11 .* SUCCESS$

cbmc/jbmc/regression/jbmc-strings/StringLastIndexOf/test.desc

@@ -3,4 +3,4 @@ Test.class
 --refine-strings --function Test.test --cover location --trace --json-ui
 ^EXIT=0$
 ^SIGNAL=0$
-20 of 23 covered \(87.0%\)|30 of 44 covered \(68.2%\)
+20 of 22 covered \(90.9%\)|30 of 44 covered \(68.2%\)

cbmc/jbmc/regression/jbmc-strings/char_escape/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$

cbmc/jbmc/regression/jbmc/ArithmeticException1/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$

cbmc/jbmc/regression/jbmc/ArithmeticException2/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$

cbmc/jbmc/regression/jbmc/ArithmeticException3/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$

cbmc/jbmc/regression/jbmc/ArithmeticException4/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

cbmc/jbmc/regression/jbmc/ArithmeticException5/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions --function ArithmeticExceptionTest.main
+--throw-runtime-exceptions --function ArithmeticExceptionTest.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 7 function.*: FAILURE$

cbmc/jbmc/regression/jbmc/ArithmeticException6/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$

cbmc/jbmc/regression/jbmc/ArithmeticException7/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArrayIndexOutOfBoundsExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$

cbmc/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArrayIndexOutOfBoundsExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$

cbmc/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArrayIndexOutOfBoundsExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$

cbmc/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc

@@ -1,6 +1,6 @@
 CORE
 ClassCastExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ClassCastExceptionTest.java line 8 function.*: FAILURE$

cbmc/jbmc/regression/jbmc/ClassCastException1/test.desc

@@ -1,6 +1,6 @@
 CORE
 ClassCastExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

cbmc/jbmc/regression/jbmc/ClassCastException2/test.desc

@@ -1,6 +1,6 @@
 CORE
 ClassCastExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ClassCastExceptionTest.java line 12 function.*: FAILURE$

cbmc/jbmc/regression/jbmc/ClassCastException3/test.desc

@@ -1,6 +1,6 @@
 CORE
 NegativeArraySizeExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file NegativeArraySizeExceptionTest.java line 7 function.*: FAILURE$

cbmc/jbmc/regression/jbmc/NegativeArraySizeException1/test.desc

@@ -1,6 +1,6 @@
 CORE
 NegativeArraySizeExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file NegativeArraySizeExceptionTest.java line 7 function.*: FAILURE$

cbmc/jbmc/regression/jbmc/NegativeArraySizeException2/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file Test.java line 14 function.*: FAILURE$

cbmc/jbmc/regression/jbmc/NullPointerException2/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file Test.java line 14 function.*: FAILURE$

cbmc/jbmc/regression/jbmc/NullPointerException3/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file Test.java line 12 function.*: FAILURE$

cbmc/jbmc/regression/jbmc/NullPointerException4/test.desc

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

cbmc/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---java-throw-runtime-exceptions --function test.main
+--throw-runtime-exceptions --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

cbmc/jbmc/regression/jbmc/cast_null2/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---show-symbol-table --cp ../../../src/java_bytecode/library/core-models.jar:.
+--no-lazy-methods --no-refine-strings --show-symbol-table --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^Symbol\s*\.*\: java\:\:org\.cprover\.CProver\.\<init\>\:\(\)V$

cbmc/jbmc/regression/jbmc/coreModels/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---function test.f --java-throw-runtime-exceptions
+--function test.f --throw-runtime-exceptions
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

cbmc/jbmc/regression/jbmc/exceptions21/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---java-throw-runtime-exceptions --function test.main
+--throw-runtime-exceptions --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED