clean out goto_symext::symex_fkt

The method is no longer in use.

Author: kroening

src/goto-symex/goto_symex.h

@@ -442,10 +442,6 @@ class goto_symext
   virtual void symex_end_of_function(statet &);
 
   /// Symbolic execution of a call to a function call.
-  /// For functions starting with \c __CPROVER_fkt
-  /// \ref goto_symext::symex_fkt
-  /// For non-special functions see
-  /// \ref goto_symext::symex_function_call_code
   /// \param get_goto_function: The delegate to retrieve function bodies (see
   ///   \ref get_goto_functiont)
   /// \param state: Symbolic execution state for current instruction
@@ -754,16 +750,7 @@ class goto_symext
   /// \param code: right-hand side containing side effect
   virtual void
   symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code);
-  /// Symbolically execute a FUNCTION_CALL instruction for a function whose
-  /// name starts with CPROVER_FKT_PREFIX
-  /// \remarks
-  /// While the name seems to imply that this would be called when symbolic
-  /// execution doesn't know what to do, it may actually be derived from a
-  /// German abbreviation for function.
-  /// This should not be called as these functions should already be removed
-  /// \param state: Symbolic execution state for current instruction
-  /// \param code: The function call instruction
-  virtual void symex_fkt(statet &state, const code_function_callt &code);
+
   /// Symbolically execute an OTHER instruction that does a CPP `printf`
   /// \param state: Symbolic execution state for current instruction
   /// \param rhs: The cleaned up CPP `printf` instruction

src/goto-symex/symex_builtin_functions.cpp

@@ -534,28 +534,3 @@ void goto_symext::symex_cpp_delete(
   bool do_array=code.get(ID_statement)==ID_cpp_delete_array;
   #endif
 }
-
-void goto_symext::symex_fkt(
-  statet &,
-  const code_function_callt &)
-{
-  // TODO: uncomment this line when TG-4667 is done
-  // UNREACHABLE;
-  #if 0
-  exprt new_fc(ID_function, fc.type());
-
-  new_fc.reserve_operands(fc.operands().size()-1);
-
-  bool first=true;
-
-  Forall_operands(it, fc)
-    if(first)
-      first=false;
-    else
-      new_fc.add_to_operands(std::move(*it));
-
-  new_fc.set(ID_identifier, fc.op0().get(ID_identifier));
-
-  fc.swap(new_fc);
-  #endif
-}

src/goto-symex/symex_function_call.cpp

@@ -203,15 +203,7 @@ void goto_symext::symex_function_call_symbol(
 
   PRECONDITION(code.function().id() == ID_symbol);
 
-  const irep_idt &identifier=
-    to_symbol_expr(code.function()).get_identifier();
-
-  if(has_prefix(id2string(identifier), CPROVER_FKT_PREFIX))
-  {
-    symex_fkt(state, code);
-  }
-  else
-    symex_function_call_code(get_goto_function, state, code);
+  symex_function_call_code(get_goto_function, state, code);
 }
 
 void goto_symext::symex_function_call_code(