Support return statements in C(!) constructors/destructors

constructors/destructors are a GCC extension, and their return type must be
void as checked earlier. As the type is then replaced by
ID_constructor/ID_destructor, and checks on the return type must consider this
case.

Author: tautschnig

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

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.