diff --git a/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp b/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp
index e895d7d7d7a..4477488b6c1 100644
--- a/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp
+++ b/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp
@@ -75,7 +75,7 @@ codet create_array_with_type_body(
   code_blockt code_block;
 
   // Declare new_array temporary:
-  code_block.add(code_declt(new_array_symbol_expr));
+  code_block.add(code_frontend_declt(new_array_symbol_expr));
 
   // new_array = new Object[length];
   side_effect_exprt new_array_expr{
@@ -105,7 +105,7 @@ codet create_array_with_type_body(
     new_array_element_classid, old_array_element_classid));
 
   // return new_array
-  code_block.add(code_returnt(new_array_symbol_expr));
+  code_block.add(code_frontend_returnt(new_array_symbol_expr));
 
   return std::move(code_block);
 }
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
index 0a215a111c5..c68372823e8 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1361,7 +1361,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
     else if(bytecode == BC_return)
     {
       PRECONDITION(op.empty() && results.empty());
-      c=code_returnt();
+      c = code_frontend_returnt();
     }
     else if(bytecode == patternt("?return"))
     {
@@ -1370,7 +1370,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
       PRECONDITION(op.size() == 1 && results.empty());
       const exprt r =
         typecast_exprt::conditional_cast(op[0], method_return_type);
-      c=code_returnt(r);
+      c = code_frontend_returnt(r);
     }
     else if(bytecode == patternt("?astore"))
     {
diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp
index 2bb7d17b206..5e97df5a83f 100644
--- a/jbmc/src/java_bytecode/java_static_initializers.cpp
+++ b/jbmc/src/java_bytecode/java_static_initializers.cpp
@@ -590,7 +590,7 @@ code_blockt get_thread_safe_clinit_wrapper_body(
       gen_clinit_eqexpr(
         clinit_thread_local_state_sym.symbol_expr(),
         clinit_statest::INIT_COMPLETE),
-      code_returnt());
+      code_frontend_returnt());
     function_body.add(std::move(conditional));
   }
 
@@ -651,7 +651,8 @@ code_blockt get_thread_safe_clinit_wrapper_body(
 
   // if(init_complete) return;
   {
-    code_ifthenelset conditional(init_complete.symbol_expr(), code_returnt());
+    code_ifthenelset conditional(
+      init_complete.symbol_expr(), code_frontend_returnt());
     function_body.add(std::move(conditional));
   }
 
@@ -696,7 +697,7 @@ code_blockt get_thread_safe_clinit_wrapper_body(
       gen_clinit_assign(
         clinit_state_sym.symbol_expr(), clinit_statest::INIT_COMPLETE));
     function_body.add(atomic_end);
-    function_body.add(code_returnt());
+    function_body.add(code_frontend_returnt());
   }
 
   return function_body;
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
index a79aedae124..405940c81fe 100644
--- a/src/ansi-c/c_typecheck_base.h
+++ b/src/ansi-c/c_typecheck_base.h
@@ -139,7 +139,7 @@ class c_typecheck_baset:
   virtual void typecheck_gcc_computed_goto(codet &code);
   virtual void typecheck_gcc_switch_case_range(code_gcc_switch_case_ranget &);
   virtual void typecheck_gcc_local_label(codet &code);
-  virtual void typecheck_return(code_returnt &code);
+  virtual void typecheck_return(code_frontend_returnt &);
   virtual void typecheck_switch(codet &code);
   virtual void typecheck_while(code_whilet &code);
   virtual void typecheck_dowhile(code_dowhilet &code);
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index ea180d4c5d3..7e46443a18f 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -68,7 +68,7 @@ void c_typecheck_baset::typecheck_code(codet &code)
   else if(statement==ID_continue)
     typecheck_continue(code);
   else if(statement==ID_return)
-    typecheck_return(to_code_return(code));
+    typecheck_return(to_code_frontend_return(code));
   else if(statement==ID_decl)
     typecheck_decl(code);
   else if(statement==ID_assign)
@@ -643,7 +643,7 @@ void c_typecheck_baset::typecheck_start_thread(codet &code)
   typecheck_code(to_code(code.op0()));
 }
 
-void c_typecheck_baset::typecheck_return(code_returnt &code)
+void c_typecheck_baset::typecheck_return(code_frontend_returnt &code)
 {
   if(code.has_return_value())
   {
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 08224545c6a..ec245bfae89 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -2680,7 +2680,7 @@ std::string expr2ct::convert_code_return(
   std::string dest=indent_str(indent);
   dest+="return";
 
-  if(to_code_return(src).has_return_value())
+  if(to_code_frontend_return(src).has_return_value())
     dest+=" "+convert(src.op0());
 
   dest+=';';
diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp
index 700bc221c2c..e7c40d9d4b4 100644
--- a/src/cpp/cpp_typecheck_compound_type.cpp
+++ b/src/cpp/cpp_typecheck_compound_type.cpp
@@ -688,8 +688,8 @@ void cpp_typecheckt::typecheck_compound_declarator(
         {
           expr_call.type()=to_code_type(component.type()).return_type();
 
-          func_symb.value = code_blockt{
-            {code_returnt(already_typechecked_exprt{std::move(expr_call)})}};
+          func_symb.value = code_blockt{{code_frontend_returnt(
+            already_typechecked_exprt{std::move(expr_call)})}};
         }
         else
         {
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
index 7220976c641..0c2d629e00d 100644
--- a/src/cpp/parse.cpp
+++ b/src/cpp/parse.cpp
@@ -7350,7 +7350,7 @@ optionalt<codet> Parser::rStatement()
 
     lex.get_token(tk1);
 
-    code_returnt statement;
+    code_frontend_returnt statement;
     set_location(statement, tk1);
 
     if(lex.LookAhead(0)==';')
diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp
index f9f75fc12ad..ce16ab6c6cf 100644
--- a/src/goto-harness/recursive_initialization.cpp
+++ b/src/goto-harness/recursive_initialization.cpp
@@ -239,7 +239,7 @@ code_blockt build_null_pointer(const symbol_exprt &result_symbol)
   const null_pointer_exprt nullptr_expr{to_pointer_type(type_to_construct)};
   const code_assignt assign_null{dereference_exprt{result_symbol},
                                  nullptr_expr};
-  return code_blockt{{assign_null, code_returnt{}}};
+  return code_blockt{{assign_null, code_frontend_returnt{}}};
 }
 
 code_blockt recursive_initializationt::build_constructor_body(
@@ -688,7 +688,7 @@ code_blockt recursive_initializationt::build_pointer_constructor(
 
   null_pointer_exprt nullptr_expr{pointer_type(type.subtype())};
   const code_assignt assign_null{dereference_exprt{result}, nullptr_expr};
-  code_blockt null_and_return{{assign_null, code_returnt{}}};
+  code_blockt null_and_return{{assign_null, code_frontend_returnt{}}};
   body.add(code_ifthenelset{conjunction(should_not_recurse), null_and_return});
 
   const auto should_recurse_nondet =
@@ -1034,7 +1034,7 @@ code_blockt recursive_initializationt::build_function_pointer_constructor(
       auto const condition = equal_exprt{
         function_pointer_selector,
         from_integer(function_pointer_index, function_pointer_selector.type())};
-      auto const then = code_blockt{{assign, code_returnt{}}};
+      auto const then = code_blockt{{assign, code_frontend_returnt{}}};
       body.add(code_ifthenelset{condition, then});
     }
     else
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index b5e89c0063c..ce88275457b 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -1074,7 +1074,7 @@ void code_contractst::add_contract_check(
   replace_symbolt common_replace;
 
   // decl ret
-  code_returnt return_stmt;
+  optionalt<code_returnt> return_stmt;
   if(code_type.return_type() != empty_typet())
   {
     symbol_exprt r = new_tmp_symbol(
@@ -1178,7 +1178,8 @@ void code_contractst::add_contract_check(
 
   if(code_type.return_type() != empty_typet())
   {
-    check.add(goto_programt::make_return(return_stmt, skip->source_location()));
+    check.add(
+      goto_programt::make_return(return_stmt.value(), skip->source_location()));
   }
 
   // prepend the new code to dest
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index e3b13f66a2d..3ff25835a38 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -470,7 +470,7 @@ void goto_convertt::convert(
   else if(statement==ID_break)
     convert_break(to_code_break(code), dest, mode);
   else if(statement==ID_return)
-    convert_return(to_code_return(code), dest, mode);
+    convert_return(to_code_frontend_return(code), dest, mode);
   else if(statement==ID_continue)
     convert_continue(to_code_continue(code), dest, mode);
   else if(statement==ID_goto)
@@ -1258,7 +1258,7 @@ void goto_convertt::convert_break(
 }
 
 void goto_convertt::convert_return(
-  const code_returnt &code,
+  const code_frontend_returnt &code,
   goto_programt &dest,
   const irep_idt &mode)
 {
@@ -1273,7 +1273,7 @@ void goto_convertt::convert_return(
     "return takes none or one operand",
     code.find_source_location());
 
-  code_returnt new_code(code);
+  code_frontend_returnt new_code(code);
 
   if(new_code.has_return_value())
   {
@@ -1297,7 +1297,8 @@ void goto_convertt::convert_return(
       new_code.find_source_location());
 
     // Now add a return node to set the return value.
-    dest.add(goto_programt::make_return(new_code, new_code.source_location()));
+    dest.add(goto_programt::make_return(
+      to_code_return(new_code), new_code.source_location()));
   }
   else
   {
diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h
index 54050055f2e..fc3554c5fb1 100644
--- a/src/goto-programs/goto_convert_class.h
+++ b/src/goto-programs/goto_convert_class.h
@@ -267,7 +267,7 @@ class goto_convertt:public messaget
     goto_programt &dest,
     const irep_idt &mode);
   void convert_return(
-    const code_returnt &code,
+    const code_frontend_returnt &,
     goto_programt &dest,
     const irep_idt &mode);
   void convert_continue(
diff --git a/src/jsil/jsil_parse_tree.cpp b/src/jsil/jsil_parse_tree.cpp
index 7d97b72651d..99f0bb68934 100644
--- a/src/jsil/jsil_parse_tree.cpp
+++ b/src/jsil/jsil_parse_tree.cpp
@@ -66,7 +66,7 @@ void jsil_declarationt::to_symbol(symbolt &symbol) const
       static_cast<const codet&>(find(ID_value))));
 
   irept returns(find(ID_return));
-  code_returnt r(symbol_exprt::typeless(returns.get(ID_value)));
+  code_frontend_returnt r(symbol_exprt::typeless(returns.get(ID_value)));
 
   irept throws(find(ID_throw));
   side_effect_expr_throwt t(
diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp
index 5d12ecbc6ac..997c939bd5f 100644
--- a/src/jsil/jsil_typecheck.cpp
+++ b/src/jsil/jsil_typecheck.cpp
@@ -637,7 +637,7 @@ void jsil_typecheckt::typecheck_code(codet &code)
   if(statement==ID_function_call)
     typecheck_function_call(to_code_function_call(code));
   else if(statement==ID_return)
-    typecheck_return(to_code_return(code));
+    typecheck_return(to_code_frontend_return(code));
   else if(statement==ID_expression)
   {
     if(code.operands().size()!=1)
@@ -678,7 +678,7 @@ void jsil_typecheckt::typecheck_code(codet &code)
   }
 }
 
-void jsil_typecheckt::typecheck_return(code_returnt &code)
+void jsil_typecheckt::typecheck_return(code_frontend_returnt &code)
 {
   if(code.has_return_value())
     typecheck_expr(code.return_value());
diff --git a/src/jsil/jsil_typecheck.h b/src/jsil/jsil_typecheck.h
index 4d66240758a..64b2e362b5a 100644
--- a/src/jsil/jsil_typecheck.h
+++ b/src/jsil/jsil_typecheck.h
@@ -20,7 +20,7 @@ Author: Michael Tautschnig, tautschn@amazon.com
 class code_assignt;
 class code_function_callt;
 class code_ifthenelset;
-class code_returnt;
+class code_frontend_returnt;
 class code_try_catcht;
 class codet;
 class message_handlert;
@@ -89,7 +89,7 @@ class jsil_typecheckt:public typecheckt
   void typecheck_expr_main(exprt &expr);
   void typecheck_code(codet &code);
   void typecheck_function_call(code_function_callt &function_call);
-  void typecheck_return(code_returnt &code);
+  void typecheck_return(code_frontend_returnt &);
   void typecheck_block(codet &code);
   void typecheck_ifthenelse(code_ifthenelset &code);
   void typecheck_assign(code_assignt &code);
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 6554aa9132e..1767fde029c 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -1582,12 +1582,9 @@ void value_sett::apply_code_rec(
   {
     const code_returnt &code_return = to_code_return(code);
     // this is turned into an assignment
-    if(code_return.has_return_value())
-    {
-      symbol_exprt lhs(
-        "value_set::return_value", code_return.return_value().type());
-      assign(lhs, code_return.return_value(), ns, false, false);
-    }
+    symbol_exprt lhs(
+      "value_set::return_value", code_return.return_value().type());
+    assign(lhs, code_return.return_value(), ns, false, false);
   }
   else if(statement==ID_array_set)
   {
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index 73e406a5cc5..d4d960a5a6b 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -1378,12 +1378,9 @@ void value_set_fit::apply_code(const codet &code, const namespacet &ns)
   {
     const code_returnt &code_return = to_code_return(code);
     // this is turned into an assignment
-    if(code_return.has_return_value())
-    {
-      std::string rvs="value_set::return_value"+std::to_string(from_function);
-      symbol_exprt lhs(rvs, code_return.return_value().type());
-      assign(lhs, code_return.return_value(), ns);
-    }
+    std::string rvs = "value_set::return_value" + std::to_string(from_function);
+    symbol_exprt lhs(rvs, code_return.return_value().type());
+    assign(lhs, code_return.return_value(), ns);
   }
   else if(statement==ID_fence)
   {
diff --git a/src/util/goto_instruction_code.h b/src/util/goto_instruction_code.h
index c5e33176668..d02fa3ae328 100644
--- a/src/util/goto_instruction_code.h
+++ b/src/util/goto_instruction_code.h
@@ -189,6 +189,71 @@ inline code_deadt &to_code_dead(codet &code)
   return static_cast<code_deadt &>(code);
 }
 
+/// A `codet` representing the declaration of a local variable.
+/// For example, if a variable (symbol) `x` is represented as a
+/// \ref symbol_exprt `sym`, then the declaration of this variable can be
+/// represented as `code_declt(sym)`.
+class code_declt : public codet
+{
+public:
+  explicit code_declt(symbol_exprt symbol) : codet(ID_decl, {std::move(symbol)})
+  {
+  }
+
+  symbol_exprt &symbol()
+  {
+    return static_cast<symbol_exprt &>(op0());
+  }
+
+  const symbol_exprt &symbol() const
+  {
+    return static_cast<const symbol_exprt &>(op0());
+  }
+
+  const irep_idt &get_identifier() const
+  {
+    return symbol().get_identifier();
+  }
+
+  static void check(
+    const codet &code,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(
+      vm, code.operands().size() == 1, "declaration must have one operand");
+    DATA_CHECK(
+      vm,
+      code.op0().id() == ID_symbol,
+      "declaring a non-symbol: " +
+        id2string(to_symbol_expr(code.op0()).get_identifier()));
+  }
+};
+
+template <>
+inline bool can_cast_expr<code_declt>(const exprt &base)
+{
+  return detail::can_cast_code_impl(base, ID_decl);
+}
+
+inline void validate_expr(const code_declt &x)
+{
+  code_declt::check(x);
+}
+
+inline const code_declt &to_code_decl(const codet &code)
+{
+  PRECONDITION(code.get_statement() == ID_decl);
+  code_declt::check(code);
+  return static_cast<const code_declt &>(code);
+}
+
+inline code_declt &to_code_decl(codet &code)
+{
+  PRECONDITION(code.get_statement() == ID_decl);
+  code_declt::check(code);
+  return static_cast<code_declt &>(code);
+}
+
 /// \ref codet representation of a function call statement.
 /// The function call statement has three operands.
 /// The first is the expression that is used to store the return value.
@@ -414,4 +479,61 @@ inline void validate_expr(const code_outputt &output)
   code_outputt::check(output);
 }
 
+/// \ref codet representation of a "return from a function" statement.
+class code_returnt : public codet
+{
+public:
+  explicit code_returnt(exprt _op) : codet(ID_return, {std::move(_op)})
+  {
+  }
+
+  const exprt &return_value() const
+  {
+    return op0();
+  }
+
+  exprt &return_value()
+  {
+    return op0();
+  }
+
+  static void check(
+    const codet &code,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(vm, code.operands().size() == 1, "return must have one operand");
+  }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
+};
+
+template <>
+inline bool can_cast_expr<code_returnt>(const exprt &base)
+{
+  return detail::can_cast_code_impl(base, ID_return);
+}
+
+inline void validate_expr(const code_returnt &x)
+{
+  code_returnt::check(x);
+}
+
+inline const code_returnt &to_code_return(const codet &code)
+{
+  PRECONDITION(code.get_statement() == ID_return);
+  code_returnt::check(code);
+  return static_cast<const code_returnt &>(code);
+}
+
+inline code_returnt &to_code_return(codet &code)
+{
+  PRECONDITION(code.get_statement() == ID_return);
+  code_returnt::check(code);
+  return static_cast<code_returnt &>(code);
+}
+
 #endif // CPROVER_GOTO_PROGRAMS_GOTO_INSTRUCTION_CODE_H
diff --git a/src/util/std_code.h b/src/util/std_code.h
index 9a2e6c74841..991ce23dd75 100644
--- a/src/util/std_code.h
+++ b/src/util/std_code.h
@@ -12,155 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <list>
 
-#include "expr_cast.h"
-#include "invariant.h"
+#include "std_code_base.h"
 #include "std_expr.h"
-#include "validate.h"
-#include "validate_code.h"
-
-/// Data structure for representing an arbitrary statement in a program. Every
-/// specific type of statement (e.g. block of statements, assignment,
-/// if-then-else statement...) is represented by a subtype of `codet`.
-/// `codet`s are represented to be subtypes of \ref exprt since statements can
-/// occur in an expression context in C: for example, the assignment `x = y;`
-/// is an expression with return value `y`. For other types of statements in an
-/// expression context, see e.g.
-/// https://gcc.gnu.org/onlinedocs/gcc/Statement-Exprs.html.
-/// To distinguish a `codet` from other [exprts](\ref exprt), we set its
-/// [id()](\ref irept::id) to `ID_code`. To distinguish different types of
-/// `codet`, we use a named sub `ID_statement`.
-class codet:public exprt
-{
-public:
-  /// \param statement: Specifies the type of the `codet` to be constructed,
-  ///   e.g. `ID_block` for a \ref code_blockt or `ID_assign` for a
-  ///   \ref code_frontend_assignt.
-  explicit codet(const irep_idt &statement) : exprt(ID_code, empty_typet())
-  {
-    set_statement(statement);
-  }
-
-  codet(const irep_idt &statement, source_locationt loc)
-    : exprt(ID_code, empty_typet(), std::move(loc))
-  {
-    set_statement(statement);
-  }
-
-  /// \param statement: Specifies the type of the `codet` to be constructed,
-  ///   e.g. `ID_block` for a \ref code_blockt or `ID_assign` for a
-  ///   \ref code_frontend_assignt.
-  /// \param _op: any operands to be added
-  explicit codet(const irep_idt &statement, operandst _op) : codet(statement)
-  {
-    operands() = std::move(_op);
-  }
-
-  codet(const irep_idt &statement, operandst op, source_locationt loc)
-    : codet(statement, std::move(loc))
-  {
-    operands() = std::move(op);
-  }
-
-  void set_statement(const irep_idt &statement)
-  {
-    set(ID_statement, statement);
-  }
-
-  const irep_idt &get_statement() const
-  {
-    return get(ID_statement);
-  }
-
-  codet &first_statement();
-  const codet &first_statement() const;
-  codet &last_statement();
-  const codet &last_statement() const;
-
-  /// Check that the code statement is well-formed (shallow checks only, i.e.,
-  /// enclosed statements, subexpressions, etc. are not checked)
-  ///
-  /// Subclasses may override this function to provide specific well-formedness
-  /// checks for the corresponding types.
-  ///
-  /// The validation mode indicates whether well-formedness check failures are
-  /// reported via DATA_INVARIANT violations or exceptions.
-  static void check(const codet &, const validation_modet)
-  {
-  }
-
-  /// Check that the code statement is well-formed, assuming that all its
-  /// enclosed statements, subexpressions, etc. have all ready been checked for
-  /// well-formedness.
-  ///
-  /// Subclasses may override this function to provide specific well-formedness
-  /// checks for the corresponding types.
-  ///
-  /// The validation mode indicates whether well-formedness check failures are
-  /// reported via DATA_INVARIANT violations or exceptions.
-  static void validate(
-    const codet &code,
-    const namespacet &,
-    const validation_modet vm = validation_modet::INVARIANT)
-  {
-    check_code(code, vm);
-  }
-
-  /// Check that the code statement is well-formed (full check, including checks
-  /// of all subexpressions)
-  ///
-  /// Subclasses may override this function to provide specific well-formedness
-  /// checks for the corresponding types.
-  ///
-  /// The validation mode indicates whether well-formedness check failures are
-  /// reported via DATA_INVARIANT violations or exceptions.
-  static void validate_full(
-    const codet &code,
-    const namespacet &,
-    const validation_modet vm = validation_modet::INVARIANT)
-  {
-    check_code(code, vm);
-  }
-
-  using exprt::op0;
-  using exprt::op1;
-  using exprt::op2;
-  using exprt::op3;
-};
-
-namespace detail // NOLINT
-{
-
-template<typename Tag>
-inline bool can_cast_code_impl(const exprt &expr, const Tag &tag)
-{
-  if(const auto ptr = expr_try_dynamic_cast<codet>(expr))
-  {
-    return ptr->get_statement() == tag;
-  }
-  return false;
-}
-
-} // namespace detail
-
-template<> inline bool can_cast_expr<codet>(const exprt &base)
-{
-  return base.id()==ID_code;
-}
-
-// to_code has no validation other than checking the id(), so no validate_expr
-// is provided for codet
-
-inline const codet &to_code(const exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_code);
-  return static_cast<const codet &>(expr);
-}
-
-inline codet &to_code(exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_code);
-  return static_cast<codet &>(expr);
-}
 
 /// A \ref codet representing an assignment in the program.
 /// For example, if an expression `e1` is represented as an \ref exprt `expr1`
@@ -499,71 +352,6 @@ template<> inline bool can_cast_expr<code_skipt>(const exprt &base)
 
 // there is no to_code_skip, so no validate_expr is provided for code_skipt
 
-/// A `codet` representing the declaration of a local variable.
-/// For example, if a variable (symbol) `x` is represented as a
-/// \ref symbol_exprt `sym`, then the declaration of this variable can be
-/// represented as `code_declt(sym)`.
-class code_declt:public codet
-{
-public:
-  explicit code_declt(symbol_exprt symbol) : codet(ID_decl, {std::move(symbol)})
-  {
-  }
-
-  symbol_exprt &symbol()
-  {
-    return static_cast<symbol_exprt &>(op0());
-  }
-
-  const symbol_exprt &symbol() const
-  {
-    return static_cast<const symbol_exprt &>(op0());
-  }
-
-  const irep_idt &get_identifier() const
-  {
-    return symbol().get_identifier();
-  }
-
-  static void check(
-    const codet &code,
-    const validation_modet vm = validation_modet::INVARIANT)
-  {
-    DATA_CHECK(
-      vm, code.operands().size() == 1, "declaration must have one operand");
-    DATA_CHECK(
-      vm,
-      code.op0().id() == ID_symbol,
-      "declaring a non-symbol: " +
-        id2string(to_symbol_expr(code.op0()).get_identifier()));
-  }
-};
-
-template <>
-inline bool can_cast_expr<code_declt>(const exprt &base)
-{
-  return detail::can_cast_code_impl(base, ID_decl);
-}
-
-inline void validate_expr(const code_declt &x)
-{
-  code_declt::check(x);
-}
-
-inline const code_declt &to_code_decl(const codet &code)
-{
-  PRECONDITION(code.get_statement() == ID_decl);
-  code_declt::check(code);
-  return static_cast<const code_declt &>(code);
-}
-
-inline code_declt &to_code_decl(codet &code)
-{
-  PRECONDITION(code.get_statement() == ID_decl);
-  code_declt::check(code);
-  return static_cast<code_declt &>(code);
-}
-
 /// A `codet` representing the declaration of a local variable.
 /// For example, if a variable (symbol) `x` is represented as a
 /// \ref symbol_exprt `sym`, then the declaration of this variable can be
@@ -1114,14 +902,14 @@ inline code_gotot &to_code_goto(codet &code)
 }
 
 /// \ref codet representation of a "return from a function" statement.
-class code_returnt:public codet
+class code_frontend_returnt : public codet
 {
 public:
-  code_returnt() : codet(ID_return, {nil_exprt()})
+  code_frontend_returnt() : codet(ID_return, {nil_exprt()})
   {
   }
 
-  explicit code_returnt(exprt _op) : codet(ID_return, {std::move(_op)})
+  explicit code_frontend_returnt(exprt _op) : codet(ID_return, {std::move(_op)})
   {
   }
 
@@ -1154,28 +942,29 @@ class code_returnt:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_returnt>(const exprt &base)
+template <>
+inline bool can_cast_expr<code_frontend_returnt>(const exprt &base)
 {
   return detail::can_cast_code_impl(base, ID_return);
 }
 
-inline void validate_expr(const code_returnt &x)
+inline void validate_expr(const code_frontend_returnt &x)
 {
-  code_returnt::check(x);
+  code_frontend_returnt::check(x);
 }
 
-inline const code_returnt &to_code_return(const codet &code)
+inline const code_frontend_returnt &to_code_frontend_return(const codet &code)
 {
   PRECONDITION(code.get_statement() == ID_return);
-  code_returnt::check(code);
-  return static_cast<const code_returnt &>(code);
+  code_frontend_returnt::check(code);
+  return static_cast<const code_frontend_returnt &>(code);
 }
 
-inline code_returnt &to_code_return(codet &code)
+inline code_frontend_returnt &to_code_frontend_return(codet &code)
 {
   PRECONDITION(code.get_statement() == ID_return);
-  code_returnt::check(code);
-  return static_cast<code_returnt &>(code);
+  code_frontend_returnt::check(code);
+  return static_cast<code_frontend_returnt &>(code);
 }
 
 /// \ref codet representation of a label for branch targets.
diff --git a/src/util/std_code_base.h b/src/util/std_code_base.h
new file mode 100644
index 00000000000..55282af4951
--- /dev/null
+++ b/src/util/std_code_base.h
@@ -0,0 +1,162 @@
+/*******************************************************************\
+
+Module: Data structures representing statements in a program
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_STD_CODE_BASE_H
+#define CPROVER_UTIL_STD_CODE_BASE_H
+
+#include "expr_cast.h"
+#include "invariant.h"
+#include "std_types.h"
+#include "validate.h"
+#include "validate_code.h"
+
+/// Data structure for representing an arbitrary statement in a program. Every
+/// specific type of statement (e.g. block of statements, assignment,
+/// if-then-else statement...) is represented by a subtype of `codet`.
+/// `codet`s are represented to be subtypes of \ref exprt since statements can
+/// occur in an expression context in C: for example, the assignment `x = y;`
+/// is an expression with return value `y`. For other types of statements in an
+/// expression context, see e.g.
+/// https://gcc.gnu.org/onlinedocs/gcc/Statement-Exprs.html.
+/// To distinguish a `codet` from other [exprts](\ref exprt), we set its
+/// [id()](\ref irept::id) to `ID_code`. To distinguish different types of
+/// `codet`, we use a named sub `ID_statement`.
+class codet : public exprt
+{
+public:
+  /// \param statement: Specifies the type of the `codet` to be constructed,
+  ///   e.g. `ID_block` for a \ref code_blockt or `ID_assign` for a
+  ///   \ref code_frontend_assignt.
+  explicit codet(const irep_idt &statement) : exprt(ID_code, empty_typet())
+  {
+    set_statement(statement);
+  }
+
+  codet(const irep_idt &statement, source_locationt loc)
+    : exprt(ID_code, empty_typet(), std::move(loc))
+  {
+    set_statement(statement);
+  }
+
+  /// \param statement: Specifies the type of the `codet` to be constructed,
+  ///   e.g. `ID_block` for a \ref code_blockt or `ID_assign` for a
+  ///   \ref code_frontend_assignt.
+  /// \param _op: any operands to be added
+  explicit codet(const irep_idt &statement, operandst _op) : codet(statement)
+  {
+    operands() = std::move(_op);
+  }
+
+  codet(const irep_idt &statement, operandst op, source_locationt loc)
+    : codet(statement, std::move(loc))
+  {
+    operands() = std::move(op);
+  }
+
+  void set_statement(const irep_idt &statement)
+  {
+    set(ID_statement, statement);
+  }
+
+  const irep_idt &get_statement() const
+  {
+    return get(ID_statement);
+  }
+
+  codet &first_statement();
+  const codet &first_statement() const;
+  codet &last_statement();
+  const codet &last_statement() const;
+
+  /// Check that the code statement is well-formed (shallow checks only, i.e.,
+  /// enclosed statements, subexpressions, etc. are not checked)
+  ///
+  /// Subclasses may override this function to provide specific well-formedness
+  /// checks for the corresponding types.
+  ///
+  /// The validation mode indicates whether well-formedness check failures are
+  /// reported via DATA_INVARIANT violations or exceptions.
+  static void check(const codet &, const validation_modet)
+  {
+  }
+
+  /// Check that the code statement is well-formed, assuming that all its
+  /// enclosed statements, subexpressions, etc. have all ready been checked for
+  /// well-formedness.
+  ///
+  /// Subclasses may override this function to provide specific well-formedness
+  /// checks for the corresponding types.
+  ///
+  /// The validation mode indicates whether well-formedness check failures are
+  /// reported via DATA_INVARIANT violations or exceptions.
+  static void validate(
+    const codet &code,
+    const namespacet &,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    check_code(code, vm);
+  }
+
+  /// Check that the code statement is well-formed (full check, including checks
+  /// of all subexpressions)
+  ///
+  /// Subclasses may override this function to provide specific well-formedness
+  /// checks for the corresponding types.
+  ///
+  /// The validation mode indicates whether well-formedness check failures are
+  /// reported via DATA_INVARIANT violations or exceptions.
+  static void validate_full(
+    const codet &code,
+    const namespacet &,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    check_code(code, vm);
+  }
+
+  using exprt::op0;
+  using exprt::op1;
+  using exprt::op2;
+  using exprt::op3;
+};
+
+namespace detail // NOLINT
+{
+template <typename Tag>
+inline bool can_cast_code_impl(const exprt &expr, const Tag &tag)
+{
+  if(const auto ptr = expr_try_dynamic_cast<codet>(expr))
+  {
+    return ptr->get_statement() == tag;
+  }
+  return false;
+}
+
+} // namespace detail
+
+template <>
+inline bool can_cast_expr<codet>(const exprt &base)
+{
+  return base.id() == ID_code;
+}
+
+// to_code has no validation other than checking the id(), so no validate_expr
+// is provided for codet
+
+inline const codet &to_code(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_code);
+  return static_cast<const codet &>(expr);
+}
+
+inline codet &to_code(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_code);
+  return static_cast<codet &>(expr);
+}
+
+#endif // CPROVER_UTIL_STD_CODE_BASE_H
diff --git a/unit/goto-programs/goto_program_validate.cpp b/unit/goto-programs/goto_program_validate.cpp
index 58fc65bb691..6c35b8e3868 100644
--- a/unit/goto-programs/goto_program_validate.cpp
+++ b/unit/goto-programs/goto_program_validate.cpp
@@ -185,35 +185,6 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]")
     }
   }
 
-  /// check_returns_removed()
-  WHEN(
-    "not all returns have been removed - an instruction is of type "
-    "'return'")
-  {
-    THEN("fail!")
-    {
-      goto_convert(goto_model, null_message_handler);
-
-      auto &function_map = goto_model.goto_functions.function_map;
-      auto it = function_map.find("g");
-      auto &instructions = it->second.body.instructions;
-      instructions.insert(
-        instructions.begin(), goto_programt::make_return(code_returnt()));
-
-      goto_model_validation_optionst validation_options{
-        goto_model_validation_optionst ::set_optionst::all_false};
-
-      validation_options.check_returns_removed = true;
-
-      REQUIRE_THROWS_AS(
-        validate_goto_model(
-          goto_model.goto_functions,
-          validation_modet::EXCEPTION,
-          validation_options),
-        incorrect_goto_program_exceptiont);
-    }
-  }
-
   WHEN("not all returns have been removed - a function call lhs is not nil")
   {
     // int h();