Merge pull request #3850 from diffblue/remove_CPROVER_MACRO

remove CPROVER_MACRO and goto_symext::symex_macro

Author: tautschnig

src/goto-symex/goto_symex.h

@@ -413,7 +413,6 @@ class goto_symext
   virtual void symex_cpp_new(
     statet &, const exprt &lhs, const side_effect_exprt &);
   virtual void symex_fkt(statet &, const code_function_callt &);
-  virtual void symex_macro(statet &, const code_function_callt &);
   virtual void symex_trace(statet &, const code_function_callt &);
   virtual void symex_printf(statet &, const exprt &rhs);
   virtual void symex_input(statet &, const codet &);

src/goto-symex/symex_builtin_functions.cpp

@@ -513,40 +513,3 @@ void goto_symext::symex_fkt(
   fc.swap(new_fc);
   #endif
 }
-
-void goto_symext::symex_macro(
-  statet &,
-  const code_function_callt &code)
-{
-  const irep_idt &identifier=code.op0().get(ID_identifier);
-
-  PRECONDITION(identifier == CPROVER_MACRO_PREFIX "waitfor");
-#if 0
-  exprt new_fc("waitfor", fc.type());
-
-  if(fc.operands().size()!=4)
-    throw "waitfor expected to have four operands";
-
-  exprt &cycle_var=fc.op1();
-  exprt &bound=fc.op2();
-  exprt &predicate=fc.op3();
-
-  if(cycle_var.id()!=ID_symbol)
-    throw "waitfor expects symbol as first operand but got "+
-          cycle_var.id();
-
-  exprt new_cycle_var(cycle_var);
-  new_cycle_var.id("waitfor_symbol");
-  new_cycle_var.copy_to_operands(bound);
-
-  replace_expr(cycle_var, new_cycle_var, predicate);
-
-  new_fc.operands().resize(4);
-  new_fc.op0().swap(cycle_var);
-  new_fc.op1().swap(new_cycle_var);
-  new_fc.op2().swap(bound);
-  new_fc.op3().swap(predicate);
-
-  fc.swap(new_fc);
-#endif
-}

src/goto-symex/symex_function_call.cpp

@@ -216,10 +216,6 @@ void goto_symext::symex_function_call_symbol(
   {
     symex_fkt(state, code);
   }
-  else if(has_prefix(id2string(identifier), CPROVER_MACRO_PREFIX))
-  {
-    symex_macro(state, code);
-  }
   else
     symex_function_call_code(get_goto_function, state, code);
 }

src/util/cprover_prefix.h

@@ -14,7 +14,5 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_PREFIX "__CPROVER_"
 // NOLINTNEXTLINE(build/deprecated)
 #define CPROVER_FKT_PREFIX "__CPROVER_fkt_"
-// NOLINTNEXTLINE(build/deprecated)
-#define CPROVER_MACRO_PREFIX "__CPROVER_macro_"
 
 #endif // CPROVER_UTIL_CPROVER_PREFIX_H