rename RETURN -> SET_RETURN_VALUE

jbmc/src/java_bytecode/replace_java_nondet.cpp

@@ -160,7 +160,7 @@ static bool is_return_with_variable(
   const goto_programt::instructiont &instr,
   const irep_idt &identifier)
 {
-  if(!instr.is_return())
+  if(!instr.is_set_return_value())
   {
     return false;
   }
@@ -271,7 +271,7 @@ static goto_programt::targett check_and_replace_target(
       instr.turn_into_skip();
     });
 
-  if(target_instruction->is_return())
+  if(target_instruction->is_set_return_value())
   {
     const auto &nondet_var = target_instruction->return_value();
 

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

@@ -45,7 +45,7 @@ void validate_nondet_method_removed(
       }
     }
 
-    if(inst.is_return())
+    if(inst.is_set_return_value())
     {
       const auto &return_value = inst.return_value();
       if(return_value.id() == ID_side_effect)
@@ -94,7 +94,7 @@ void validate_nondets_converted(
     exprt target_expression =
       (inst.is_assign()
          ? inst.get_assign().rhs()
-         : inst.is_return() ? inst.return_value() : inst.get_code());
+         : inst.is_set_return_value() ? inst.return_value() : inst.get_code());
 
     if(
       const auto side_effect =

src/analyses/custom_bitvector_analysis.cpp

@@ -540,8 +540,8 @@ void custom_bitvector_domaint::transform(
   case THROW:
     DATA_INVARIANT(false, "Exceptions must be removed before analysis");
     break;
-  case RETURN:
-    DATA_INVARIANT(false, "Returns must be removed before analysis");
+  case SET_RETURN_VALUE:
+    DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
     break;
   case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
   case ATOMIC_END:   // Ignoring is a valid over-approximation

src/analyses/escape_analysis.cpp

@@ -255,8 +255,8 @@ void escape_domaint::transform(
   case THROW:
     DATA_INVARIANT(false, "Exceptions must be removed before analysis");
     break;
-  case RETURN:
-    DATA_INVARIANT(false, "Returns must be removed before analysis");
+  case SET_RETURN_VALUE:
+    DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
     break;
   case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
   case ATOMIC_END:   // Ignoring is a valid over-approximation

src/analyses/global_may_alias.cpp

@@ -134,8 +134,8 @@ void global_may_alias_domaint::transform(
   case THROW:
     DATA_INVARIANT(false, "Exceptions must be removed before analysis");
     break;
-  case RETURN:
-    DATA_INVARIANT(false, "Returns must be removed before analysis");
+  case SET_RETURN_VALUE:
+    DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
     break;
   case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
   case ATOMIC_END:   // Ignoring is a valid over-approximation

src/analyses/goto_check.cpp

@@ -2032,7 +2032,7 @@ void goto_checkt::goto_check(
       // the call might invalidate any assertion
       assertions.clear();
     }
-    else if(i.is_return())
+    else if(i.is_set_return_value())
     {
       check(i.return_value());
       // the return value invalidate any assertion

src/analyses/goto_rw.cpp

@@ -771,7 +771,7 @@ void goto_rw(
       target->get_condition());
     break;
 
-  case RETURN:
+  case SET_RETURN_VALUE:
     rw_set.get_objects_rec(
       function, target, rw_range_sett::get_modet::READ, target->return_value());
     break;

src/analyses/interval_domain.cpp

@@ -115,8 +115,8 @@ void interval_domaint::transform(
   case THROW:
     DATA_INVARIANT(false, "Exceptions must be removed before analysis");
     break;
-  case RETURN:
-    DATA_INVARIANT(false, "Returns must be removed before analysis");
+  case SET_RETURN_VALUE:
+    DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
     break;
   case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
   case ATOMIC_END:   // Ignoring is a valid over-approximation

src/analyses/invariant_set_domain.cpp

@@ -50,11 +50,11 @@ void invariant_set_domaint::transform(
     }
     break;
 
-  case RETURN:
-    // ignore
-    break;
+    case SET_RETURN_VALUE:
+      // ignore
+      break;
 
-  case ASSIGN:
+    case ASSIGN:
     {
       const code_assignt &assignment = from_l->get_assign();
       invariant_set.assignment(assignment.lhs(), assignment.rhs());

src/analyses/local_bitvector_analysis.cpp

@@ -307,9 +307,9 @@ void local_bitvector_analysist::build()
       DATA_INVARIANT(false, "Exceptions must be removed before analysis");
       break;
 #endif
-    case RETURN:
+    case SET_RETURN_VALUE:
 #if 0
-      DATA_INVARIANT(false, "Returns must be removed before analysis");
+      DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
       break;
 #endif
     case ATOMIC_BEGIN: // Ignoring is a valid over-approximation

src/analyses/local_cfg.cpp

@@ -61,7 +61,7 @@ void local_cfgt::build(const goto_programt &goto_program)
       break; // no successor
 
     case CATCH:
-    case RETURN:
+    case SET_RETURN_VALUE:
     case ATOMIC_BEGIN:
     case ATOMIC_END:
     case LOCATION:

src/analyses/local_may_alias.cpp

@@ -423,9 +423,9 @@ void local_may_aliast::build(const goto_functiont &goto_function)
     case THROW:
       DATA_INVARIANT(false, "Exceptions must be removed before analysis");
       break;
-    case RETURN:
+    case SET_RETURN_VALUE:
 #if 0
-      DATA_INVARIANT(false, "Returns must be removed before analysis");
+      DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
 #endif
       break;
     case GOTO:         // Ignoring the guard is a valid over-approximation

src/analyses/local_safe_pointers.cpp

@@ -116,7 +116,7 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
     case ASSERT:
     case SKIP:
     case LOCATION:
-    case RETURN:
+    case SET_RETURN_VALUE:
     case THROW:
     case CATCH:
     case END_FUNCTION:

src/analyses/uncaught_exceptions_analysis.cpp

@@ -132,7 +132,7 @@ void uncaught_exceptions_domaint::transform(
   case DEAD:   // Safe to ignore in this context
   case ASSIGN: // Safe to ignore in this context
     break;
-  case RETURN:
+  case SET_RETURN_VALUE:
 #if 0
     DATA_INVARIANT(false, "Returns must be removed before analysis");
 #endif

src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

@@ -140,8 +140,8 @@ void variable_sensitivity_domaint::transform(
     // Can ignore
     break;
 
-  case RETURN:
-    throw "return instructions should be removed first";
+  case SET_RETURN_VALUE:
+    throw "the SET_RETURN_VALUE instructions should be removed first";
 
   case START_THREAD:
   case END_THREAD:

src/goto-instrument/dot.cpp

@@ -155,10 +155,9 @@ void dott::write_dot_subgraph(
         function_calls.push_back(
           std::pair<std::string, exprt>(ss.str(), function_call.function()));
       }
-      else if(it->is_assign() ||
-              it->is_decl() ||
-              it->is_return() ||
-              it->is_other())
+      else if(
+        it->is_assign() || it->is_decl() || it->is_set_return_value() ||
+        it->is_other())
       {
         std::string t = from_expr(ns, function_id, it->get_code());
         while(t[ t.size()-1 ]=='\n')

src/goto-instrument/function.cpp

@@ -125,7 +125,7 @@ void function_exit(
 
     Forall_goto_program_instructions(i_it, body)
     {
-      if(i_it->is_return())
+      if(i_it->is_set_return_value())
       {
         goto_programt::instructiont call = goto_programt::make_function_call(
           function_to_call(goto_model.symbol_table, id, gf_entry.first));
@@ -142,17 +142,17 @@ void function_exit(
     assert(last->is_end_function());
 
     // is there already a return?
-    bool has_return=false;
+    bool has_set_return_value = false;
 
     if(last!=body.instructions.begin())
     {
       goto_programt::targett before_last=last;
       --before_last;
-      if(before_last->is_return())
-        has_return=true;
+      if(before_last->is_set_return_value())
+        has_set_return_value = true;
     }
 
-    if(!has_return)
+    if(!has_set_return_value)
     {
       goto_programt::instructiont call = goto_programt::make_function_call(
         function_to_call(goto_model.symbol_table, id, gf_entry.first));

src/goto-instrument/goto_program2code.cpp

@@ -180,8 +180,8 @@ goto_programt::const_targett goto_program2codet::convert_instruction(
     case ASSIGN:
       return convert_assign(target, upper_bound, dest);
 
-    case RETURN:
-      return convert_return(target, upper_bound, dest);
+    case SET_RETURN_VALUE:
+      return convert_set_return_value(target, upper_bound, dest);
 
     case DECL:
       return convert_decl(target, upper_bound, dest);
@@ -410,7 +410,7 @@ void goto_program2codet::convert_assign_rec(
     dest.add(assign);
 }
 
-goto_programt::const_targett goto_program2codet::convert_return(
+goto_programt::const_targett goto_program2codet::convert_set_return_value(
   goto_programt::const_targett target,
   goto_programt::const_targett upper_bound,
   code_blockt &dest)

src/goto-instrument/goto_program2code.h

@@ -141,7 +141,7 @@ class goto_program2codet
 
   void convert_assign_rec(const code_assignt &assign, code_blockt &dest);
 
-  goto_programt::const_targett convert_return(
+  goto_programt::const_targett convert_set_return_value(
     goto_programt::const_targett target,
     goto_programt::const_targett upper_bound,
     code_blockt &dest);

src/goto-instrument/points_to.cpp

@@ -58,7 +58,7 @@ bool points_tot::transform(const cfgt::nodet &e)
 
   switch(instruction.type)
   {
-  case RETURN:
+  case SET_RETURN_VALUE:
     // TODO
     break;
 

src/goto-instrument/wmm/goto2graph.cpp

@@ -260,7 +260,7 @@ void instrumentert::cfg_visitort::visit_cfg_function(
       ); // NOLINT(whitespace/parens)
     }
 #ifdef CONTEXT_INSENSITIVE
-    else if(instruction.is_return())
+    else if(instruction.is_set_return_value())
     {
       visit_cfg_propagate(i_it);
       add_all_pos(it, out_nodes[function_id], in_pos[i_it]);
@@ -1227,13 +1227,10 @@ void inline instrumentert::add_instr_to_interleaving(
   goto_programt::instructionst::iterator it,
   goto_programt &interleaving)
 {
-  if(it->is_return() ||
-     it->is_throw() ||
-     it->is_catch() ||
-     it->is_skip() ||
-     it->is_dead() ||
-     it->is_start_thread() ||
-     it->is_end_thread())
+  if(
+    it->is_set_return_value() || it->is_throw() || it->is_catch() ||
+    it->is_skip() || it->is_dead() || it->is_start_thread() ||
+    it->is_end_thread())
     return;
 
   if(it->is_atomic_begin() ||

src/goto-programs/cfg.h

@@ -507,7 +507,7 @@ void cfg_baset<T, P, I>::compute_edges(
   case ASSIGN:
   case ASSERT:
   case OTHER:
-  case RETURN:
+  case SET_RETURN_VALUE:
   case SKIP:
   case LOCATION:
   case ATOMIC_BEGIN:

src/goto-programs/goto_convert_functions.cpp

@@ -119,7 +119,7 @@ void goto_convert_functionst::add_return(
       }
 
       // return?
-      if(last_instruction->is_return())
+      if(last_instruction->is_set_return_value())
         return;
 
       // advance if it's a 'dead' without branch target

src/goto-programs/goto_functions.cpp

@@ -138,7 +138,7 @@ void goto_functionst::validate(const namespacet &ns, const validation_modet vm)
       {
         DATA_CHECK(
           vm,
-          !instruction.is_return(),
+          !instruction.is_set_return_value(),
           "void function should not return a value");
       }
     }

src/goto-programs/goto_inline_class.cpp

@@ -155,7 +155,7 @@ void goto_inlinet::replace_return(
       it!=dest.instructions.end();
       it++)
   {
-    if(it->is_return())
+    if(it->is_set_return_value())
     {
       if(lhs.is_not_nil())
       {