Consistently use void_type() in the C/C++ front-end

Should we ever choose to add any annotations consistent use of the generator
function will ensure these are available.

Author: tautschnig

src/ansi-c/ansi_c_entry_point.cpp

@@ -54,8 +54,8 @@ void record_function_outputs(
   code_blockt &init_code,
   symbol_tablet &symbol_table)
 {
-  bool has_return_value=
-    to_code_type(function.type).return_type()!=empty_typet();
+  bool has_return_value =
+    to_code_type(function.type).return_type() != void_type();
 
   if(has_return_value)
   {
@@ -232,7 +232,7 @@ bool generate_ansi_c_start_function(
   call_main.add_source_location()=symbol.location;
   call_main.function().add_source_location()=symbol.location;
 
-  if(to_code_type(symbol.type).return_type()!=empty_typet())
+  if(to_code_type(symbol.type).return_type() != void_type())
   {
     auxiliary_symbolt return_symbol;
     return_symbol.mode=ID_C;
@@ -515,7 +515,7 @@ bool generate_ansi_c_start_function(
   symbolt new_symbol;
 
   new_symbol.name=goto_functionst::entry_point();
-  new_symbol.type = code_typet({}, empty_typet());
+  new_symbol.type = code_typet({}, void_type());
   new_symbol.value.swap(init_code);
   new_symbol.mode=symbol.mode;
 

src/ansi-c/c_typecheck_base.cpp

@@ -11,10 +11,11 @@ Author: Daniel Kroening, [email protected]
 
 #include "c_typecheck_base.h"
 
+#include <util/c_types.h>
+#include <util/config.h>
 #include <util/invariant.h>
-#include <util/std_types.h>
 #include <util/prefix.h>
-#include <util/config.h>
+#include <util/std_types.h>
 
 #include "expr2c.h"
 #include "type2name.h"
@@ -740,7 +741,7 @@ void c_typecheck_baset::typecheck_declaration(
 
       typecheck_spec_expr(static_cast<codet &>(contract), ID_C_spec_requires);
 
-      typet ret_type=empty_typet();
+      typet ret_type = void_type();
       if(new_symbol.type.id()==ID_code)
         ret_type=to_code_type(new_symbol.type).return_type();
       assert(parameter_map.empty());

src/ansi-c/c_typecheck_code.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "c_typecheck_base.h"
 
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/expr_initializer.h>
 
@@ -575,7 +576,7 @@ void c_typecheck_baset::typecheck_gcc_computed_goto(codet &code)
   assert(dest.operands().size()==1);
 
   typecheck_expr(dest.op0());
-  dest.type()=empty_typet();
+  dest.type() = void_type();
 }
 
 void c_typecheck_baset::typecheck_ifthenelse(code_ifthenelset &code)

src/ansi-c/c_typecheck_expr.cpp

@@ -1601,7 +1601,7 @@ void c_typecheck_baset::typecheck_expr_trinary(if_exprt &expr)
     {
       // Make it void *.
       // gcc and clang issue a warning for this.
-      expr.type()=pointer_type(empty_typet());
+      expr.type() = pointer_type(void_type());
       implicit_typecast(operands[1], expr.type());
       implicit_typecast(operands[2], expr.type());
     }

src/cpp/cpp_typecheck_expr.cpp

@@ -219,7 +219,7 @@ void cpp_typecheckt::typecheck_expr_trinary(if_exprt &expr)
       expr.type()=expr.op1().type();
     else if(expr.op1().type().id()==ID_empty &&
             expr.op2().type().id()==ID_empty)
-      expr.type()=empty_typet();
+      expr.type() = void_type();
     else
     {
       error().source_location=expr.find_source_location();
@@ -738,8 +738,7 @@ void cpp_typecheckt::typecheck_expr_address_of(exprt &expr)
 
 void cpp_typecheckt::typecheck_expr_throw(exprt &expr)
 {
-  // these are of type void
-  expr.type()=empty_typet();
+  expr.type() = void_type();
 
   assert(expr.operands().size()==1 ||
          expr.operands().empty());
@@ -1514,7 +1513,7 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
         {code_typet::parametert(ptr_arg.type()),
          code_typet::parametert(ptr_arg.type().subtype()),
          code_typet::parametert(signed_int_type())},
-        empty_typet());
+        void_type());
       symbol_exprt result(identifier, t);
       result.add_source_location() = source_location;
       expr.swap(result);
@@ -1588,7 +1587,7 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
         {code_typet::parametert(ptr_arg.type()),
          code_typet::parametert(ptr_arg.type()),
          code_typet::parametert(signed_int_type())},
-        empty_typet());
+        void_type());
       symbol_exprt result(identifier, t);
       result.add_source_location() = source_location;
       expr.swap(result);
@@ -1636,7 +1635,7 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
          code_typet::parametert(ptr_arg.type()),
          code_typet::parametert(ptr_arg.type()),
          code_typet::parametert(signed_int_type())},
-        empty_typet());
+        void_type());
       symbol_exprt result(identifier, t);
       result.add_source_location() = source_location;
       expr.swap(result);

src/cpp/cpp_typecheck_function.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "cpp_typecheck.h"
 
+#include <util/c_types.h>
+
 #include <ansi-c/c_qualifiers.h>
 
 #include "cpp_template_type.h"
@@ -139,9 +141,8 @@ void cpp_typecheckt::convert_function(symbolt &symbol)
   return_type=function_type.return_type();
 
   // constructor, destructor?
-  if(return_type.id()==ID_constructor ||
-     return_type.id()==ID_destructor)
-    return_type=empty_typet();
+  if(return_type.id() == ID_constructor || return_type.id() == ID_destructor)
+    return_type = void_type();
 
   typecheck_code(to_code(symbol.value));