diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
index 320ef2c90aa..40d8ad6e7c5 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1225,7 +1225,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     if(statement=="aconst_null")
     {
       assert(results.size()==1);
-      results[0]=null_pointer_exprt(java_reference_type(void_typet()));
+      results[0] = null_pointer_exprt(java_reference_type(java_void_type()));
     }
     else if(statement=="athrow")
     {
@@ -1349,7 +1349,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
         from_integer(
           std::next(i_it)->address,
           unsignedbv_typet(64));
-      results[0].type()=pointer_type(void_typet());
+      results[0].type() = pointer_type(java_void_type());
     }
     else if(statement=="ret")
     {
@@ -1981,8 +1981,8 @@ codet java_bytecode_convert_methodt::convert_monitorenterexit(
 
   // becomes a function call
   java_method_typet type(
-    {java_method_typet::parametert(java_reference_type(void_typet()))},
-    void_typet());
+    {java_method_typet::parametert(java_reference_type(java_void_type()))},
+    java_void_type());
   code_function_callt call(symbol_exprt(descriptor, type), {op[0]});
   call.add_source_location() = source_location;
   if(needed_lazy_methods && symbol_table.has_symbol(descriptor))
@@ -2725,7 +2725,7 @@ code_ifthenelset java_bytecode_convert_methodt::convert_ifnull(
   const mp_integer &number,
   const source_locationt &location) const
 {
-  const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
+  const typecast_exprt lhs(op[0], java_reference_type(java_void_type()));
   const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
 
   const method_offsett label_number = numeric_cast_v<method_offsett>(number);
@@ -2747,7 +2747,7 @@ code_ifthenelset java_bytecode_convert_methodt::convert_ifnonull(
   const mp_integer &number,
   const source_locationt &location) const
 {
-  const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
+  const typecast_exprt lhs(op[0], java_reference_type(java_void_type()));
   const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
 
   const method_offsett label_number = numeric_cast_v<method_offsett>(number);
@@ -2830,7 +2830,7 @@ code_blockt java_bytecode_convert_methodt::convert_ret(
     {
       auto address_ptr =
         from_integer(jsr_ret_targets[idx], unsignedbv_typet(64));
-      address_ptr.type() = pointer_type(void_typet());
+      address_ptr.type() = pointer_type(java_void_type());
 
       code_ifthenelset branch(equal_exprt(retvar, address_ptr), std::move(g));
 
diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp
index 725814dd850..117294b423e 100644
--- a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp
@@ -224,7 +224,7 @@ code_ifthenelset java_bytecode_instrumentt::check_class_cast(
   binary_predicate_exprt class_cast_check(
     class1, ID_java_instanceof, class2);
 
-  pointer_typet voidptr=pointer_type(empty_typet());
+  pointer_typet voidptr = pointer_type(java_void_type());
   exprt null_check_op=class1;
   if(null_check_op.type()!=voidptr)
     null_check_op.make_typecast(voidptr);
diff --git a/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp b/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp
index 02e4e7f5dd8..7a8d9632471 100644
--- a/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp
@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_bytecode_internal_additions.h"
 
 // For INFLIGHT_EXCEPTION_VARIABLE_NAME
+#include "java_types.h"
 #include "remove_exceptions.h"
 
 #include <util/std_types.h>
@@ -37,7 +38,7 @@ void java_internal_additions(symbol_table_baset &dest)
     symbolt symbol;
     symbol.base_name = CPROVER_PREFIX "malloc_object";
     symbol.name=CPROVER_PREFIX "malloc_object";
-    symbol.type=pointer_type(empty_typet());
+    symbol.type = pointer_type(java_void_type());
     symbol.mode=ID_C;
     symbol.is_lvalue=true;
     symbol.is_state_var=true;
@@ -50,7 +51,7 @@ void java_internal_additions(symbol_table_baset &dest)
     symbol.base_name = INFLIGHT_EXCEPTION_VARIABLE_BASENAME;
     symbol.name = INFLIGHT_EXCEPTION_VARIABLE_NAME;
     symbol.mode = ID_java;
-    symbol.type = pointer_type(empty_typet());
+    symbol.type = pointer_type(java_void_type());
     symbol.type.set(ID_C_no_nondet_initialization, true);
     symbol.value = null_pointer_exprt(to_pointer_type(symbol.type));
     symbol.is_file_local = false;
diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp
index 0dc74ef6333..39a834cc3da 100644
--- a/jbmc/src/java_bytecode/java_entry_point.cpp
+++ b/jbmc/src/java_bytecode/java_entry_point.cpp
@@ -38,7 +38,7 @@ static void create_initialize(symbol_table_baset &symbol_table)
   initialize.base_name=INITIALIZE_FUNCTION;
   initialize.mode=ID_java;
 
-  initialize.type = java_method_typet({}, empty_typet());
+  initialize.type = java_method_typet({}, java_void_type());
 
   code_blockt init_code;
 
@@ -225,7 +225,7 @@ static void java_static_lifetime_init(
         // Then call the init function:
         code_block.add(std::move(initializer_call));
       }
-      else if(sym.value.is_nil() && sym.type!=empty_typet())
+      else if(sym.value.is_nil() && sym.type != java_void_type())
       {
         const bool is_class_model =
           has_suffix(id2string(sym.name), "@class_model");
@@ -446,7 +446,7 @@ void java_record_outputs(
   result.reserve(parameters.size()+1);
 
   bool has_return_value =
-    to_java_method_type(function.type).return_type() != empty_typet();
+    to_java_method_type(function.type).return_type() != java_void_type();
 
   if(has_return_value)
   {
@@ -702,7 +702,7 @@ bool generate_java_start_function(
 
   // if the method return type is not void, store return value in a new variable
   // named 'return'
-  if(to_java_method_type(symbol.type).return_type() != empty_typet())
+  if(to_java_method_type(symbol.type).return_type() != java_void_type())
   {
     auxiliary_symbolt return_symbol;
     return_symbol.mode=ID_java;
@@ -720,7 +720,7 @@ bool generate_java_start_function(
   exc_symbol.mode=ID_java;
   exc_symbol.name=JAVA_ENTRY_POINT_EXCEPTION_SYMBOL;
   exc_symbol.base_name=exc_symbol.name;
-  exc_symbol.type=java_reference_type(empty_typet());
+  exc_symbol.type = java_reference_type(java_void_type());
   symbol_table.add(exc_symbol);
 
   // Zero-initialise the top-level exception catch variable:
@@ -792,7 +792,7 @@ bool generate_java_start_function(
   symbolt new_symbol;
 
   new_symbol.name=goto_functionst::entry_point();
-  new_symbol.type = java_method_typet({}, empty_typet());
+  new_symbol.type = java_method_typet({}, java_void_type());
   new_symbol.value.swap(init_code);
   new_symbol.mode=ID_java;
 
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index 0c8d2b7cf0b..9f9a52efec7 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -592,7 +592,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
 
   // If this is a void* we *must* initialise with null:
   // (This can currently happen for some cases of #exception_value)
-  bool must_be_null = subtype == empty_typet();
+  bool must_be_null = subtype == java_void_type();
 
   // If we may be about to initialize a non-null enum type, always run the
   // clinit_wrapper of its class first.
diff --git a/jbmc/src/java_bytecode/java_pointer_casts.cpp b/jbmc/src/java_bytecode/java_pointer_casts.cpp
index 7a89e4367ed..cbc8c4f4cf0 100644
--- a/jbmc/src/java_bytecode/java_pointer_casts.cpp
+++ b/jbmc/src/java_bytecode/java_pointer_casts.cpp
@@ -15,6 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_types.h>
 #include <util/namespace.h>
 
+#include "java_types.h"
+
 /// dereference pointer expression
 /// \return dereferenced pointer
 static exprt clean_deref(const exprt &ptr)
@@ -94,8 +96,9 @@ exprt make_clean_pointer_cast(
   if(ptr.type()==target_type)
     return ptr;
 
-  if(ptr.type().subtype()==empty_typet() ||
-     target_type.subtype()==empty_typet())
+  if(
+    ptr.type().subtype() == java_void_type() ||
+    target_type.subtype() == java_void_type())
     return typecast_exprt(ptr, target_type);
 
   const typet &target_base=ns.follow(target_type.subtype());
@@ -106,7 +109,7 @@ exprt make_clean_pointer_cast(
     assert(
       bare_ptr.type().id()==ID_pointer &&
       "Non-pointer in make_clean_pointer_cast?");
-    if(bare_ptr.type().subtype()==empty_typet())
+    if(bare_ptr.type().subtype() == java_void_type())
       bare_ptr=bare_ptr.op0();
   }
 
diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp
index c0234064361..d412c76d570 100644
--- a/jbmc/src/java_bytecode/java_static_initializers.cpp
+++ b/jbmc/src/java_bytecode/java_static_initializers.cpp
@@ -352,7 +352,7 @@ static void create_clinit_wrapper_symbols(
 
   // Create symbol for the "clinit_wrapper"
   symbolt wrapper_method_symbol;
-  const java_method_typet wrapper_method_type({}, void_typet());
+  const java_method_typet wrapper_method_type({}, java_void_type());
   wrapper_method_symbol.name = clinit_wrapper_name(class_name);
   wrapper_method_symbol.pretty_name = wrapper_method_symbol.name;
   wrapper_method_symbol.base_name = "clinit_wrapper";
@@ -790,7 +790,7 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols(
       "a class cannot be both incomplete, and so have stub static fields, and "
       "also define a static initializer");
 
-    const java_method_typet thunk_type({}, void_typet());
+    const java_method_typet thunk_type({}, java_void_type());
 
     symbolt static_init_symbol;
     static_init_symbol.name = static_init_name;
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index ef720d8e3ce..9cd208b9860 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -1291,7 +1291,7 @@ dereference_exprt java_string_library_preprocesst::get_object_at_index(
   std::size_t index)
 {
   dereference_exprt deref_objs(argv, argv.type().subtype());
-  pointer_typet empty_pointer=pointer_type(empty_typet());
+  pointer_typet empty_pointer = pointer_type(java_void_type());
   pointer_typet pointer_of_pointer=pointer_type(empty_pointer);
   member_exprt data_member(deref_objs, "data", pointer_of_pointer);
   plus_exprt data_pointer_plus_index(
diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp
index e02142283e2..9937d4d3905 100644
--- a/jbmc/src/java_bytecode/java_types.cpp
+++ b/jbmc/src/java_bytecode/java_types.cpp
@@ -35,9 +35,9 @@ signedbv_typet java_int_type()
   return result;
 }
 
-void_typet java_void_type()
+empty_typet java_void_type()
 {
-  static const auto result = void_typet();
+  static const auto result = empty_typet();
   return result;
 }
 
@@ -209,7 +209,8 @@ typet java_type_from_char(char t)
   case 'f': return java_float_type();
   case 'd': return java_double_type();
   case 'z': return java_boolean_type();
-  case 'a': return java_reference_type(void_typet());
+  case 'a':
+    return java_reference_type(java_void_type());
   default:
     UNREACHABLE;
   }
diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h
index 252ad568561..c0b0eb75b86 100644
--- a/jbmc/src/java_bytecode/java_types.h
+++ b/jbmc/src/java_bytecode/java_types.h
@@ -368,7 +368,7 @@ unsignedbv_typet java_char_type();
 floatbv_typet java_float_type();
 floatbv_typet java_double_type();
 c_bool_typet java_boolean_type();
-void_typet java_void_type();
+empty_typet java_void_type();
 reference_typet java_reference_type(const typet &subtype);
 reference_typet java_lang_object_type();
 struct_tag_typet java_classname(const std::string &);
diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp
index 94a0b873533..b078ca1c939 100644
--- a/jbmc/src/java_bytecode/remove_exceptions.cpp
+++ b/jbmc/src/java_bytecode/remove_exceptions.cpp
@@ -30,6 +30,8 @@ Date:   December 2016
 
 #include <analyses/uncaught_exceptions_analysis.h>
 
+#include "java_types.h"
+
 /// Lowers high-level exception descriptions into low-level operations suitable
 /// for symex and other analyses that don't understand the THROW or CATCH GOTO
 /// instructions.
@@ -228,7 +230,7 @@ void remove_exceptionst::instrument_exception_handler(
     const symbol_exprt thrown_global_symbol=
       get_inflight_exception_global();
     // next we reset the exceptional return to NULL
-    null_pointer_exprt null_voidptr((pointer_type(empty_typet())));
+    null_pointer_exprt null_voidptr((pointer_type(java_void_type())));
 
     // add the assignment @inflight_exception = NULL
     goto_programt::targett t_null=goto_program.insert_after(instr_it);
@@ -443,7 +445,7 @@ bool remove_exceptionst::instrument_function_call(
   {
     equal_exprt no_exception_currently_in_flight(
       get_inflight_exception_global(),
-      null_pointer_exprt(pointer_type(empty_typet())));
+      null_pointer_exprt(pointer_type(java_void_type())));
 
     if(symbol_table.lookup_ref(callee_id).type.get_bool(ID_C_must_not_throw))
     {
diff --git a/jbmc/src/java_bytecode/simple_method_stubbing.cpp b/jbmc/src/java_bytecode/simple_method_stubbing.cpp
index 96bda1db533..4c75878c20c 100644
--- a/jbmc/src/java_bytecode/simple_method_stubbing.cpp
+++ b/jbmc/src/java_bytecode/simple_method_stubbing.cpp
@@ -187,7 +187,7 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
   else
   {
     const typet &required_return_type = required_type.return_type();
-    if(required_return_type != empty_typet())
+    if(required_return_type != java_void_type())
     {
       symbolt &to_return_symbol = get_fresh_aux_symbol(
         required_return_type,
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp
index d3a8f56444b..ae388857585 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp
@@ -139,7 +139,7 @@ SCENARIO(
         const auto &id =
           to_symbol_expr(element_value_pair.value).get_identifier();
         const auto &java_type = java_type_from_string(id2string(id));
-        REQUIRE(*java_type == void_type());
+        REQUIRE(*java_type == java_void_type());
       }
     }
     WHEN("Parsing an annotation with an array field.")
diff --git a/regression/invariants/driver.cpp b/regression/invariants/driver.cpp
index b19b443576b..2e69451c7d3 100644
--- a/regression/invariants/driver.cpp
+++ b/regression/invariants/driver.cpp
@@ -118,7 +118,7 @@ int main(int argc, char** argv)
   else if(arg=="data-invariant-string")
     DATA_INVARIANT(false, "Test invariant failure");
   else if(arg=="irep")
-    INVARIANT_WITH_IREP(false, "error with irep", pointer_type(void_typet()));
+    INVARIANT_WITH_IREP(false, "error with irep", pointer_type(empty_typet()));
   else if(arg == "invariant-diagnostics")
     INVARIANT_WITH_DIAGNOSTICS(
       false,
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
index 02033a2e39b..fbef18a84e7 100644
--- a/src/ansi-c/ansi_c_entry_point.cpp
+++ b/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;
 
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index 20505c16273..0337772d696 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/src/ansi-c/c_typecheck_base.cpp
@@ -11,10 +11,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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());
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index e059de7fc94..adad675857f 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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)
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 3f363ea9cd7..5d3ca4a2015 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/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());
     }
diff --git a/src/ansi-c/parser_static.inc b/src/ansi-c/parser_static.inc
index 41b604a1929..d4590859c31 100644
--- a/src/ansi-c/parser_static.inc
+++ b/src/ansi-c/parser_static.inc
@@ -82,7 +82,6 @@ Function: statement
 static void statement(YYSTYPE &expr, const irep_idt &id)
 {
   set(expr, ID_code);
-  stack(expr).type().id(ID_code);
   stack(expr).set(ID_statement, id);
 }
 
diff --git a/src/assembler/remove_asm.cpp b/src/assembler/remove_asm.cpp
index e98457eeddb..e944149ebc2 100644
--- a/src/assembler/remove_asm.cpp
+++ b/src/assembler/remove_asm.cpp
@@ -78,7 +78,7 @@ void remove_asmt::gcc_asm_function_call(
 
   code_function_callt::argumentst arguments;
 
-  const typet void_pointer = pointer_type(void_typet());
+  const typet void_pointer = pointer_type(empty_typet());
 
   // outputs
   forall_operands(it, code.op1())
@@ -100,7 +100,7 @@ void remove_asmt::gcc_asm_function_call(
     }
   }
 
-  code_typet fkt_type({}, void_typet());
+  code_typet fkt_type({}, empty_typet());
   fkt_type.make_ellipsis();
 
   symbol_exprt fkt(function_identifier, fkt_type);
@@ -147,9 +147,9 @@ void remove_asmt::msc_asm_function_call(
 {
   irep_idt function_identifier = function_base_name;
 
-  const typet void_pointer = pointer_type(void_typet());
+  const typet void_pointer = pointer_type(empty_typet());
 
-  code_typet fkt_type({}, void_typet());
+  code_typet fkt_type({}, empty_typet());
   fkt_type.make_ellipsis();
 
   symbol_exprt fkt(function_identifier, fkt_type);
diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp
index ae56300115d..d538cac5269 100644
--- a/src/cpp/cpp_typecheck_code.cpp
+++ b/src/cpp/cpp_typecheck_code.cpp
@@ -25,12 +25,12 @@ void cpp_typecheckt::typecheck_code(codet &code)
 
   if(statement==ID_try_catch)
   {
-    code.type() = code_typet({}, empty_typet());
+    code.type() = empty_typet();
     typecheck_try_catch(code);
   }
   else if(statement==ID_member_initializer)
   {
-    code.type() = code_typet({}, empty_typet());
+    code.type() = empty_typet();
     typecheck_member_initializer(code);
   }
   else if(statement==ID_msc_if_exists ||
diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp
index 54e3ebbed46..e17e2e783e5 100644
--- a/src/cpp/cpp_typecheck_constructor.cpp
+++ b/src/cpp/cpp_typecheck_constructor.cpp
@@ -349,12 +349,7 @@ void cpp_typecheckt::default_assignop_value(
   source_locationt source_location=declarator.source_location();
   declarator.make_nil();
 
-  declarator.value().add_source_location()=source_location;
-  declarator.value().id(ID_code);
-  declarator.value().set(ID_statement, ID_block);
-  declarator.value().type() = code_typet({}, empty_typet());
-
-  exprt &block=declarator.value();
+  code_blockt block;
 
   std::string arg_name("ref");
 
@@ -405,12 +400,11 @@ void cpp_typecheckt::default_assignop_value(
   }
 
   // Finally we add the return statement
-  block.operands().push_back(exprt(ID_code));
-  exprt &ret_code=declarator.value().operands().back();
-  ret_code.operands().push_back(exprt(ID_dereference));
-  ret_code.op0().operands().push_back(exprt("cpp-this"));
-  ret_code.set(ID_statement, ID_return);
-  ret_code.type() = code_typet({}, empty_typet());
+  block.add(
+    code_returnt(dereference_exprt(exprt("cpp-this"), uninitialized_typet())));
+
+  declarator.value() = std::move(block);
+  declarator.value().add_source_location() = source_location;
 }
 
 /// Check a constructor initialization-list. An initializer has to be a data
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
index 3bf0da62939..a7d0829bd19 100644
--- a/src/cpp/cpp_typecheck_expr.cpp
+++ b/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);
@@ -1964,8 +1963,8 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
   else if(expr.function().id() == ID_cpp_dummy_destructor)
   {
     // these don't do anything, e.g., (char*)->~char()
-    expr.set(ID_statement, ID_skip);
-    expr.type()=empty_typet();
+    typecast_exprt no_op(from_integer(0, signed_int_type()), void_type());
+    expr.swap(no_op);
     return;
   }
 
diff --git a/src/cpp/cpp_typecheck_function.cpp b/src/cpp/cpp_typecheck_function.cpp
index 206cdd08c86..b23f803a15b 100644
--- a/src/cpp/cpp_typecheck_function.cpp
+++ b/src/cpp/cpp_typecheck_function.cpp
@@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #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));
 
diff --git a/src/goto-instrument/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp
index 244f77decc5..3559caae777 100644
--- a/src/goto-instrument/generate_function_bodies.cpp
+++ b/src/goto-instrument/generate_function_bodies.cpp
@@ -266,7 +266,7 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
       function.body.destructive_append(dest);
     }
 
-    if(function.type.return_type() != void_typet())
+    if(function.type.return_type() != empty_typet())
     {
       typet type(function.type.return_type());
       type.remove(ID_C_constant);
diff --git a/src/jsil/parser.y b/src/jsil/parser.y
index 7461e378873..12c9385d8fa 100644
--- a/src/jsil/parser.y
+++ b/src/jsil/parser.y
@@ -198,9 +198,8 @@ statements_opt: /* empty */
 
 statements: statement
           {
-            newstack($$).id(ID_code);
-            to_code(stack($$)).set_statement(ID_block);
-            stack($$).add_to_operands(std::move(stack($1)));
+            code_blockt b({static_cast<codet &>(stack($1))});
+            newstack($$).swap(b);
           }
           | statements statement
           {
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index a8cbd48afa5..9f47c211ab9 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -86,7 +86,7 @@ bv_pointerst::bv_pointerst(
   pointer_logic(_ns)
 {
   object_bits=config.bv_encoding.object_bits;
-  std::size_t pointer_width=boolbv_width(pointer_type(void_type()));
+  std::size_t pointer_width = boolbv_width(pointer_type(empty_typet()));
   offset_bits=pointer_width-object_bits;
   bits=pointer_width;
 }
diff --git a/src/util/c_types.cpp b/src/util/c_types.cpp
index 11fea1ecc01..bd0a6b268a0 100644
--- a/src/util/c_types.cpp
+++ b/src/util/c_types.cpp
@@ -250,9 +250,10 @@ reference_typet reference_type(const typet &subtype)
   return reference_typet(subtype, config.ansi_c.pointer_width);
 }
 
-typet void_type()
+empty_typet void_type()
 {
-  return empty_typet();
+  static const auto result = empty_typet();
+  return result;
 }
 
 std::string c_type_as_string(const irep_idt &c_type)
diff --git a/src/util/c_types.h b/src/util/c_types.h
index 9e97d19f266..998066f60fe 100644
--- a/src/util/c_types.h
+++ b/src/util/c_types.h
@@ -36,7 +36,7 @@ unsignedbv_typet size_type();
 signedbv_typet signed_size_type();
 signedbv_typet pointer_diff_type();
 pointer_typet pointer_type(const typet &);
-typet void_type();
+empty_typet void_type();
 
 // This is for Java and C++
 reference_typet reference_type(const typet &);
diff --git a/src/util/std_types.h b/src/util/std_types.h
index 5e2bdfdaf9e..1fe6c0c8f4a 100644
--- a/src/util/std_types.h
+++ b/src/util/std_types.h
@@ -54,11 +54,6 @@ class empty_typet:public typet
   }
 };
 
-/// The void type, the same as \ref empty_typet.
-class void_typet:public empty_typet
-{
-};
-
 /// A reference into the symbol table
 class symbol_typet:public typet
 {
diff --git a/unit/analyses/ai/ai.cpp b/unit/analyses/ai/ai.cpp
index 4148c646846..2ef0266a834 100644
--- a/unit/analyses/ai/ai.cpp
+++ b/unit/analyses/ai/ai.cpp
@@ -156,7 +156,7 @@ SCENARIO(
   symbolt g;
   g.name = "g";
   g.mode = ID_C;
-  g.type = code_typet({}, void_typet());
+  g.type = code_typet({}, empty_typet());
   g.value = code_assignt(gy.symbol_expr(), from_integer(0, signed_int_type()));
 
   // h:
@@ -169,7 +169,7 @@ SCENARIO(
   symbolt h;
   h.name = "h";
   h.mode = ID_C;
-  h.type = code_typet({}, void_typet());
+  h.type = code_typet({}, empty_typet());
   h.value = code_assignt(hy.symbol_expr(), from_integer(0, signed_int_type()));
 
   goto_model.symbol_table.add(g);
@@ -226,7 +226,7 @@ SCENARIO(
   symbolt f;
   f.name = "f";
   f.mode = ID_C;
-  f.type = code_typet({}, void_typet());
+  f.type = code_typet({}, empty_typet());
   f.value = f_body;
 
   goto_model.symbol_table.add(f);
@@ -236,7 +236,7 @@ SCENARIO(
   symbolt start;
   start.name = goto_functionst::entry_point();
   start.mode = ID_C;
-  start.type = code_typet({}, void_typet());
+  start.type = code_typet({}, empty_typet());
   start.value = make_void_call(f.symbol_expr());
 
   goto_model.symbol_table.add(start);
diff --git a/unit/analyses/constant_propagator.cpp b/unit/analyses/constant_propagator.cpp
index 88f36659bab..117d6b599ac 100644
--- a/unit/analyses/constant_propagator.cpp
+++ b/unit/analyses/constant_propagator.cpp
@@ -54,7 +54,7 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]")
 
     symbolt main_function_symbol;
     main_function_symbol.name = "main";
-    main_function_symbol.type = code_typet({}, void_typet());
+    main_function_symbol.type = code_typet({}, empty_typet());
     main_function_symbol.value = code;
     main_function_symbol.mode = ID_C;
 
@@ -146,7 +146,7 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]")
 
     symbolt main_function_symbol;
     main_function_symbol.name = "main";
-    main_function_symbol.type = code_typet({}, void_typet());
+    main_function_symbol.type = code_typet({}, empty_typet());
     main_function_symbol.value = code;
     main_function_symbol.mode = ID_C;
 
@@ -295,7 +295,7 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]")
 
     symbolt main_function_symbol;
     main_function_symbol.name = "main";
-    main_function_symbol.type = code_typet({}, void_typet());
+    main_function_symbol.type = code_typet({}, empty_typet());
     main_function_symbol.value = program;
     main_function_symbol.mode = ID_C;