remove CBMC_trace

This has no known users.

Author: Daniel Kroening

src/ansi-c/cprover_builtin_headers.h

@@ -33,9 +33,6 @@ void __CPROVER_atomic_begin();
 void __CPROVER_atomic_end();
 void __CPROVER_fence(const char *kind, ...);
 
-// traces
-void CBMC_trace(int lvl, const char *event, ...);
-
 // pointers
 __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *);
 __CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *);

src/goto-symex/goto_symex.h

@@ -468,8 +468,7 @@ class goto_symext
   virtual void symex_end_of_function(statet &);
 
   /// Symbolic execution of a call to a function call.
-  /// For functions \c CBMC_trace and functions starting with \c __CPROVER_fkt
-  /// see \ref goto_symext::symex_trace and
+  /// For functions starting with \c __CPROVER_fkt
   /// \ref goto_symext::symex_fkt
   /// For non-special functions see
   /// \ref goto_symext::symex_function_call_code
@@ -678,11 +677,6 @@ class goto_symext
   /// \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 a FUNCTION_CALL instruction for the `CBMC_trace`
-  /// function
-  /// \param state: Symbolic execution state for current instruction
-  /// \param code: The function call instruction
-  virtual void symex_trace(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

@@ -545,38 +545,6 @@ void goto_symext::symex_cpp_delete(
   #endif
 }
 
-void goto_symext::symex_trace(
-  statet &state,
-  const code_function_callt &code)
-{
-  PRECONDITION(code.arguments().size() >= 2);
-
-  mp_integer debug_lvl;
-  optionalt<mp_integer> maybe_debug =
-    numeric_cast<mp_integer>(code.arguments()[0]);
-  DATA_INVARIANT(
-    maybe_debug.has_value(), "CBMC_trace expects constant as first argument");
-  debug_lvl = maybe_debug.value();
-
-  DATA_INVARIANT(
-    code.arguments()[1].id() == "implicit_address_of" &&
-      code.arguments()[1].operands().size() == 1 &&
-      code.arguments()[1].op0().id() == ID_string_constant,
-    "CBMC_trace expects string constant as second argument");
-
-  if(symex_config.debug_level >= debug_lvl)
-  {
-    std::list<renamedt<exprt, L2>> vars;
-
-    irep_idt event = to_string_constant(code.arguments()[1].op0()).get_value();
-
-    for(std::size_t j=2; j<code.arguments().size(); j++)
-      vars.push_back(state.rename(code.arguments()[j], ns));
-
-    target.output(state.guard.as_expr(), state.source, event, vars);
-  }
-}
-
 void goto_symext::symex_fkt(
   statet &,
   const code_function_callt &)

src/goto-symex/symex_function_call.cpp

@@ -211,11 +211,7 @@ void goto_symext::symex_function_call_symbol(
   const irep_idt &identifier=
     to_symbol_expr(code.function()).get_identifier();
 
-  if(identifier=="CBMC_trace")
-  {
-    symex_trace(state, code);
-  }
-  else if(has_prefix(id2string(identifier), CPROVER_FKT_PREFIX))
+  if(has_prefix(id2string(identifier), CPROVER_FKT_PREFIX))
   {
     symex_fkt(state, code);
   }