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,21 @@
+struct a
+{
+#ifdef void_member
+  void b;
+#else
+  int b;
+#endif
+};
+struct a *ae;
+void d()
+{
+  ae->b;
+}
+#ifdef void_global
+void x;
+#endif
+int main()
+{
+  void v;
+  d();
+}

regression/ansi-c/invalid_use_of_void1/test-global.desc

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

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

@@ -0,0 +1,9 @@
+CORE test-c++-front-end
+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 test-c++-front-end
+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_code.cpp

@@ -448,6 +448,13 @@ void cpp_typecheckt::typecheck_decl(codet &code)
     if(is_typedef)
       continue;
 
+    if(!symbol.is_type && symbol.type.id() == ID_empty)
+    {
+      error().source_location = symbol.location;
+      error() << "void-typed symbol not permitted" << eom;
+      throw 0;
+    }
+
     code_declt decl_statement(cpp_symbol_expr(symbol));
     decl_statement.add_source_location()=symbol.location;
 

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())
     {