Introduce code_frontend_returnt

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);
 }

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

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;

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);

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

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+=';';

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
         {

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)==';')

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

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

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
   {

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(

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(

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

src/jsil/jsil_typecheck.h

@@ -20,7 +20,7 @@ Author: Michael Tautschnig, [email protected]
 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);

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

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