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