Factor out value_sett::get_entry_for_symbol

Make this a separate function so it can be used from other places.
No change in behaviour.

Author: Owen

src/goto-symex/goto_symex.h

@@ -315,6 +315,28 @@ class goto_symext
   virtual void symex_other(statet &state);
 
   void symex_assert(const goto_programt::instructiont &, statet &);
+
+  /// Try to filter value sets based on whether possible values of a
+  /// pointer-typed symbol make the condition true or false. We only do this
+  /// when there is only one pointer-typed symbol in \p condition.
+  /// \param state: The current state
+  /// \param condition: The condition which is being evaluated, which it expects
+  ///   will not have been cleaned or renamed. In practice, it's fine if it has
+  ///   been cleaned and renamed up to level L1.
+  /// \param value_set_for_true_case: A pointer to the value set that possible
+  ///   values should be removed from if they make the condition false, or
+  ///   nullptr if this shouldn't be done
+  /// \param value_set_for_false_case: A pointer to the value set that possible
+  ///   values should be removed from if they make the condition true, or
+  ///   nullptr if this shouldn't be done
+  /// \param ns: A namespace
+  void try_filter_value_sets(
+    goto_symex_statet &state,
+    exprt condition,
+    value_sett *value_set_for_true_case,
+    value_sett *value_set_for_false_case,
+    const namespacet &ns);
+
   virtual void vcc(
     const exprt &,
     const std::string &msg,

src/pointer-analysis/value_set.cpp

@@ -366,6 +366,54 @@ static std::string strip_first_field_from_suffix(
   return suffix.substr(field.length() + 1);
 }
 
+const value_sett::entryt *value_sett::get_entry_for_symbol(
+  const irep_idt identifier,
+  const typet &type,
+  const std::string &suffix,
+  const namespacet &ns) const
+{
+  if(
+    type.id() != ID_pointer && type.id() != ID_signedbv &&
+    type.id() != ID_unsignedbv && type.id() != ID_array &&
+    type.id() != ID_struct && type.id() != ID_struct_tag &&
+    type.id() != ID_union && type.id() != ID_union_tag)
+  {
+    return nullptr;
+  }
+
+  const typet &followed_type = type.id() == ID_struct_tag
+                                 ? ns.follow_tag(to_struct_tag_type(type))
+                                 : type.id() == ID_union_tag
+                                     ? ns.follow_tag(to_union_tag_type(type))
+                                     : type;
+
+  // look it up
+  const value_sett::entryt *entry = find_entry(id2string(identifier) + suffix);
+
+  // try first component name as suffix if not yet found
+  if(
+    !entry &&
+    (followed_type.id() == ID_struct || followed_type.id() == ID_union))
+  {
+    const struct_union_typet &struct_union_type =
+      to_struct_union_type(followed_type);
+
+    const irep_idt &first_component_name =
+      struct_union_type.components().front().get_name();
+
+    entry = find_entry(
+      id2string(identifier) + "." + id2string(first_component_name) + suffix);
+  }
+
+  if(!entry)
+  {
+    // not found? try without suffix
+    entry = find_entry(identifier);
+  }
+
+  return entry;
+}
+
 void value_sett::get_value_set_rec(
   const exprt &expr,
   object_mapt &dest,
@@ -413,43 +461,11 @@ void value_sett::get_value_set_rec(
   }
   else if(expr.id()==ID_symbol)
   {
-    irep_idt identifier=to_symbol_expr(expr).get_identifier();
-
-    // is it a pointer, integer, array or struct?
-    if(expr_type.id()==ID_pointer ||
-       expr_type.id()==ID_signedbv ||
-       expr_type.id()==ID_unsignedbv ||
-       expr_type.id()==ID_struct ||
-       expr_type.id()==ID_union ||
-       expr_type.id()==ID_array)
-    {
-      // look it up
-      const entryt *entry =
-        find_entry(id2string(identifier) + suffix);
-
-      // try first component name as suffix if not yet found
-      if(!entry && (expr_type.id() == ID_struct || expr_type.id() == ID_union))
-      {
-        const struct_union_typet &struct_union_type=
-          to_struct_union_type(expr_type);
+    const entryt *entry = get_entry_for_symbol(
+      to_symbol_expr(expr).get_identifier(), expr_type, suffix, ns);
 
-        const irep_idt &first_component_name =
-          struct_union_type.components().front().get_name();
-
-        entry = find_entry(
-          id2string(identifier) + "." + id2string(first_component_name) +
-          suffix);
-      }
-
-      // not found? try without suffix
-      if(!entry)
-        entry = find_entry(identifier);
-
-      if(entry)
-        make_union(dest, entry->object_map);
-      else
-        insert(dest, exprt(ID_unknown, original_type));
-    }
+    if(entry)
+      make_union(dest, entry->object_map);
     else
       insert(dest, exprt(ID_unknown, original_type));
   }

src/pointer-analysis/value_set.h

@@ -460,6 +460,19 @@ class value_sett
     exprt &expr,
     const namespacet &ns) const;
 
+  /// Get the entry for the symbol and suffix
+  /// \param identifier: The identifier for the symbol
+  /// \param type: The type of the symbol
+  /// \param suffix: The suffix for the entry
+  /// \param ns: The global namespace, for following \p type if it is a
+  ///   struct tag type or a union tag type
+  /// \return The entry for the symbol and suffix
+  const value_sett::entryt *get_entry_for_symbol(
+    const irep_idt identifier,
+    const typet &type,
+    const std::string &suffix,
+    const namespacet &ns) const;
+
 protected:
   /// Reads the set of objects pointed to by `expr`, including making
   /// recursive lookups for dereference operations etc.