Remove unused case of return assignment in symex

The return instructions should have been removed by return-value
removal, so they should not reach symex.
We replace this case by an unreachable statement and remove the method
that is now unused.

Author: romainbrenguier

src/goto-symex/goto_symex.h

@@ -275,11 +275,6 @@ class goto_symext
 
   virtual void loop_bound_exceeded(statet &, const exprt &guard);
 
-  /// Assuming the program counter of \p state is currently pointing to a return
-  /// instruction, assign the value in that return to the top frame's
-  /// \p return_value field.
-  void return_assignment(statet &);
-
   virtual void no_body(const irep_idt &)
   {
   }

src/goto-symex/symex_function_call.cpp

@@ -447,28 +447,3 @@ static void locality(
   }
 }
 
-void goto_symext::return_assignment(statet &state)
-{
-  framet &frame = state.top();
-
-  const goto_programt::instructiont &instruction=*state.source.pc;
-  PRECONDITION(instruction.is_return());
-  const code_returnt &code = instruction.get_return();
-
-  target.location(state.guard.as_expr(), state.source);
-
-  PRECONDITION(code.operands().size() == 1 || frame.return_value.is_nil());
-
-  exprt value = code.return_value();
-
-  if(frame.return_value.is_not_nil())
-  {
-    code_assignt assignment(frame.return_value, value);
-
-    INVARIANT(
-      base_type_eq(assignment.lhs().type(), assignment.rhs().type(), ns),
-      "goto_symext::return_assignment type mismatch");
-
-    symex_assign(state, assignment);
-  }
-}

src/goto-symex/symex_main.cpp

@@ -441,10 +441,8 @@ void goto_symext::symex_step(
     break;
 
   case RETURN:
-    if(!state.guard.is_false())
-      return_assignment(state);
-
-    symex_transition(state);
+    // This case should have been removed by return-value removal
+    UNREACHABLE;
     break;
 
   case ASSIGN: