diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index 013362406aa..ea180d4c5d3 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -316,7 +316,7 @@ void c_typecheck_baset::typecheck_decl(codet &code)
     }
     else
     {
-      code_declt decl(symbol.symbol_expr());
+      code_frontend_declt decl(symbol.symbol_expr());
       decl.add_source_location() = symbol.location;
       decl.symbol().add_source_location() = symbol.location;
 
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index ad9a2dc2701..fb597a90f72 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -323,7 +323,7 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
 
     // replace declarations by symbol expressions
     for(auto &binding : bindings)
-      binding = to_code_decl(to_code(binding)).symbol();
+      binding = to_code_frontend_decl(to_code(binding)).symbol();
 
     if(expr.id() == ID_lambda)
     {
@@ -788,7 +788,7 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr)
         throw 0;
       }
 
-      code_declt decl(symbol.symbol_expr());
+      code_frontend_declt decl(symbol.symbol_expr());
       decl.add_source_location() = declaration.source_location();
 
       binding = decl;
diff --git a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
index 386943e029c..b3e0d725007 100644
--- a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
+++ b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
@@ -635,7 +635,7 @@ static void instantiate_atomic_fetch_op(
   const symbol_exprt result =
     result_symbol(identifier_with_type, type, source_location, symbol_table)
       .symbol_expr();
-  block.add(codet{ID_decl_block, {code_declt{result}}});
+  block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
 
   // place operations on *ptr in an atomic section
   block.add(code_expressiont{side_effect_expr_function_callt{
@@ -697,7 +697,7 @@ static void instantiate_atomic_op_fetch(
   const symbol_exprt result =
     result_symbol(identifier_with_type, type, source_location, symbol_table)
       .symbol_expr();
-  block.add(codet{ID_decl_block, {code_declt{result}}});
+  block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
 
   // place operations on *ptr in an atomic section
   block.add(code_expressiont{side_effect_expr_function_callt{
@@ -810,7 +810,7 @@ static void instantiate_sync_val_compare_and_swap(
   const symbol_exprt result =
     result_symbol(identifier_with_type, type, source_location, symbol_table)
       .symbol_expr();
-  block.add(codet{ID_decl_block, {code_declt{result}}});
+  block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
 
   // place operations on *ptr in an atomic section
   block.add(code_expressiont{side_effect_expr_function_callt{
@@ -868,7 +868,7 @@ static void instantiate_sync_lock_test_and_set(
   const symbol_exprt result =
     result_symbol(identifier_with_type, type, source_location, symbol_table)
       .symbol_expr();
-  block.add(codet{ID_decl_block, {code_declt{result}}});
+  block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
 
   // place operations on *ptr in an atomic section
   block.add(code_expressiont{side_effect_expr_function_callt{
@@ -990,7 +990,7 @@ static void instantiate_atomic_load_n(
   const symbol_exprt result =
     result_symbol(identifier_with_type, type, source_location, symbol_table)
       .symbol_expr();
-  block.add(codet{ID_decl_block, {code_declt{result}}});
+  block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
 
   block.add(code_expressiont{side_effect_expr_function_callt{
     symbol_exprt::typeless(ID___atomic_load),
@@ -1105,7 +1105,7 @@ static void instantiate_atomic_exchange_n(
   const symbol_exprt result =
     result_symbol(identifier_with_type, type, source_location, symbol_table)
       .symbol_expr();
-  block.add(codet{ID_decl_block, {code_declt{result}}});
+  block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
 
   block.add(code_expressiont{side_effect_expr_function_callt{
     symbol_exprt::typeless(ID___atomic_exchange),
@@ -1142,7 +1142,7 @@ static void instantiate_atomic_compare_exchange(
     result_symbol(
       identifier_with_type, c_bool_type(), source_location, symbol_table)
       .symbol_expr();
-  block.add(codet{ID_decl_block, {code_declt{result}}});
+  block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
 
   // place operations on *ptr in an atomic section
   block.add(code_expressiont{side_effect_expr_function_callt{
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index aa44d7dbbfa..70e2c397857 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -634,7 +634,7 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
       // produce the code that declares and initializes the symbol
       symbol_exprt symbol_expr = new_symbol.symbol_expr();
 
-      code_declt declaration(symbol_expr);
+      code_frontend_declt declaration(symbol_expr);
       declaration.add_source_location() = size_source_location;
 
       code_assignt assignment;
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 91ba5aa039e..e82b696d608 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -2761,9 +2761,8 @@ std::string expr2ct::convert_code_continue(unsigned indent)
   return dest;
 }
 
-std::string expr2ct::convert_code_decl(
-  const codet &src,
-  unsigned indent)
+std::string
+expr2ct::convert_code_frontend_decl(const codet &src, unsigned indent)
 {
   // initializer to go away
   if(src.operands().size()!=1 &&
@@ -3013,7 +3012,7 @@ std::string expr2ct::convert_code(
     return convert_code_continue(indent);
 
   if(statement==ID_decl)
-    return convert_code_decl(src, indent);
+    return convert_code_frontend_decl(src, indent);
 
   if(statement==ID_decl_block)
     return convert_code_decl_block(src, indent);
diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h
index 513f8969bfa..66dac11166d 100644
--- a/src/ansi-c/expr2c_class.h
+++ b/src/ansi-c/expr2c_class.h
@@ -214,7 +214,7 @@ class expr2ct
   std::string convert_code_break(unsigned indent);
   std::string convert_code_switch(const codet &src, unsigned indent);
   std::string convert_code_continue(unsigned indent);
-  std::string convert_code_decl(const codet &src, unsigned indent);
+  std::string convert_code_frontend_decl(const codet &, unsigned indent);
   std::string convert_code_decl_block(const codet &src, unsigned indent);
   std::string convert_code_dead(const codet &src, unsigned indent);
   // NOLINTNEXTLINE(whitespace/line_length)
diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp
index c4f76e4ef2e..15e4e32a0e2 100644
--- a/src/cpp/cpp_typecheck_code.cpp
+++ b/src/cpp/cpp_typecheck_code.cpp
@@ -120,7 +120,7 @@ void cpp_typecheckt::typecheck_try_catch(codet &code)
       {
         // turn references into non-references
         {
-          code_declt &decl = to_code_decl(statements.front());
+          code_frontend_declt &decl = to_code_frontend_decl(statements.front());
           cpp_declarationt &cpp_declaration = to_cpp_declaration(decl.symbol());
 
           assert(cpp_declaration.declarators().size()==1);
@@ -139,8 +139,8 @@ void cpp_typecheckt::typecheck_try_catch(codet &code)
           catch_block.statements().front().get_statement() == ID_decl_block);
 
         // get the declaration
-        const code_declt &code_decl =
-          to_code_decl(to_code(catch_block.statements().front().op0()));
+        const code_frontend_declt &code_decl = to_code_frontend_decl(
+          to_code(catch_block.statements().front().op0()));
 
         // get the type
         const typet &type = code_decl.symbol().type();
@@ -199,7 +199,7 @@ void cpp_typecheckt::typecheck_switch(codet &code)
     assert(decl.operands().size()==1);
 
     // replace declaration by its symbol
-    value = to_code_decl(to_code(to_unary_expr(decl).op())).symbol();
+    value = to_code_frontend_decl(to_code(to_unary_expr(decl).op())).symbol();
 
     c_typecheck_baset::typecheck_switch(code);
 
@@ -456,7 +456,7 @@ void cpp_typecheckt::typecheck_decl(codet &code)
       throw 0;
     }
 
-    code_declt decl_statement(cpp_symbol_expr(symbol));
+    code_frontend_declt decl_statement(cpp_symbol_expr(symbol));
     decl_statement.add_source_location()=symbol.location;
 
     // Do we have an initializer that's not code?
diff --git a/src/cpp/cpp_typecheck_declaration.cpp b/src/cpp/cpp_typecheck_declaration.cpp
index c31580b3fb3..c1e0043b679 100644
--- a/src/cpp/cpp_typecheck_declaration.cpp
+++ b/src/cpp/cpp_typecheck_declaration.cpp
@@ -58,7 +58,7 @@ codet cpp_typecheckt::convert_anonymous_union(cpp_declarationt &declaration)
     throw 0;
   }
 
-  new_code.add_to_operands(code_declt(cpp_symbol_expr(symbol)));
+  new_code.add_to_operands(code_frontend_declt(cpp_symbol_expr(symbol)));
 
   // do scoping
   symbolt union_symbol =
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
index 2759b64a6b7..7220976c641 100644
--- a/src/cpp/parse.cpp
+++ b/src/cpp/parse.cpp
@@ -679,7 +679,7 @@ optionalt<codet> Parser::rTypedefStatement()
   if(!rTypedef(declaration))
     return {};
 
-  return code_declt(
+  return code_frontend_declt(
     static_cast<symbol_exprt &>(static_cast<exprt &>(declaration)));
 }
 
@@ -7501,7 +7501,7 @@ optionalt<codet> Parser::rStatement()
         cpp_declarationt declaration;
         if(!rTypedefUsing(declaration))
           return {};
-        code_declt statement(
+        code_frontend_declt statement(
           static_cast<symbol_exprt &>(static_cast<exprt &>(declaration)));
         statement.add_source_location() = declaration.source_location();
         return std::move(statement);
@@ -7790,7 +7790,7 @@ optionalt<codet> Parser::rTryStatement()
       if(declaration.declarators().front().name().is_nil())
         declaration.declarators().front().name() = cpp_namet("#anon");
 
-      code_declt code_decl(
+      code_frontend_declt code_decl(
         static_cast<symbol_exprt &>(static_cast<exprt &>(declaration)));
       set_location(code_decl, catch_token);
 
@@ -8237,7 +8237,7 @@ optionalt<codet> Parser::rDeclarationStatement()
       cpp_declarationt declaration;
       if(!rConstDeclaration(declaration))
         return {};
-      return code_declt(
+      return code_frontend_declt(
         static_cast<symbol_exprt &>(static_cast<exprt &>(declaration)));
     }
     else
@@ -8268,7 +8268,7 @@ optionalt<codet> Parser::rIntegralDeclStatement(
   if(lex.LookAhead(0)==';')
   {
     lex.get_token(tk);
-    code_declt statement(
+    code_frontend_declt statement(
       static_cast<symbol_exprt &>(static_cast<exprt &>(declaration)));
     set_location(statement, tk);
     return std::move(statement);
@@ -8281,7 +8281,7 @@ optionalt<codet> Parser::rIntegralDeclStatement(
     if(lex.get_token(tk)!=';')
       return {};
 
-    code_declt statement(
+    code_frontend_declt statement(
       static_cast<symbol_exprt &>(static_cast<exprt &>(declaration)));
     set_location(statement, tk);
     return std::move(statement);
@@ -8333,7 +8333,7 @@ Parser::rOtherDeclStatement(cpp_storage_spect &storage_spec, typet &cv_q)
   if(lex.get_token(tk)!=';')
     return {};
 
-  code_declt statement(
+  code_frontend_declt statement(
     static_cast<symbol_exprt &>(static_cast<exprt &>(declaration)));
   set_location(statement, tk);
   return std::move(statement);
diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
index 0c56f35517c..b821df81f8d 100644
--- a/src/goto-instrument/dump_c.cpp
+++ b/src/goto-instrument/dump_c.cpp
@@ -649,7 +649,7 @@ void dump_ct::convert_compound_enum(
 }
 
 void dump_ct::cleanup_decl(
-  code_declt &decl,
+  code_frontend_declt &decl,
   std::list<irep_idt> &local_static,
   std::list<irep_idt> &local_type_decls)
 {
@@ -908,7 +908,7 @@ void dump_ct::convert_global_variable(
       !converted_global.insert(symbol.name).second)
     return;
 
-  code_declt d(symbol.symbol_expr());
+  code_frontend_declt d(symbol.symbol_expr());
 
   find_symbols_sett syms;
   if(symbol.value.is_not_nil())
@@ -1214,7 +1214,7 @@ void dump_ct::insert_local_static_decls(
       local_static_decls.find(*it);
     PRECONDITION(d_it!=local_static_decls.end());
 
-    code_declt d=d_it->second;
+    code_frontend_declt d = d_it->second;
     std::list<irep_idt> redundant;
     cleanup_decl(d, redundant, type_decls);
 
diff --git a/src/goto-instrument/dump_c_class.h b/src/goto-instrument/dump_c_class.h
index 6190a6f5c16..f69e437e189 100644
--- a/src/goto-instrument/dump_c_class.h
+++ b/src/goto-instrument/dump_c_class.h
@@ -198,7 +198,7 @@ class dump_ct
       const typet &type)
   {
     symbol_exprt sym(identifier, type);
-    code_declt d(sym);
+    code_frontend_declt d(sym);
 
     std::string d_str=expr_to_string(d);
     assert(!d_str.empty());
@@ -232,7 +232,7 @@ class dump_ct
     const typet &type,
     std::ostream &os);
 
-  typedef std::unordered_map<irep_idt, code_declt> local_static_declst;
+  typedef std::unordered_map<irep_idt, code_frontend_declt> local_static_declst;
 
   void convert_global_variable(
       const symbolt &symbol,
@@ -259,7 +259,7 @@ class dump_ct
   void cleanup_expr(exprt &expr);
   void cleanup_type(typet &type);
   void cleanup_decl(
-    code_declt &decl,
+    code_frontend_declt &decl,
     std::list<irep_idt> &local_static,
     std::list<irep_idt> &local_type_decls);
   void cleanup_harness(code_blockt &b);
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
index ed548ddef59..a8a9136732e 100644
--- a/src/goto-instrument/goto_program2code.cpp
+++ b/src/goto-instrument/goto_program2code.cpp
@@ -449,7 +449,7 @@ goto_programt::const_targett goto_program2codet::convert_decl(
   goto_programt::const_targett upper_bound,
   code_blockt &dest)
 {
-  code_declt d = code_declt{target->decl_symbol()};
+  code_frontend_declt d = code_frontend_declt{target->decl_symbol()};
   symbol_exprt &symbol = d.symbol();
 
   goto_programt::const_targett next=target;
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index 455e1322090..80b04fab3af 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -436,7 +436,7 @@ void goto_convertt::convert(
   if(statement==ID_block)
     convert_block(to_code_block(code), dest, mode);
   else if(statement==ID_decl)
-    convert_decl(to_code_decl(code), dest, mode);
+    convert_frontend_decl(to_code_frontend_decl(code), dest, mode);
   else if(statement==ID_decl_type)
     convert_decl_type(code, dest);
   else if(statement==ID_expression)
@@ -606,8 +606,8 @@ void goto_convertt::convert_expression(
   }
 }
 
-void goto_convertt::convert_decl(
-  const code_declt &code,
+void goto_convertt::convert_frontend_decl(
+  const code_frontend_declt &code,
   goto_programt &dest,
   const irep_idt &mode)
 {
@@ -1845,9 +1845,9 @@ symbolt &goto_convertt::new_tmp_symbol(
     mode,
     symbol_table);
 
-  code_declt decl(new_symbol.symbol_expr());
+  code_frontend_declt decl(new_symbol.symbol_expr());
   decl.add_source_location()=source_location;
-  convert_decl(decl, dest, mode);
+  convert_frontend_decl(decl, dest, mode);
 
   return new_symbol;
 }
diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h
index 0f644dad6ad..54050055f2e 100644
--- a/src/goto-programs/goto_convert_class.h
+++ b/src/goto-programs/goto_convert_class.h
@@ -222,9 +222,9 @@ class goto_convertt:public messaget
     const code_blockt &code,
     goto_programt &dest,
     const irep_idt &mode);
-  void convert_decl(
-    const code_declt &code,
-    goto_programt &dest,
+  void convert_frontend_decl(
+    const code_frontend_declt &,
+    goto_programt &,
     const irep_idt &mode);
   void convert_decl_type(const codet &code, goto_programt &dest);
   void convert_expression(
diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp
index c118abcd498..8ed67d19b53 100644
--- a/src/goto-programs/goto_convert_side_effect.cpp
+++ b/src/goto-programs/goto_convert_side_effect.cpp
@@ -381,9 +381,9 @@ void goto_convertt::remove_function_call(
     symbol_table);
 
   {
-    code_declt decl(new_symbol.symbol_expr());
+    code_frontend_declt decl(new_symbol.symbol_expr());
     decl.add_source_location()=new_symbol.location;
-    convert_decl(decl, dest, mode);
+    convert_frontend_decl(decl, dest, mode);
   }
 
   {
@@ -421,9 +421,9 @@ void goto_convertt::remove_cpp_new(
     ID_cpp,
     symbol_table);
 
-  code_declt decl(new_symbol.symbol_expr());
+  code_frontend_declt decl(new_symbol.symbol_expr());
   decl.add_source_location()=new_symbol.location;
-  convert_decl(decl, dest, ID_cpp);
+  convert_frontend_decl(decl, dest, ID_cpp);
 
   const code_assignt call(new_symbol.symbol_expr(), expr);
 
@@ -467,9 +467,9 @@ void goto_convertt::remove_malloc(
       mode,
       symbol_table);
 
-    code_declt decl(new_symbol.symbol_expr());
+    code_frontend_declt decl(new_symbol.symbol_expr());
     decl.add_source_location()=new_symbol.location;
-    convert_decl(decl, dest, mode);
+    convert_frontend_decl(decl, dest, mode);
 
     code_assignt call(new_symbol.symbol_expr(), expr);
     call.add_source_location()=expr.source_location();
diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h
index bbb3d8ee823..4ba2865849c 100644
--- a/src/goto-programs/goto_program.h
+++ b/src/goto-programs/goto_program.h
@@ -226,9 +226,6 @@ class goto_programt
     {
       PRECONDITION(is_decl());
       auto &decl = expr_checked_cast<code_declt>(code);
-      INVARIANT(
-        !decl.initial_value(),
-        "code_declt in goto program may not contain initialization.");
       return decl.symbol();
     }
 
@@ -237,9 +234,6 @@ class goto_programt
     {
       PRECONDITION(is_decl());
       auto &decl = expr_checked_cast<code_declt>(code);
-      INVARIANT(
-        !decl.initial_value(),
-        "code_declt in goto program may not contain initialization.");
       return decl.symbol();
     }
 
diff --git a/src/goto-programs/wp.cpp b/src/goto-programs/wp.cpp
index 76502d2ce7c..8961215313a 100644
--- a/src/goto-programs/wp.cpp
+++ b/src/goto-programs/wp.cpp
@@ -225,7 +225,6 @@ exprt wp_decl(
   const exprt &post,
   const namespacet &ns)
 {
-  PRECONDITION(!code.initial_value());
   // Model decl(var) as var = nondet()
   const exprt &var = code.symbol();
   side_effect_expr_nondett nondet(var.type(), source_locationt());
diff --git a/src/jsil/jsil_convert.cpp b/src/jsil/jsil_convert.cpp
index e65b18eeb03..db34bf3504d 100644
--- a/src/jsil/jsil_convert.cpp
+++ b/src/jsil/jsil_convert.cpp
@@ -91,7 +91,7 @@ bool jsil_convertt::convert_code(const symbolt &symbol, codet &code)
 
       code_try_catcht t_c(std::move(t));
       // Adding empty symbol to catch decl
-      code_declt d(symbol_exprt::typeless("decl_symbol"));
+      code_frontend_declt d(symbol_exprt::typeless("decl_symbol"));
       t_c.add_catch(d, g);
       t_c.add_source_location()=code.source_location();
 
diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp
index 5d6273c6e80..780bdb16135 100644
--- a/src/util/format_expr.cpp
+++ b/src/util/format_expr.cpp
@@ -443,7 +443,7 @@ void format_expr_configt::setup()
     {
       return os << "dead " << format(to_code_dead(code).symbol()) << ";";
     }
-    else if(const auto decl = expr_try_dynamic_cast<code_declt>(code))
+    else if(const auto decl = expr_try_dynamic_cast<code_frontend_declt>(code))
     {
       const auto &declaration_symb = decl->symbol();
       os << "decl " << format(declaration_symb.type()) << " "
diff --git a/src/util/std_code.h b/src/util/std_code.h
index 04aaa27d53d..dad84b5e009 100644
--- a/src/util/std_code.h
+++ b/src/util/std_code.h
@@ -311,6 +311,72 @@ class code_declt:public codet
     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
+/// represented as `code_frontend_declt(sym)`.
+class code_frontend_declt : public codet
+{
+public:
+  explicit code_frontend_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();
+  }
+
   /// Returns the initial value to which the declared variable is initialized,
   /// or empty in the case where no initialisation is included.
   /// \note: Initial values may be present in the front end but they must be
@@ -360,28 +426,29 @@ class code_declt:public codet
   }
 };
 
-template<> inline bool can_cast_expr<code_declt>(const exprt &base)
+template <>
+inline bool can_cast_expr<code_frontend_declt>(const exprt &base)
 {
   return detail::can_cast_code_impl(base, ID_decl);
 }
 
-inline void validate_expr(const code_declt &x)
+inline void validate_expr(const code_frontend_declt &x)
 {
-  code_declt::check(x);
+  code_frontend_declt::check(x);
 }
 
-inline const code_declt &to_code_decl(const codet &code)
+inline const code_frontend_declt &to_code_frontend_decl(const codet &code)
 {
   PRECONDITION(code.get_statement() == ID_decl);
-  code_declt::check(code);
-  return static_cast<const code_declt &>(code);
+  code_frontend_declt::check(code);
+  return static_cast<const code_frontend_declt &>(code);
 }
 
-inline code_declt &to_code_decl(codet &code)
+inline code_frontend_declt &to_code_frontend_decl(codet &code)
 {
   PRECONDITION(code.get_statement() == ID_decl);
-  code_declt::check(code);
-  return static_cast<code_declt &>(code);
+  code_frontend_declt::check(code);
+  return static_cast<code_frontend_declt &>(code);
 }
 
 /// Create a fatal assertion, which checks a condition and then halts if it does
@@ -1944,16 +2011,16 @@ class code_try_catcht:public codet
     return static_cast<const codet &>(op0());
   }
 
-  code_declt &get_catch_decl(unsigned i)
+  code_frontend_declt &get_catch_decl(unsigned i)
   {
     PRECONDITION((2 * i + 2) < operands().size());
-    return to_code_decl(to_code(operands()[2*i+1]));
+    return to_code_frontend_decl(to_code(operands()[2 * i + 1]));
   }
 
-  const code_declt &get_catch_decl(unsigned i) const
+  const code_frontend_declt &get_catch_decl(unsigned i) const
   {
     PRECONDITION((2 * i + 2) < operands().size());
-    return to_code_decl(to_code(operands()[2*i+1]));
+    return to_code_frontend_decl(to_code(operands()[2 * i + 1]));
   }
 
   codet &get_catch_code(unsigned i)
@@ -1968,7 +2035,7 @@ class code_try_catcht:public codet
     return to_code(operands()[2*i+2]);
   }
 
-  void add_catch(const code_declt &to_catch, const codet &code_catch)
+  void add_catch(const code_frontend_declt &to_catch, const codet &code_catch)
   {
     add_to_operands(to_catch, code_catch);
   }
diff --git a/unit/util/format.cpp b/unit/util/format.cpp
index dd6017662b4..8fd1d5d0dc5 100644
--- a/unit/util/format.cpp
+++ b/unit/util/format.cpp
@@ -16,7 +16,7 @@
 TEST_CASE("Format a declaration statement.", "[core][util][format]")
 {
   const signedbv_typet int_type{32};
-  code_declt declaration{symbol_exprt{"foo", int_type}};
+  code_frontend_declt declaration{symbol_exprt{"foo", int_type}};
   REQUIRE(format_to_string(declaration) == "decl signedbv[32] foo;");
   declaration.set_initial_value({int_type.zero_expr()});
   REQUIRE(format_to_string(declaration) == "decl signedbv[32] foo = 0;");