C/C++ front-end: do not accept void-typed objects or members

We silently accepted these, as many cases would work fine in goto
programs. The included regression test, however, demonstrates where this
would fail an invariant during Boolean flattening (if run with
--pointer-check). GCC refuses void typed variables, and so should we.

Test originates from an SV-COMP task, reduced to this minimal example
using C-Reduce.

Author: tautschnig

regression/ansi-c/invalid_use_of_void1/main.c

@@ -0,0 +1,18 @@
+struct a
+{
+#ifdef void_member
+  void b;
+#else
+  int b;
+#endif
+};
+struct a *ae;
+void d(x)
+{
+  ae->b;
+}
+int main()
+{
+  void v;
+  d();
+}

regression/ansi-c/invalid_use_of_void1/test-non-member.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=(64|1)$
+^SIGNAL=0$
+void-typed symbol not permitted
+^CONVERSION ERROR$
+--
+Invariant check failed

regression/ansi-c/invalid_use_of_void1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+-Dvoid_member
+^EXIT=(64|1)$
+^SIGNAL=0$
+void-typed member not permitted
+^CONVERSION ERROR$
+--
+Invariant check failed

src/ansi-c/c_typecheck_base.cpp

@@ -103,6 +103,13 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol)
     symbol.pretty_name=new_name;
   }
 
+  if(!symbol.is_type && symbol.type.id() == ID_empty)
+  {
+    error().source_location = symbol.location;
+    error() << "void-typed symbol not permitted" << eom;
+    throw 0;
+  }
+
   // see if we have it already
   symbol_tablet::symbolst::const_iterator old_it=
     symbol_table.symbols.find(symbol.name);

src/ansi-c/c_typecheck_type.cpp

@@ -934,6 +934,13 @@ void c_typecheck_baset::typecheck_compound_body(
           throw 0;
         }
 
+        if(new_component.type().id() == ID_empty)
+        {
+          error().source_location = source_location;
+          error() << "void-typed member not permitted" << eom;
+          throw 0;
+        }
+
         components.push_back(new_component);
       }
     }

src/cpp/cpp_typecheck_compound_type.cpp

@@ -317,6 +317,13 @@ void cpp_typecheckt::typecheck_compound_declarator(
 
   typecheck_type(final_type);
 
+  if(final_type.id() == ID_empty)
+  {
+    error().source_location = declaration.type().source_location();
+    error() << "void-typed member not permitted" << eom;
+    throw 0;
+  }
+
   cpp_namet cpp_name;
   cpp_name.swap(declarator.name());
 

src/cpp/cpp_typecheck_declaration.cpp

@@ -148,6 +148,13 @@ void cpp_typecheckt::convert_non_template_declaration(
       declaration_type, declaration.storage_spec(),
       declaration.member_spec(), declarator);
 
+    if(!symbol.is_type && symbol.type.id() == ID_empty)
+    {
+      error().source_location = symbol.location;
+      error() << "void-typed symbol not permitted" << eom;
+      throw 0;
+    }
+
     // any template instance to remember?
     if(declaration.find(ID_C_template).is_not_nil())
     {