Merge pull request #4427 from tautschnig/remove-long-deprecated-methods

Remove long deprecated methods

Author: tautschnig

src/goto-harness/recursive_initialization.cpp

@@ -164,7 +164,8 @@ void recursive_initializationt::initialize_nondet(
     lhs.id() != ID_symbol ||
     !is_array_size_parameter(to_symbol_expr(lhs).get_identifier()))
   {
-    body.add(code_assignt{lhs, side_effect_expr_nondett{lhs.type()}});
+    body.add(code_assignt{
+      lhs, side_effect_expr_nondett{lhs.type(), source_locationt{}}});
   }
 }
 

src/goto-instrument/cover.cpp

@@ -18,7 +18,6 @@ Date: May 2016
 #include <util/make_unique.h>
 #include <util/cmdline.h>
 #include <util/options.h>
-#include <util/deprecate.h>
 
 #include <goto-programs/remove_skip.h>
 
@@ -49,33 +48,6 @@ void instrument_cover_goals(
   instrumenters(function_id, goto_program, *basic_blocks);
 }
 
-/// Instruments goto program for a given coverage criterion
-/// \param symbol_table: the symbol table
-/// \param function_id: name of \p goto_program
-/// \param goto_program: the goto program
-/// \param criterion: the coverage criterion
-/// \param message_handler: a message handler
-/// \deprecated use instrument_cover_goals(goto_programt &goto_program,
-/// const cover_instrumenterst &instrumenters,
-/// message_handlert &message_handler, const irep_idt mode) instead
-DEPRECATED(SINCE(2018, 2, 9, "use instrument_cover_goals goto_programt &..."))
-void instrument_cover_goals(
-  const symbol_tablet &symbol_table,
-  const irep_idt &function_id,
-  goto_programt &goto_program,
-  coverage_criteriont criterion,
-  message_handlert &message_handler)
-{
-  goal_filterst goal_filters;
-  goal_filters.add(util_make_unique<internal_goals_filtert>(message_handler));
-
-  cover_instrumenterst instrumenters;
-  instrumenters.add_from_criterion(criterion, symbol_table, goal_filters);
-
-  instrument_cover_goals(
-    function_id, goto_program, instrumenters, ID_unknown, message_handler);
-}
-
 /// Create and add an instrumenter based on the given criterion
 /// \param criterion: the coverage criterion
 /// \param symbol_table: the symbol table

src/goto-symex/ssa_step.cpp

@@ -7,120 +7,8 @@ Author: Romain Brenguier <[email protected]>
 *******************************************************************/
 
 #include "ssa_step.h"
-#include <langapi/language_util.h>
-#include <util/format_expr.h>
-
-void SSA_stept::output(const namespacet &ns, std::ostream &out) const
-{
-  out << "Thread " << source.thread_nr;
-
-  if(source.pc->source_location.is_not_nil())
-    out << " " << source.pc->source_location << '\n';
-  else
-    out << '\n';
 
-  switch(type)
-  {
-  case goto_trace_stept::typet::ASSERT:
-    out << "ASSERT " << from_expr(ns, source.function_id, cond_expr) << '\n';
-    break;
-  case goto_trace_stept::typet::ASSUME:
-    out << "ASSUME " << from_expr(ns, source.function_id, cond_expr) << '\n';
-    break;
-  case goto_trace_stept::typet::LOCATION:
-    out << "LOCATION" << '\n';
-    break;
-  case goto_trace_stept::typet::INPUT:
-    out << "INPUT" << '\n';
-    break;
-  case goto_trace_stept::typet::OUTPUT:
-    out << "OUTPUT" << '\n';
-    break;
-
-  case goto_trace_stept::typet::DECL:
-    out << "DECL" << '\n';
-    out << from_expr(ns, source.function_id, ssa_lhs) << '\n';
-    break;
-
-  case goto_trace_stept::typet::ASSIGNMENT:
-    out << "ASSIGNMENT (";
-    switch(assignment_type)
-    {
-    case symex_targett::assignment_typet::HIDDEN:
-      out << "HIDDEN";
-      break;
-    case symex_targett::assignment_typet::STATE:
-      out << "STATE";
-      break;
-    case symex_targett::assignment_typet::VISIBLE_ACTUAL_PARAMETER:
-      out << "VISIBLE_ACTUAL_PARAMETER";
-      break;
-    case symex_targett::assignment_typet::HIDDEN_ACTUAL_PARAMETER:
-      out << "HIDDEN_ACTUAL_PARAMETER";
-      break;
-    case symex_targett::assignment_typet::PHI:
-      out << "PHI";
-      break;
-    case symex_targett::assignment_typet::GUARD:
-      out << "GUARD";
-      break;
-    default:
-    {
-    }
-    }
-
-    out << ")\n";
-    break;
-
-  case goto_trace_stept::typet::DEAD:
-    out << "DEAD\n";
-    break;
-  case goto_trace_stept::typet::FUNCTION_CALL:
-    out << "FUNCTION_CALL\n";
-    break;
-  case goto_trace_stept::typet::FUNCTION_RETURN:
-    out << "FUNCTION_RETURN\n";
-    break;
-  case goto_trace_stept::typet::CONSTRAINT:
-    out << "CONSTRAINT\n";
-    break;
-  case goto_trace_stept::typet::SHARED_READ:
-    out << "SHARED READ\n";
-    break;
-  case goto_trace_stept::typet::SHARED_WRITE:
-    out << "SHARED WRITE\n";
-    break;
-  case goto_trace_stept::typet::ATOMIC_BEGIN:
-    out << "ATOMIC_BEGIN\n";
-    break;
-  case goto_trace_stept::typet::ATOMIC_END:
-    out << "AUTOMIC_END\n";
-    break;
-  case goto_trace_stept::typet::SPAWN:
-    out << "SPAWN\n";
-    break;
-  case goto_trace_stept::typet::MEMORY_BARRIER:
-    out << "MEMORY_BARRIER\n";
-    break;
-  case goto_trace_stept::typet::GOTO:
-    out << "IF " << from_expr(ns, source.function_id, cond_expr) << " GOTO\n";
-    break;
-
-  default:
-    UNREACHABLE;
-  }
-
-  if(is_assert() || is_assume() || is_assignment() || is_constraint())
-    out << from_expr(ns, source.function_id, cond_expr) << '\n';
-
-  if(is_assert() || is_constraint())
-    out << comment << '\n';
-
-  if(is_shared_read() || is_shared_write())
-    out << from_expr(ns, source.function_id, ssa_lhs) << '\n';
-
-  out << "Guard: " << from_expr(ns, source.function_id, guard) << '\n';
-}
+#include <util/format_expr.h>
 
 void SSA_stept::output(std::ostream &out) const
 {

src/goto-symex/ssa_step.h

@@ -191,9 +191,6 @@ class SSA_stept
   {
   }
 
-  DEPRECATED(SINCE(2018, 4, 23, "Use output without ns param"))
-  void output(const namespacet &ns, std::ostream &out) const;
-
   void output(std::ostream &out) const;
 
   void validate(const namespacet &ns, const validation_modet vm) const;

src/goto-symex/symex_target_equation.cpp

@@ -17,9 +17,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/throw_with_nested.h>
 #include <util/unwrap_nested_exception.h>
 
-// Can be removed once deprecated SSA_stept::output is removed
-#include <langapi/language_util.h>
-
 #include <solvers/flattening/bv_conversion_exceptions.h>
 #include <solvers/prop/literal_expr.h>
 #include <solvers/prop/prop.h>
@@ -682,13 +679,11 @@ void symex_target_equationt::merge_ireps(SSA_stept &SSA_step)
   // converted_io_args is merged in convert_io
 }
 
-void symex_target_equationt::output(
-  std::ostream &out,
-  const namespacet &ns) const
+void symex_target_equationt::output(std::ostream &out) const
 {
   for(const auto &step : SSA_steps)
   {
-    step.output(ns, out);
+    step.output(out);
     out << "--------------\n";
   }
 }

src/goto-symex/symex_target_equation.h

@@ -255,7 +255,7 @@ class symex_target_equationt:public symex_targett
     return it;
   }
 
-  void output(std::ostream &out, const namespacet &ns) const;
+  void output(std::ostream &out) const;
 
   void clear()
   {

src/util/mp_arith.cpp

@@ -186,28 +186,6 @@ const mp_integer binary2integer(const std::string &n, bool is_signed)
   #endif
 }
 
-mp_integer::ullong_t integer2ulong(const mp_integer &n)
-{
-  PRECONDITION(n.is_ulong());
-  return n.to_ulong();
-}
-
-std::size_t integer2size_t(const mp_integer &n)
-{
-  PRECONDITION(n>=0 && n<=std::numeric_limits<std::size_t>::max());
-  PRECONDITION(n.is_ulong());
-  mp_integer::ullong_t ull = n.to_ulong();
-  return (std::size_t) ull;
-}
-
-unsigned integer2unsigned(const mp_integer &n)
-{
-  PRECONDITION(n>=0 && n<=std::numeric_limits<unsigned>::max());
-  PRECONDITION(n.is_ulong());
-  mp_integer::ullong_t ull = n.to_ulong();
-  return (unsigned)ull;
-}
-
 /// bitwise binary operation over two integers, given as a functor
 /// \param a: the first integer
 /// \param b: the second integer

src/util/mp_arith.h

@@ -14,7 +14,6 @@ Author: Daniel Kroening, [email protected]
 #include <string>
 
 #include "big-int/bigint.hh"
-#include "deprecate.h"
 
 // NOLINTNEXTLINE(readability/identifiers)
 typedef BigInt mp_integer;
@@ -49,17 +48,4 @@ const mp_integer string2integer(const std::string &, unsigned base=10);
 const std::string integer2binary(const mp_integer &, std::size_t width);
 const mp_integer binary2integer(const std::string &, bool is_signed);
 
-/// \deprecated use numeric_cast_v<unsigned long long> instead
-DEPRECATED(
-  SINCE(2017, 11, 13, "Use numeric_cast_v<unsigned long long> instead"))
-mp_integer::ullong_t integer2ulong(const mp_integer &);
-
-/// \deprecated use numeric_cast_v<std::size_t> instead
-DEPRECATED(SINCE(2017, 11, 13, "Use numeric_cast_v<std::size_t> instead"))
-std::size_t integer2size_t(const mp_integer &);
-
-/// \deprecated use numeric_cast_v<unsigned> instead
-DEPRECATED(SINCE(2017, 11, 13, "Use numeric_cast_v<unsigned> instead"))
-unsigned integer2unsigned(const mp_integer &);
-
 #endif // CPROVER_UTIL_MP_ARITH_H