find_symbols kindt: clarify enum entries

"F_BOTH" is not a good fit when there are three (and not two) other
entries. While at it, also add support to selectively choose current or
next expression symbols.

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

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_BOTH))
+      if(has_symbol(get_original_name(e), identifier, kindt::F_EXPR_BOTH))
       {
         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_BOTH))
+      if(has_symbol(e, lhs_identifier, kindt::F_EXPR_BOTH))
       {
         may_alias = true;
         break;

src/util/find_symbols.cpp

@@ -95,11 +95,19 @@ void find_symbols(kindt kind, const exprt &src, find_symbols_sett &dest)
 
   find_symbols(kind, src.type(), dest);
 
-  if(kind==kindt::F_BOTH || kind==kindt::F_EXPR)
+  if(
+    kind == kindt::F_ALL || kind == kindt::F_EXPR_CURRENT ||
+    kind == kindt::F_EXPR_BOTH)
   {
     if(src.id() == ID_symbol)
       dest.insert(to_symbol_expr(src).get_identifier());
-    else if(src.id() == ID_next_symbol)
+  }
+
+  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));
   }
 
@@ -146,10 +154,6 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
     for(const auto &p : code_type.parameters())
     {
       find_symbols(kind, p, dest);
-
-      // irep_idt identifier=it->get_identifier();
-      // if(!identifier.empty() && (kind==F_TYPE || kind==F_BOTH))
-      //  dest.insert(identifier);
     }
   }
   else if(src.id()==ID_array)
@@ -204,10 +208,10 @@ void find_non_pointer_type_symbols(
 
 void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
 {
-  find_symbols(kindt::F_BOTH, src, dest);
+  find_symbols(kindt::F_ALL, src, dest);
 }
 
 void find_type_and_expr_symbols(const typet &src, find_symbols_sett &dest)
 {
-  find_symbols(kindt::F_BOTH, src, dest);
+  find_symbols(kindt::F_ALL, src, dest);
 }

src/util/find_symbols.h

@@ -32,9 +32,13 @@ enum class kindt
   /// pointer.
   F_TYPE_NON_PTR,
   /// Symbol expressions.
-  F_EXPR,
+  F_EXPR_CURRENT,
+  /// Next-state symbol expressions.
+  F_EXPR_NEXT,
   /// Current or next-state symbol expressions.
-  F_BOTH,
+  F_EXPR_BOTH,
+  /// All of the above.
+  F_ALL
 };
 
 /// Returns true if one of the symbols in \p src with identifier \p identifier