Remove support for ID_next_symbol

This is never used in CBMC's code base.

Author: tautschnig

src/ansi-c/expr2c.cpp

@@ -1663,9 +1663,6 @@ std::string expr2ct::convert_symbol(const exprt &src)
     #endif
   }
 
-  if(src.id()==ID_next_symbol)
-    dest="NEXT("+dest+")";
-
   return dest;
 }
 
@@ -3850,9 +3847,6 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_symbol)
     return convert_symbol(src);
 
-  else if(src.id()==ID_next_symbol)
-    return convert_symbol(src);
-
   else if(src.id()==ID_nondet_symbol)
     return convert_nondet_symbol(to_nondet_symbol_expr(src));
 

src/ansi-c/goto_check_c.cpp

@@ -466,7 +466,7 @@ void goto_check_ct::invalidate(const exprt &lhs)
     for(auto it = assertions.begin(); it != assertions.end();)
     {
       if(
-        has_symbol(it->second, lhs_id, kindt::F_EXPR_CURRENT) ||
+        has_symbol(it->second, lhs_id, kindt::F_EXPR) ||
         has_subexpr(it->second, ID_dereference))
       {
         it = assertions.erase(it);

src/goto-programs/slice_global_inits.cpp

@@ -64,7 +64,7 @@ void slice_global_inits(
     for(const auto &i : it->second.body.instructions)
     {
       i.apply([&symbols_to_keep](const exprt &expr) {
-        find_symbols(expr, symbols_to_keep, true, false);
+        find_symbols(expr, symbols_to_keep);
       });
     }
   }
@@ -103,7 +103,7 @@ void slice_global_inits(
           symbols_to_keep.find(id) != symbols_to_keep.end())
         {
           fixed_point_reached = false;
-          find_symbols(instruction.assign_rhs(), symbols_to_keep, true, false);
+          find_symbols(instruction.assign_rhs(), symbols_to_keep);
           *seen_it = true;
         }
       }

src/goto-symex/postcondition.cpp

@@ -167,7 +167,7 @@ bool postconditiont::is_used(
     for(const exprt &e :
         value_set.get_value_set(to_dereference_expr(expr).pointer(), ns))
     {
-      if(has_symbol(get_original_name(e), identifier, kindt::F_EXPR_BOTH))
+      if(has_symbol(get_original_name(e), identifier, kindt::F_EXPR))
       {
         return true;
       }

src/goto-symex/precondition.cpp

@@ -117,7 +117,7 @@ void preconditiont::compute_rec(exprt &dest)
     for(const exprt &e : value_sets.get_values(
           SSA_step.source.function_id, target, deref_expr.pointer()))
     {
-      if(has_symbol(e, lhs_identifier, kindt::F_EXPR_BOTH))
+      if(has_symbol(e, lhs_identifier, kindt::F_EXPR))
       {
         may_alias = true;
         break;

src/util/find_macros.cpp

@@ -42,19 +42,6 @@ void find_macros(
           stack.push(&symbol.value);
       }
     }
-    else if(e.id() == ID_next_symbol)
-    {
-      const irep_idt &identifier=e.get(ID_identifier);
-
-      const symbolt &symbol=ns.lookup(identifier);
-
-      if(symbol.is_macro)
-      {
-        // inserted?
-        if(dest.insert(identifier).second)
-          stack.push(&symbol.value);
-      }
-    }
     else
     {
       forall_operands(it, e)

src/util/find_symbols.cpp

@@ -13,33 +13,20 @@ Author: Daniel Kroening, [email protected]
 #include "range.h"
 #include "std_expr.h"
 
-bool has_symbol(
-  const exprt &src,
-  const find_symbols_sett &symbols,
-  bool current,
-  bool next)
+bool has_symbol(const exprt &src, const find_symbols_sett &symbols)
 {
-  if(src.id() == ID_symbol && current)
+  if(src.id() == ID_symbol)
     return symbols.count(to_symbol_expr(src).get_identifier()) != 0;
-  else if(src.id() == ID_next_symbol && next)
-    return symbols.count(src.get(ID_identifier))!=0;
   else
   {
     forall_operands(it, src)
-      if(has_symbol(*it, symbols, current, next))
+      if(has_symbol(*it, symbols))
         return true;
   }
 
   return false;
 }
 
-bool has_symbol(
-  const exprt &src,
-  const find_symbols_sett &symbols)
-{
-  return has_symbol(src, symbols, true, true);
-}
-
 void find_symbols(
   const exprt &src,
   std::set<symbol_exprt> &dest)
@@ -76,22 +63,12 @@ void find_symbols(kindt kind, const exprt &src, find_symbols_sett &dest)
 
   find_symbols(kind, src.type(), dest);
 
-  if(
-    kind == kindt::F_ALL || kind == kindt::F_EXPR_CURRENT ||
-    kind == kindt::F_EXPR_BOTH)
+  if(kind == kindt::F_ALL || kind == kindt::F_EXPR)
   {
     if(src.id() == ID_symbol)
       dest.insert(to_symbol_expr(src).get_identifier());
   }
 
-  if(
-    kind == kindt::F_ALL || kind == kindt::F_EXPR_NEXT ||
-    kind == kindt::F_EXPR_BOTH)
-  {
-    if(src.id() == ID_next_symbol)
-      dest.insert(src.get(ID_identifier));
-  }
-
   const irept &c_sizeof_type=src.find(ID_C_c_sizeof_type);
 
   if(c_sizeof_type.is_not_nil())
@@ -199,22 +176,10 @@ void find_type_and_expr_symbols(const typet &src, find_symbols_sett &dest)
 
 void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
 {
-  find_symbols(kindt::F_EXPR_BOTH, src, dest);
+  find_symbols(kindt::F_EXPR, src, dest);
 }
 
-void find_symbols(
-  const exprt &src,
-  find_symbols_sett &dest,
-  bool current,
-  bool next)
+void find_symbols(const exprt &src, find_symbols_sett &dest)
 {
-  if(current)
-  {
-    if(next)
-      find_symbols(kindt::F_EXPR_BOTH, src, dest);
-    else
-      find_symbols(kindt::F_EXPR_CURRENT, src, dest);
-  }
-  else if(next)
-    find_symbols(kindt::F_EXPR_NEXT, src, dest);
+  find_symbols(kindt::F_EXPR, src, dest);
 }

src/util/find_symbols.h

@@ -32,11 +32,7 @@ enum class kindt
   /// pointer.
   F_TYPE_NON_PTR,
   /// Symbol expressions.
-  F_EXPR_CURRENT,
-  /// Next-state symbol expressions.
-  F_EXPR_NEXT,
-  /// Current or next-state symbol expressions.
-  F_EXPR_BOTH,
+  F_EXPR,
   /// All of the above.
   F_ALL
 };
@@ -50,13 +46,8 @@ DEPRECATED(SINCE(2022, 3, 14, "use find_symbols"))
 /// ID_next_symbol
 void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest);
 
-/// Add to the set \p dest the sub-expressions of \p src with id ID_symbol if
-/// \p current is true, and ID_next_symbol if \p next is true
-void find_symbols(
-  const exprt &src,
-  find_symbols_sett &dest,
-  bool current = true,
-  bool next = true);
+/// Add to the set \p dest the sub-expressions of \p src with id ID_symbol.
+void find_symbols(const exprt &src, find_symbols_sett &dest);
 
 /// \return set of sub-expressions of the expressions contained in the range
 ///   defined by \p begin and \p end which have id ID_symbol or ID_next_symbol
@@ -72,14 +63,6 @@ find_symbols_sett find_symbols_or_nexts(iteratort begin, iteratort end)
   return result;
 }
 
-/// Add to the set \p dest the sub-expressions of \p src with id ID_symbol if
-/// \p current is true, and ID_next_symbol if \p next is true
-void find_symbols(
-  const exprt &src,
-  find_symbols_sett &dest,
-  bool current,
-  bool next);
-
 /// Find sub expressions with id ID_symbol
 void find_symbols(
   const exprt &src,

src/util/irep_ids.def

@@ -58,7 +58,6 @@ IREP_ID_ONE(bitxnor)
 IREP_ID_ONE(notequal)
 IREP_ID_ONE(if)
 IREP_ID_ONE(symbol)
-IREP_ID_ONE(next_symbol)
 IREP_ID_ONE(nondet_symbol)
 IREP_ID_ONE(predicate_symbol)
 IREP_ID_ONE(predicate_next_symbol)