WIP: Refine symbol well-formedness checks to handle special cases

Author: chrisr-diffblue

src/util/symbol.cpp

@@ -10,8 +10,11 @@ Author: Daniel Kroening, [email protected]
 
 #include <ostream>
 
+#include <iostream>
+
 #include "source_location.h"
 #include "std_expr.h"
+#include "string_utils.h"
 #include "suffix.h"
 
 /// Dump the state of a symbol object to a given output stream.
@@ -139,7 +142,51 @@ bool symbolt::is_well_formed() const
   // general name.
   if(!has_suffix(id2string(name), id2string(base_name)))
   {
-    return false;
+    bool criterion_must_hold = true;
+
+    // There are some special cases where this criterion doesn't hold, check
+    // to see if we have one of those cases
+
+    if (is_type)
+    {
+      // Typedefs
+      if (type.find(ID_C_typedef).is_not_nil())
+      {
+        // FIXME: Is there an additional check that can be made here, like for tag types below?
+        criterion_must_hold = false;
+      }
+
+      // Tag types
+      if (type.find(ID_tag).is_not_nil() && type.find(ID_tag).id() == base_name)
+      {
+          criterion_must_hold = false;
+      }
+    }
+
+    // Linker renaming may have added $linkN suffixes to the name, and other
+    // suffixes such as #return_value may have then be subsequently added.
+    // Strip out the first $linkN substring and then see if the criterion holds
+
+    const auto split_name = split_string(id2string(name), '$');
+    if(
+      split_name.size() > 1 && has_prefix(split_name[1], "link")) // FIXME: Should loop for all delimited?
+    {
+
+      size_t post_link_start = 4;
+      while (post_link_start < split_name[1].size() && std::isdigit(split_name[1][post_link_start]))
+        ++post_link_start;
+
+      const auto stripped_name = split_name[0] + split_name[1].substr(post_link_start,split_name[1].size());
+
+      if (has_suffix(stripped_name, id2string(base_name)))
+        criterion_must_hold = false;
+    }
+
+    if (criterion_must_hold)
+    {
+      // For all other cases this criterion should hold
+      return false;
+    }
   }
 
   return true;