Merge pull request #729 from tautschnig/c-linking

Bug fixes to linking and C/C++ conversion

Author: kroening

regression/ansi-c/gcc_builtins6/main.c

@@ -0,0 +1,23 @@
+#include <stddef.h>
+
+struct S
+{
+  int x;
+  union {
+    int y;
+    struct S2
+    {
+      int z;
+    } s[1];
+  } u[2];
+};
+
+int main()
+{
+  int A[offsetof(struct S, u[0].y)==sizeof(int)?1:-1];
+#if defined(__GNUC__) && !defined(__clang__)
+  int B[offsetof(struct S, u->y)==sizeof(int)?1:-1];
+  int C[offsetof(struct S, u->s[0].z)==sizeof(int)?1:-1];
+#endif
+  return 0;
+}

regression/ansi-c/gcc_builtins6/test.desc

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

regression/cbmc/Linking6/main.c

@@ -0,0 +1,23 @@
+#include <stdio.h>
+
+void set();
+
+char buffer[10];
+
+void init() {
+  int i;
+  for (i = 0; i < 10; i++) {buffer[i] = 0;}
+}
+
+void print() {
+  printf("buffer = %s\n",buffer);
+}
+
+void main () {
+  init();
+  set();
+  print();
+}
+
+
+

regression/cbmc/Linking6/module.c

@@ -0,0 +1,9 @@
+#include <stdlib.h>
+
+extern char buffer[];
+
+static size_t _debug_tempBufferHead = ((size_t)(&buffer));
+
+void set() {
+  *(char *)_debug_tempBufferHead = 'a';
+}

regression/cbmc/Linking6/test.desc

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

regression/cbmc/constructor1/main.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+
+#ifdef __GNUC__
+int x;
+
+static __attribute__((constructor)) void format_init(void);
+
+static __attribute__((constructor))
+void format_init(void)
+{
+  x=42;
+  return;
+}
+#endif
+
+int main()
+{
+#ifdef __GNUC__
+  assert(x==42);
+#endif
+  return 0;
+}

regression/cbmc/constructor1/test.desc

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

regression/cbmc/hex_string1/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+#define static_assert(x) ((struct { char some[(x)?1:-1]; }*)0)
+
+int main()
+{
+  static_assert('\xe8'==(char)0xe8);
+  static_assert(sizeof("abc")==4);
+  static_assert(sizeof("\u0201")==3);
+  static_assert(sizeof("\xe8")==2);
+  static_assert(sizeof("\u0201\xe8")==4);
+
+  if("\xe8"[0]!=(char)0xe8)
+    assert(0);
+  return 0;
+}

regression/cbmc/hex_string1/test.desc

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

src/ansi-c/ansi_c_convert_type.cpp

@@ -272,6 +272,15 @@ void ansi_c_convert_typet::write(typet &type)
       throw 0;
     }
 
+    // asm blocks (cf. regression/ansi-c/asm1) - ignore the asm
+    if(other.size()==2)
+    {
+      if(other.front().id()==ID_asm && other.back().id()==ID_empty)
+        other.pop_front();
+      else if(other.front().id()==ID_empty && other.back().id()==ID_asm)
+        other.pop_back();
+    }
+
     if(other.size()!=1)
     {
       error().source_location=source_location;