Merge pull request diffblue#391 from diffblue/CBMC_merge_2018-04-25

[SEC-367] CBMC merge 2018-04-25

Author: NathanJPhillips

cbmc/.clang-format

@@ -84,7 +84,7 @@ NamespaceIndentation: None
 PenaltyBreakString: 10000
 PointerAlignment: Right
 ReflowComments: 'false'
-SortIncludes: 'false'
+SortIncludes: 'true'
 SpaceAfterCStyleCast: 'false'
 SpaceBeforeAssignmentOperators: 'true'
 SpaceBeforeParens: Never

cbmc/regression/ansi-c/Struct_ptrmember1/main.c

@@ -0,0 +1,10 @@
+struct some_struct
+{
+  int some_field;
+} array[10];
+
+int main()
+{
+  array[0].some_field=1;
+  array->some_field=1;
+}

cbmc/regression/ansi-c/Struct_ptrmember1/test.desc

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

cbmc/regression/ansi-c/gcc_attributes11/main.c

@@ -0,0 +1,18 @@
+#ifdef __GNUC__
+// example extracted from SV-COMP's ldv-linux-3.4-simple/
+// 32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640
+static int __attribute__((__section__(".init.text")))
+__attribute__((no_instrument_function)) dp83640_init(void)
+{
+  return 0;
+}
+int init_module(void) __attribute__((alias("dp83640_init")));
+#endif
+
+int main()
+{
+#ifdef __GNUC__
+  dp83640_init();
+#endif
+  return 0;
+}

cbmc/regression/ansi-c/gcc_attributes11/test.desc

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

cbmc/regression/ansi-c/gcc_attributes9/main.c

@@ -11,11 +11,23 @@ const char* __attribute__((section("s"))) __attribute__((weak)) bar();
 volatile int __attribute__((__section__(".init.data1"))) txt_heap_base1;
 volatile int __attribute__((__section__(".init.data3"))) txt_heap_base, __attribute__((__section__(".init.data4"))) txt_heap_size;
 
+int __attribute__((__section__(".init.text"))) __attribute__((__cold__))
+__alloc_bootmem_huge_page(void *h);
+int __attribute__((__section__(".init.text"))) __attribute__((__cold__))
+alloc_bootmem_huge_page(void *h);
+int alloc_bootmem_huge_page(void *h)
+  __attribute__((weak, alias("__alloc_bootmem_huge_page")));
+int __alloc_bootmem_huge_page(void *h)
+{
+  return 1;
+}
 #endif
 
 int main()
 {
 #ifdef __GNUC__
+  int r = alloc_bootmem_huge_page(0);
+
   static int __attribute__((section(".data.unlikely"))) __warned;
   __warned=1;
   return __warned;

cbmc/regression/ansi-c/linking_conflicts1/main.c

@@ -0,0 +1,14 @@
+int bar()
+{
+  return 0;
+}
+
+int bar2()
+{
+  return 0;
+}
+
+int main()
+{
+  unsigned x = foo();
+}

cbmc/regression/ansi-c/linking_conflicts1/other.c

@@ -0,0 +1,12 @@
+void bar()
+{
+}
+
+void bar2()
+{
+}
+
+unsigned foo()
+{
+  return 0;
+}

cbmc/regression/ansi-c/linking_conflicts1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+other.c
+^EXIT=(64|1)$
+^SIGNAL=0$
+^CONVERSION ERROR$
+error: conflicting function declarations `bar'
+error: conflicting function declarations `bar2'
+--
+^warning: ignoring

cbmc/regression/cbmc-java/assertion_error_constructors/AssertionIssue.class

@@ -0,0 +1,13 @@
+public class AssertionIssue {
+
+    public static void throwAssertion() {
+        throw new AssertionError("Something went terribly wrong.", new ThrowableAssertion());
+    }
+
+    public static class ThrowableAssertion extends Throwable {
+        @Override
+        public String getMessage() {
+            return "How did we get here?";
+        }
+    }
+}

cbmc/regression/cbmc-java/assertion_error_constructors/AssertionIssue.java

@@ -0,0 +1,8 @@
+CORE
+AssertionIssue.class
+--function AssertionIssue.throwAssertion
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

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

@@ -0,0 +1,7 @@
+public class TestClass {
+  public static void f(int y) {
+    float[][] a1 = new float[y][3];
+    int j = 0;
+    a1[j][0] = 34.5f;
+  }
+}

cbmc/regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.class

@@ -0,0 +1,10 @@
+CORE
+TestClass.class
+--function TestClass.f --cover location --unwind 2
+Source GOTO statement: .*
+(^ exception: Can't convert byte_extraction|Nested exception printing not supported on Windows)
+^EXIT=6$
+--
+--
+The exception thrown in this test is the symptom of a bug; the purpose of this
+test is the validate the output of that exception

cbmc/regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.java

@@ -0,0 +1,12 @@
+public class Test {
+
+  interface factory_intf {
+    public intf getintf();
+  }
+
+  interface intf {
+    public void f();
+  }
+
+  public static void main(factory_intf i) { i.getintf().f(); }
+}

cbmc/regression/cbmc-java/dynamic-multi-dimensional-array/test.desc

@@ -0,0 +1,10 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--lazy-methods --show-goto-functions --verbosity 10 --function Test.main
+^EXIT=0$
+^SIGNAL=0$
+^CI lazy methods: elaborate java::Test\$intf\.f:\(\)V$
+Test\$intf\.f:\(\)V\(\);$
+--
+--
+This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods

cbmc/regression/cbmc-java/lazyloading_no_candidates/Test$factory_intf.class

@@ -3,6 +3,6 @@ test.class
 --show-goto-functions --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
-IF.*"java::C".*THEN GOTO
-IF.*"java::D".*THEN GOTO
+IF.*"java::B".*THEN GOTO
+IF.*"java::E".*THEN GOTO
 IF.*"java::A".*THEN GOTO

cbmc/regression/cbmc-java/lazyloading_no_candidates/Test$intf.class

@@ -0,0 +1,53 @@
+#include <stdlib.h>
+#include <assert.h>
+
+#pragma pack(1)
+struct A
+{
+  unsigned char a;
+  unsigned char b : 2;
+  unsigned char c : 2;
+  unsigned char d;
+};
+
+struct B
+{
+  unsigned char a;
+  unsigned char b : 2;
+  unsigned char c;
+  unsigned char d : 2;
+};
+
+struct C
+{
+  unsigned char a;
+  unsigned char b : 4;
+  unsigned char c : 4;
+  unsigned char d;
+};
+#pragma pack()
+
+int main(void)
+{
+  assert(sizeof(struct A) == 3);
+  struct A *p = malloc(3);
+  assert((unsigned char *)p + 2 == &(p->d));
+  p->c = 3;
+  if(p->c != 3)
+  {
+    free(p);
+  }
+  free(p);
+
+  assert(sizeof(struct B) == 4);
+  struct B *pb = malloc(4);
+  assert((unsigned char *)pb + 2 == &(pb->c));
+  free(pb);
+
+  assert(sizeof(struct C) == 3);
+  struct C *pc = malloc(3);
+  assert((unsigned char *)pc + 2 == &(pc->d));
+  free(pc);
+
+  return 0;
+}

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

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

cbmc/regression/cbmc-java/lazyloading_no_candidates/Test.java

@@ -0,0 +1 @@
+other.c

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

@@ -0,0 +1,6 @@
+int foo();
+
+int main()
+{
+  return foo();
+}

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

@@ -0,0 +1,4 @@
+int foo()
+{
+  return 1;
+}

cbmc/regression/cbmc/Bitfields3/main.c

@@ -0,0 +1,8 @@
+CORE
+main.c
+@args
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

cbmc/regression/cbmc/Bitfields3/test.desc

@@ -0,0 +1,81 @@
+
+int x;
+
+void func0()
+{
+  func0();
+}
+
+void func1()
+{
+  x = 1;
+}
+
+void func2()
+{
+  x = 2;
+  func3();
+}
+
+void func3()
+{
+  x = 3;
+}
+
+void func4(int b)
+{
+  x = 4;
+  if(b)
+  {
+    func5(0);
+  }
+}
+
+void func5(int b)
+{
+  x = 5;
+  func4(b);
+}
+
+void func6()
+{
+  x = 6;
+}
+
+void func7(int b)
+{
+  x = 7;
+  if(b)
+  {
+    func8(0);
+  }
+}
+
+void func8(int b)
+{
+  x = 8;
+  func7(b);
+}
+
+void func9()
+{
+  x = 9;
+  funca();
+}
+
+void funca()
+{
+  x = 10;
+  func9();
+}
+
+
+
+int main()
+{
+  func1();
+  func2();
+  func4(1);
+
+  return 0;
+}

cbmc/regression/goto-gcc/at_files/args

@@ -0,0 +1,20 @@
+CORE
+main.c
+--call-graph
+^EXIT=0$
+^SIGNAL=0$
+^main -> func2$
+^main -> func1$
+^main -> func4$
+^funca -> func9$
+^func9 -> funca$
+^func8 -> func7$
+^func7 -> func8$
+^__CPROVER__start -> __CPROVER_initialize$
+^__CPROVER__start -> main$
+^func2 -> func3$
+^func0 -> func0$
+^func4 -> func5$
+^func5 -> func4$
+--
+^warning: ignoring