Store goto_symex::\guard in a single place

The static member of a static function will ensure both proper initialisation
and making it available to all users.

Author: tautschnig

src/goto-symex/auto_objects.cpp

@@ -87,7 +87,7 @@ void goto_symext::trigger_auto_object(
     const ssa_exprt &ssa_expr=to_ssa_expr(expr);
     const irep_idt &obj_identifier=ssa_expr.get_object_name();
 
-    if(obj_identifier!="goto_symex::\\guard")
+    if(obj_identifier != symex_targett::guard_identifier())
     {
       const symbolt &symbol=
         ns.lookup(obj_identifier);

src/goto-symex/goto_symex.h

@@ -84,7 +84,6 @@ class goto_symext
       target(_target),
       atomic_section_counter(0),
       log(mh),
-      guard_identifier("goto_symex::\\guard"),
       path_storage(path_storage),
       path_segment_vccs(0),
       _total_vccs(std::numeric_limits<unsigned>::max()),
@@ -238,10 +237,6 @@ class goto_symext
     guardt &,
     bool keep_array);
 
-  // guards
-
-  const irep_idt guard_identifier;
-
   virtual void symex_goto(statet &);
   virtual void symex_start_thread(statet &);
   virtual void symex_atomic_begin(statet &);

src/goto-symex/goto_symex_state.cpp

@@ -180,7 +180,7 @@ void goto_symex_statet::assignment(
 
 #if 0
   PRECONDITION(l1_identifier != get_original_name(l1_identifier)
-      || l1_identifier=="goto_symex::\\guard"
+      || l1_identifier == symex_targett::guard_identifier()
       || ns.lookup(l1_identifier).is_shared()
       || has_prefix(id2string(l1_identifier), "symex::invalid_object")
       || has_prefix(id2string(l1_identifier), "symex_dynamic::dynamic_object"));
@@ -372,7 +372,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
   // is it a shared object?
   const irep_idt &obj_identifier=expr.get_object_name();
   if(
-    obj_identifier == "goto_symex::\\guard" ||
+    obj_identifier == symex_targett::guard_identifier() ||
     (!ns.lookup(obj_identifier).is_shared() && !(dirty)(obj_identifier)))
     return false;
 
@@ -508,7 +508,7 @@ bool goto_symex_statet::l2_thread_write_encoding(
   // is it a shared object?
   const irep_idt &obj_identifier=expr.get_object_name();
   if(
-    obj_identifier == "goto_symex::\\guard" ||
+    obj_identifier == symex_targett::guard_identifier() ||
     (!ns.lookup(obj_identifier).is_shared() && !(dirty)(obj_identifier)))
     return false; // not shared
 

src/goto-symex/renaming_level.cpp

@@ -15,6 +15,8 @@ Author: Romain Brenguier, [email protected]
 #include <util/ssa_expr.h>
 #include <util/symbol.h>
 
+#include "symex_target.h"
+
 void symex_level0t::
 operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
 {
@@ -25,7 +27,7 @@ operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
   const irep_idt &obj_identifier = ssa_expr.get_object_name();
 
   // guards are not L0-renamed
-  if(obj_identifier == "goto_symex::\\guard")
+  if(obj_identifier == symex_targett::guard_identifier())
     return;
 
   const symbolt *s;

src/goto-symex/symex_goto.cpp

@@ -243,8 +243,8 @@ void goto_symext::symex_goto(statet &state)
     }
     else
     {
-      symbol_exprt guard_symbol_expr=
-        symbol_exprt(guard_identifier, bool_typet());
+      symbol_exprt guard_symbol_expr =
+        symbol_exprt(symex_targett::guard_identifier(), bool_typet());
       exprt new_rhs = boolean_negate(new_guard);
 
       ssa_exprt new_lhs(guard_symbol_expr);
@@ -544,7 +544,7 @@ void goto_symext::phi_function(
         dest_state,
         ns,
         diff_guard,
-        guard_identifier,
+        symex_targett::guard_identifier(),
         log,
         symex_config.simplify_opt,
         target,

src/goto-symex/symex_target.h

@@ -71,6 +71,13 @@ class symex_targett
     GUARD,
   };
 
+  // guards
+  static irep_idt guard_identifier()
+  {
+    static irep_idt id = "goto_symex::\\guard";
+    return id;
+  }
+
   /// Read from a shared variable \p ssa_object (which is both the left- and the
   /// right--hand side of assignment): we effectively assign the value stored in
   /// \p ssa_object by another thread to \p ssa_object in the memory scope of