Merge pull request #7594 from tautschnig/bugfixes/constructor

Constructor attribute is not required with forward declaration

Author: tautschnig

regression/cbmc/constructor1/main.c

@@ -1,22 +1,30 @@
 #include <assert.h>
 
 #ifdef __GNUC__
-int x;
+int x, y;
 
+// forward declaration with and without attribute is ok
 static __attribute__((constructor)) void format_init(void);
+static void other_init(void);
 
 static __attribute__((constructor))
 void format_init(void)
 {
   x=42;
   return;
 }
+
+static __attribute__((constructor)) void other_init(void)
+{
+  y = 42;
+}
 #endif
 
 int main()
 {
 #ifdef __GNUC__
   assert(x==42);
+  assert(y == 42);
 #endif
   return 0;
 }

src/ansi-c/c_typecheck_base.cpp

@@ -375,7 +375,9 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
 
     if(
       old_ct.return_type() != new_ct.return_type() &&
-      !old_ct.get_bool(ID_C_incomplete))
+      !old_ct.get_bool(ID_C_incomplete) &&
+      new_ct.return_type().id() != ID_constructor &&
+      new_ct.return_type().id() != ID_destructor)
     {
       throw invalid_source_file_exceptiont{
         "function symbol '" + id2string(new_symbol.display_name()) +