Fix --nondet-static-exclude to handle symbol names and report errors

regression/goto-instrument/nondet_static_exclude_symbol_name/main.c

@@ -0,0 +1,14 @@
+int foo = 0;
+
+int f()
+{
+  static int bar = 0;
+  return bar;
+}
+
+int main()
+{
+  assert(foo == 0);
+  assert(f() == 0);
+  return 0;
+}

regression/goto-instrument/nondet_static_exclude_symbol_name/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--nondet-static --nondet-static-exclude f::1::bar --nondet-static-exclude foo
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Test that --nondet-static-exclude works with symbol names like f::1::bar and with global variable names like foo

src/goto-instrument/nondet_static.cpp

@@ -19,6 +19,7 @@ Date: November 2011
 
 #include "nondet_static.h"
 
+#include <util/exception_utils.h>
 #include <util/prefix.h>
 #include <util/std_code.h>
 
@@ -149,10 +150,22 @@ void nondet_static(
 
   for(auto const &except : except_values)
   {
-    const bool file_prefix_found = except.find(":") != std::string::npos;
+    // Check if this looks like a file:variable format
+    // We look for a single ":" that's not part of "::"
+    bool file_prefix_found = false;
+    size_t colon_pos = except.find(":");
+    if(colon_pos != std::string::npos)
+    {
+      // Check if this ":" is not part of "::"
+      if(colon_pos + 1 >= except.length() || except[colon_pos + 1] != ':')
+      {
+        file_prefix_found = true;
+      }
+    }
 
     if(file_prefix_found)
     {
+      // This is in file:variable format
       to_exclude.insert(except);
       if(has_prefix(except, "./"))
       {
@@ -165,10 +178,25 @@ void nondet_static(
     }
     else
     {
+      // This is either a simple name or a symbol identifier (with "::")
+      // Try to look it up directly in the symbol table
       irep_idt symbol_name(except);
-      symbolt lookup_results = ns.lookup(symbol_name);
-      to_exclude.insert(
-        id2string(lookup_results.location.get_file()) + ":" + except);
+      const symbolt *symbol_ptr = ns.get_symbol_table().lookup(symbol_name);
+
+      if(symbol_ptr != nullptr)
+      {
+        // Found the symbol by its identifier
+        to_exclude.insert(
+          id2string(symbol_ptr->location.get_file()) + ":" +
+          id2string(symbol_ptr->display_name()));
+      }
+      else
+      {
+        // Symbol not found, report an error
+        throw invalid_command_line_argument_exceptiont(
+          "symbol '" + except + "' not found in symbol table",
+          "--nondet-static-exclude");
+      }
     }
   }