Merge pull request diffblue#424 from diffblue/CBMC_merge_2018-05-21

Cbmc merge 2018 05 21

Author: owen-jones-diffblue

cbmc/.travis.yml

@@ -90,17 +90,6 @@ jobs:
         - COMPILER="ccache /usr/bin/g++-5"
         - EXTRA_CXXFLAGS="-D_GLIBCXX_DEBUG"
 
-    # OS X using g++
-    - stage: Test different OS/CXX/Flags
-      os: osx
-      sudo: false
-      compiler: gcc
-      cache: ccache
-      before_install:
-        - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache parallel
-        - export PATH=$PATH:/usr/local/opt/ccache/libexec
-      env: COMPILER="ccache g++"
-
     # OS X using clang++
     - stage: Test different OS/CXX/Flags
       os: osx

cbmc/regression/cbmc-java/NondetCharSequence/NondetCharSequence.class

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetCharSequence
+{
+  static void main()
+  {
+    CharSequence x = CProver.nondetWithNull();
+    assert x == null || x instanceof CharSequence;
+  }
+}

cbmc/regression/cbmc-java/NondetCharSequence/NondetCharSequence.java

@@ -0,0 +1,8 @@
+CORE
+NondetCharSequence.class
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

cbmc/regression/cbmc-java/NondetCharSequence/test.desc

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetString
+{
+  static void main()
+  {
+    String x = CProver.nondetWithNull();
+    assert x == null || x instanceof String;
+  }
+}

cbmc/regression/cbmc-java/NondetString/NondetString.class

@@ -0,0 +1,8 @@
+CORE
+NondetString.class
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

cbmc/regression/cbmc-java/NondetString/NondetString.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetStringBuffer
+{
+  static void main()
+  {
+    StringBuffer x = CProver.nondetWithNull();
+    assert x == null || x instanceof StringBuffer;
+  }
+}

cbmc/regression/cbmc-java/NondetString/test.desc

@@ -0,0 +1,8 @@
+CORE
+NondetStringBuffer.class
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring