Bug fixes to linking and C/C++ conversion

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;

src/ansi-c/c_storage_spec.h

@@ -76,7 +76,13 @@ class c_storage_spect
     is_register     |=other.is_register;
     is_inline       |=other.is_inline;
     is_thread_local |=other.is_thread_local;
-    // attributes belong to the declarator, don't replace them
+    is_weak         |=other.is_weak;
+    if(alias.empty())
+      alias=other.alias;
+    if(asm_label.empty())
+      asm_label=other.asm_label;
+    if(section.empty())
+      section=other.section;
 
     return *this;
   }

src/ansi-c/c_typecheck_base.cpp

@@ -210,27 +210,6 @@ void c_typecheck_baset::typecheck_new_symbol(symbolt &symbol)
   }
   else
   {
-    if(symbol.type.id()==ID_array &&
-       to_array_type(symbol.type).size().is_nil() &&
-       !symbol.is_type)
-    {
-      // Insert a new type symbol for the array.
-      // We do this because we want a convenient way
-      // of adjusting the size of the type later on.
-
-      type_symbolt new_symbol(symbol.type);
-      new_symbol.name=id2string(symbol.name)+"$type";
-      new_symbol.base_name=id2string(symbol.base_name)+"$type";
-      new_symbol.location=symbol.location;
-      new_symbol.mode=symbol.mode;
-      new_symbol.module=symbol.module;
-
-      symbol.type=symbol_typet(new_symbol.name);
-
-      symbolt *new_sp;
-      symbol_table.move(new_symbol, new_sp);
-    }
-
     // check the initializer
     do_initializer(symbol);
   }

src/ansi-c/c_typecheck_code.cpp

@@ -901,7 +901,9 @@ void c_typecheck_baset::typecheck_return(codet &code)
 {
   if(code.operands().empty())
   {
-    if(follow(return_type).id()!=ID_empty)
+    if(follow(return_type).id()!=ID_empty &&
+       return_type.id()!=ID_constructor &&
+       return_type.id()!=ID_destructor)
     {
       // gcc doesn't actually complain, it just warns!
       // We'll put a zero here, which is dubious.

src/ansi-c/c_typecheck_expr.cpp

@@ -459,6 +459,11 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
           expr.id()==ID_gcc_asm_clobbered_register)
   {
   }
+  else if(expr.id()==ID_lshr || expr.id()==ID_ashr ||
+          expr.id()==ID_assign_lshr || expr.id()==ID_assign_ashr)
+  {
+    // already type checked
+  }
   else
   {
     err_location(expr);

src/ansi-c/gcc_builtin_headers_generic.h

@@ -86,7 +86,7 @@ void __sync_lock_release();
 // other
 int __builtin_choose_expr(_Bool, ...);
 int __builtin_classify_type();
-int __builtin_constant_p();
+int __builtin_constant_p(int);
 void __builtin_trap(void);
 void __builtin_unreachable(void);
 

src/ansi-c/literals/convert_string_literal.cpp

@@ -47,7 +47,7 @@ std::basic_string<unsigned int> convert_one_string_literal(
 
     // pad into wide string
     value.resize(utf8_value.size());
-    for(unsigned i=0; i<utf8_value.size(); i++)
+    for(std::size_t i=0; i<utf8_value.size(); i++)
       value[i]=utf8_value[i];
 
     return value;
@@ -64,16 +64,14 @@ std::basic_string<unsigned int> convert_one_string_literal(
     assert(src[0]=='"');
     assert(src[src.size()-1]=='"');
 
-    std::basic_string<unsigned int> value=
-      unescape_wide_string(std::string(src, 1, src.size()-2));
-
-    // turn into utf-8
-    std::string utf8_value=utf32_to_utf8(value);
+    std::string char_value=
+      unescape_string(std::string(src, 1, src.size()-2));
 
     // pad into wide string
-    value.resize(utf8_value.size());
-    for(unsigned i=0; i<utf8_value.size(); i++)
-      value[i]=utf8_value[i];
+    std::basic_string<unsigned int> value;
+    value.resize(char_value.size());
+    for(std::size_t i=0; i<char_value.size(); i++)
+      value[i]=char_value[i];
 
     return value;
   }
@@ -101,7 +99,7 @@ exprt convert_string_literal(const std::string &src)
 
   char wide=0;
 
-  for(unsigned i=0; i<src.size(); i++)
+  for(std::size_t i=0; i<src.size(); i++)
   {
     char ch=src[i];
 
@@ -115,27 +113,24 @@ exprt convert_string_literal(const std::string &src)
       wide=ch;
 
     // find start of sequence
-    unsigned j=i;
-    while(j<src.size() && src[j]!='"') j++;
+    std::size_t j=src.find('"', i);
+    if(j==std::string::npos)
+      throw "invalid string constant `"+src+"'";
 
     // find end of sequence, considering escaping
-    j++;
-    while(j<src.size() && src[j]!='"')
-    {
-      if(src[j]=='\\')
-        j+=2;
-      else
-        j++;
-    }
-
-    if(j<src.size())
-    {
-      std::string tmp_src=std::string(src, i, j-i+1);
-      std::basic_string<unsigned int> tmp_value=
-        convert_one_string_literal(tmp_src);
-      value.append(tmp_value);
-      i=j;
-    }
+    for(++j; j<src.size() && src[j]!='"'; ++j)
+      if(src[j]=='\\') // skip next character
+        ++j;
+
+    assert(j<=src.size());
+    if(j==src.size())
+      throw "non-terminated string constant `"+src+"'";
+
+    std::string tmp_src=std::string(src, i, j-i+1);
+    std::basic_string<unsigned int> tmp_value=
+      convert_one_string_literal(tmp_src);
+    value.append(tmp_value);
+    i=j;
   }
 
   if(wide!=0)
@@ -161,7 +156,7 @@ exprt convert_string_literal(const std::string &src)
     result.type().set(ID_size, from_integer(value.size(), index_type()));
 
     result.operands().resize(value.size());
-    for(unsigned i=0; i<value.size(); i++)
+    for(std::size_t i=0; i<value.size(); i++)
       result.operands()[i]=from_integer(value[i], subtype);
 
     return result;
@@ -172,7 +167,7 @@ exprt convert_string_literal(const std::string &src)
 
     char_value.resize(value.size());
 
-    for(unsigned i=0; i<value.size(); i++)
+    for(std::size_t i=0; i<value.size(); i++)
     {
       // Loss of data here if value[i]>255.
       // gcc issues a warning in this case.