Restrict has_symbol to symbol expressions and rename it to has_symbol_expr

With the removal of support for ID_next_symbol all uses of `has_symbol`
searched for symbol expressions only.

Author: tautschnig

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, symbol_kindt::F_EXPR) ||
+        has_symbol_expr(it->second, lhs_id) ||
         has_subexpr(it->second, ID_dereference))
       {
         it = assertions.erase(it);

src/goto-symex/postcondition.cpp

@@ -167,10 +167,8 @@ 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, symbol_kindt::F_EXPR))
-      {
+      if(has_symbol_expr(get_original_name(e), identifier))
         return true;
-      }
     }
 
     return false;

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, symbol_kindt::F_EXPR))
+      if(has_symbol_expr(e, lhs_identifier))
       {
         may_alias = true;
         break;

src/util/find_symbols.cpp

@@ -13,6 +13,22 @@ Author: Daniel Kroening, [email protected]
 #include "range.h"
 #include "std_expr.h"
 
+/// Kinds of symbols to be considered by \ref has_symbol or \ref find_symbols.
+enum class symbol_kindt
+{
+  /// Struct, union, or enum tag symbols.
+  F_TYPE,
+  /// Struct, union, or enum tag symbols when the expression using them is not a
+  /// pointer.
+  F_TYPE_NON_PTR,
+  /// Symbol expressions.
+  F_EXPR,
+  /// Symbol expressions, but excluding bindings.
+  F_EXPR_NOT_BOUND,
+  /// All of the above.
+  F_ALL
+};
+
 bool has_symbol(const exprt &src, const find_symbols_sett &symbols)
 {
   if(src.id() == ID_symbol)
@@ -164,9 +180,9 @@ void find_symbols(const exprt &src, std::set<symbol_exprt> &dest)
   });
 }
 
-bool has_symbol(const exprt &src, const irep_idt &identifier, symbol_kindt kind)
+bool has_symbol_expr(const exprt &src, const irep_idt &identifier)
 {
-  return !find_symbols(kind, src, [&identifier](const symbol_exprt &e) {
+  return !find_symbols(symbol_kindt::F_EXPR, src, [&identifier](const symbol_exprt &e) {
     return e.get_identifier() != identifier;
   });
 }

src/util/find_symbols.h

@@ -23,26 +23,9 @@ class typet;
 
 typedef std::unordered_set<irep_idt> find_symbols_sett;
 
-/// Kinds of symbols to be considered by \ref has_symbol or \ref find_symbols.
-enum class symbol_kindt
-{
-  /// Struct, union, or enum tag symbols.
-  F_TYPE,
-  /// Struct, union, or enum tag symbols when the expression using them is not a
-  /// pointer.
-  F_TYPE_NON_PTR,
-  /// Symbol expressions.
-  F_EXPR,
-  /// All of the above.
-  F_ALL
-};
-
-/// Returns true if one of the symbols in \p src with identifier \p identifier
-/// is of kind \p kind.
-bool has_symbol(
-  const exprt &src,
-  const irep_idt &identifier,
-  symbol_kindt kind);
+/// Returns true if one of the symbol expressions in \p src has identifier
+/// \p identifier.
+bool has_symbol_expr(const exprt &src, const irep_idt &identifier);
 
 DEPRECATED(SINCE(2022, 3, 14, "use find_symbols"))
 /// Add to the set \p dest the sub-expressions of \p src with id ID_symbol or
@@ -87,7 +70,7 @@ inline find_symbols_sett find_symbol_identifiers(const exprt &src)
   return identifiers;
 }
 
-DEPRECATED(SINCE(2022, 3, 14, "use has_symbol(exprt, irep_idt, symbol_kindt)"))
+DEPRECATED(SINCE(2022, 3, 14, "use has_symbol_expr(exprt, irep_idt, bool)"))
 /// \return true if one of the symbols in \p src is present in \p symbols
 bool has_symbol(
   const exprt &src,