Merge pull request diffblue#334 from diffblue/pull-support-20180216

Merge from master, 20180216

Author: smowton

.gitignore

@@ -10,6 +10,7 @@ src/goto-analyzer/taint_driver_scripts/.idea/*
 /*.creator
 /*.creator.user
 /*.files
+/*.idea
 /*.includes
 # Eclipse
 src/.cproject
@@ -45,6 +46,7 @@ src/ansi-c/gcc_builtin_headers_tm.inc
 src/ansi-c/gcc_builtin_headers_mips.inc
 src/ansi-c/gcc_builtin_headers_power.inc
 src/ansi-c/gcc_builtin_headers_ubsan.inc
+src/java_bytecode/java_core_models.inc
 
 # regression/test files
 *.out
@@ -116,8 +118,11 @@ src/ansi-c/file_converter
 src/ansi-c/file_converter.exe
 src/ansi-c/library/converter
 src/ansi-c/library/converter.exe
+src/java_bytecode/converter
+src/java_bytecode/converter.exe
 src/util/irep_ids_convert
 src/util/irep_ids_convert.exe
+build/
 
 *.pyc
 

regression/cbmc-java/ArithmeticException6/test.desc

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

regression/cbmc-java/LocalVarTable5/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---show-goto-functions
+--show-goto-functions --function test.main
 dead anonlocal::1i
 dead anonlocal::2i
 dead anonlocal::3a

regression/cbmc-java/NondetInitValidate/Test.class renamed to regression/cbmc-java/NondetInit/Test.class

@@ -0,0 +1,16 @@
+import org.cprover.CProver;
+
+class Test {
+
+    int[] arr;
+
+    void cproverNondetInitialize() {
+        CProver.assume(arr != null && arr.length == 1);
+        // The following access should now be legal:
+        arr[0] = 100;
+    }
+
+    public static void main(Test nondetInput) {
+    }
+
+}

regression/cbmc-java/NondetInitValidate/Test.java renamed to regression/cbmc-java/NondetInit/Test.java

@@ -0,0 +1,4 @@
+CORE
+Test.class
+--function Test.main
+^VERIFICATION SUCCESSFUL$