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

cbmc/regression/cbmc-java/NondetStringBuffer/NondetStringBuffer.class

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

cbmc/regression/cbmc-java/NondetStringBuffer/NondetStringBuffer.java

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

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

@@ -3,7 +3,7 @@ NullPointer3.class
 --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-^.*Throw null: FAILURE$
+^.*Null pointer check: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

cbmc/regression/cbmc-java/NondetStringBuilder/NondetStringBuilder.class

@@ -0,0 +1,45 @@
+public class Test {
+
+  // In each of these cases a guard is repeated -- either an explicit assertion,
+  // or a guard implied by Java's semantics, e.g. that an array index is in bounds.
+  // It should be possible to violate the condition the first time, but not the second,
+  // as the program would have aborted (without --java-throw-runtime-exceptions) or a
+  // runtime exception thrown (with --java-throw-runtime-exceptions).
+
+  public static void testAssertion(boolean condition) {
+    assert(condition);
+    assert(condition);
+  }
+
+  public static void testArrayBounds(int[] array, int index) {
+    if(array == null)
+      return;
+    int got = array[index];
+    got = array[index];
+  }
+
+  public static void testClassCast(boolean unknown) {
+    A maybe_b = unknown ? new A() : new B();
+    B definitely_b = (B)maybe_b;
+    definitely_b = (B)maybe_b;
+  }
+
+  public static void testNullDeref(A maybeNull) {
+    int got = maybeNull.field;
+    got = maybeNull.field;
+  }
+
+  public static void testDivByZero(int unknown) {
+    int div = 1 / unknown;
+    div = 1 / unknown;
+  }
+
+  public static void testArrayCreation(int maybeNegative) {
+    int[] arr = new int[maybeNegative];
+    arr = new int[maybeNegative];
+  }
+
+}
+
+class A { public int field; }
+class B extends A {}

cbmc/regression/cbmc-java/NondetStringBuilder/NondetStringBuilder.java

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.testArrayBounds
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+array-index-out-of-bounds-low\.1.*: FAILURE$
+array-index-out-of-bounds-low\.2.*: SUCCESS$
+array-index-out-of-bounds-high\.1.*: FAILURE$
+array-index-out-of-bounds-high\.2.*: SUCCESS$
+--
+^warning: ignoring

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

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.testArrayCreation
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+array-create-negative-size\.1.*: FAILURE$
+array-create-negative-size\.2.*: SUCCESS$
+--
+^warning: ignoring

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

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.testAssertion
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Test\.java line 10.*: FAILURE$
+assertion at file Test\.java line 11.*: SUCCESS$
+--
+^warning: ignoring

cbmc/regression/cbmc-java/repeated_guards/A.class

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.testClassCast
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+bad-dynamic-cast\.1.*: FAILURE$
+bad-dynamic-cast\.2.*: SUCCESS$
+--
+^warning: ignoring

cbmc/regression/cbmc-java/repeated_guards/B.class

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.testDivByZero
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+integer-divide-by-zero\.1.*: FAILURE$
+integer-divide-by-zero\.2.*: SUCCESS$
+--
+^warning: ignoring

cbmc/regression/cbmc-java/repeated_guards/Test.class

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.testNullDeref
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+testNullDeref:\(LA;\)V\.null-pointer-exception\.1.*: FAILURE$
+testNullDeref:\(LA;\)V\.null-pointer-exception\.2.*: SUCCESS$
+--
+^warning: ignoring

cbmc/regression/cbmc-java/repeated_guards/Test.java

@@ -0,0 +1,76 @@
+#include <assert.h>
+
+// After a reachability slice based on the assertion in `target`, we should
+// retain both its possible callers (...may_call_target_1, ...may_call_target_2)
+// and their callees, but should be more precise concerning before_target and
+// after_target, which even though they are also called by
+// `unreachable_calls_before_target` and `unreachable_calls_after_target`, those
+// functions are not reachable.
+
+void before_target()
+{
+  const char *local = "before_target_kept";
+}
+
+void after_target()
+{
+  const char *local = "after_target_kept";
+}
+
+void target()
+{
+  const char *local = "target_kept";
+
+  before_target();
+  assert(0);
+  after_target();
+}
+
+void unreachable_calls_before_target()
+{
+  const char *local = "unreachable_calls_before_target_kept";
+  before_target();
+}
+
+void unreachable_calls_after_target()
+{
+  const char *local = "unreachable_calls_after_target_kept";
+  after_target();
+}
+
+void reachable_before_target_caller_1()
+{
+  const char *local = "reachable_before_target_caller_1_kept";
+}
+
+void reachable_after_target_caller_1()
+{
+  const char *local = "reachable_after_target_caller_1_kept";
+}
+
+void reachable_may_call_target_1()
+{
+  const char *local = "reachable_may_call_target_1_kept";
+  reachable_before_target_caller_1();
+  target();
+  reachable_after_target_caller_1();
+}
+
+void reachable_before_target_caller_2()
+{
+  const char *local = "reachable_before_target_caller_2_kept";
+}
+
+void reachable_after_target_caller_2()
+{
+  const char *local = "reachable_after_target_caller_2_kept";
+}
+
+void reachable_may_call_target_2()
+{
+  const char *local = "reachable_may_call_target_2_kept";
+  reachable_before_target_caller_2();
+  target();
+  reachable_after_target_caller_2();
+}
+

cbmc/regression/cbmc-java/repeated_guards/test_arraybounds.desc

@@ -0,0 +1,13 @@
+CORE
+test.c
+--reachability-slice-fb --show-goto-functions
+target_kept
+reachable_before_target_caller_1_kept
+reachable_after_target_caller_1_kept
+reachable_may_call_target_1_kept
+reachable_before_target_caller_2_kept
+reachable_after_target_caller_2_kept
+reachable_may_call_target_2_kept
+--
+unreachable_calls_before_target_kept
+unreachable_calls_after_target_kept

cbmc/regression/cbmc-java/repeated_guards/test_arraycreation.desc

@@ -0,0 +1,9 @@
+typedef float _Float32;
+typedef double _Float32x;
+typedef double _Float64;
+typedef long double _Float64x;
+typedef long double _Float128;
+typedef long double _Float128x;
+
+int main(int argc, char** argv) {
+}

cbmc/regression/cbmc-java/repeated_guards/test_assertion.desc

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

cbmc/regression/cbmc-java/repeated_guards/test_classcast.desc

@@ -9,10 +9,10 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$
 function \w+: replacing function pointer by 9 possible targets

cbmc/regression/cbmc-java/repeated_guards/test_divbyzero.desc

@@ -10,10 +10,10 @@ replacing function pointer by 3 possible targets
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$
 function \w+: replacing function pointer by 9 possible targets

cbmc/regression/cbmc-java/repeated_guards/test_nullderef.desc

@@ -9,10 +9,10 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$
 function \w+: replacing function pointer by 9 possible targets

cbmc/regression/cbmc/reachability-slice-interproc/test.c

@@ -9,10 +9,10 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$
 function \w+: replacing function pointer by 9 possible targets