Remove "::" from SYMEX_DYNAMIC_PREFIX

This is to prepare use in combination with get_fresh_aux_symbol.

Author: tautschnig

src/ansi-c/expr2c.cpp

@@ -1617,7 +1617,7 @@ std::string expr2ct::convert_symbol(
     dest=id2string(entry->second);
 
     #if 0
-    if(has_prefix(id2string(id), SYMEX_DYNAMIC_PREFIX "dynamic_object"))
+    if(has_prefix(id2string(id), SYMEX_DYNAMIC_PREFIX "::dynamic_object"))
     {
       if(sizeof_nesting++ == 0)
         dest+=" /*"+convert(src.type());

src/goto-instrument/race_check.cpp

@@ -130,7 +130,7 @@ static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
     identifier == "stdout" || identifier == "stderr" ||
     identifier == "sys_nerr" ||
     has_prefix(id2string(identifier), "symex::invalid_object") ||
-    has_prefix(id2string(identifier), SYMEX_DYNAMIC_PREFIX "dynamic_object"))
+    has_prefix(id2string(identifier), SYMEX_DYNAMIC_PREFIX "::dynamic_object"))
     return false; // no race check
 
   const symbolt &symbol=ns.lookup(identifier);

src/goto-symex/goto_symex_state.cpp

@@ -202,7 +202,8 @@ void goto_symex_statet::assignment(
       || l1_identifier == guard_identifier()
       || ns.lookup(l1_identifier).is_shared()
       || has_prefix(id2string(l1_identifier), "symex::invalid_object")
-      || has_prefix(id2string(l1_identifier), SYMEX_DYNAMIC_PREFIX "dynamic_object"));
+      || has_prefix(id2string(l1_identifier),
+                    SYMEX_DYNAMIC_PREFIX "::dynamic_object"));
 #endif
 
   // do the l2 renaming

src/goto-symex/symex_builtin_functions.cpp

@@ -137,7 +137,7 @@ void goto_symext::symex_allocate(
       size_symbol.base_name=
         "dynamic_object_size"+std::to_string(dynamic_counter);
       size_symbol.name =
-        SYMEX_DYNAMIC_PREFIX + id2string(size_symbol.base_name);
+        SYMEX_DYNAMIC_PREFIX "::" + id2string(size_symbol.base_name);
       size_symbol.type=tmp_size.type();
       size_symbol.mode = mode;
       size_symbol.type.set(ID_C_constant, true);
@@ -156,7 +156,8 @@ void goto_symext::symex_allocate(
   symbolt value_symbol;
 
   value_symbol.base_name="dynamic_object"+std::to_string(dynamic_counter);
-  value_symbol.name = SYMEX_DYNAMIC_PREFIX + id2string(value_symbol.base_name);
+  value_symbol.name =
+    SYMEX_DYNAMIC_PREFIX "::" + id2string(value_symbol.base_name);
   value_symbol.is_lvalue=true;
   value_symbol.type = *object_type;
   value_symbol.type.set(ID_C_dynamic, true);
@@ -401,7 +402,7 @@ void goto_symext::symex_cpp_new(
   symbol.base_name=
     do_array?"dynamic_"+count_string+"_array":
              "dynamic_"+count_string+"_value";
-  symbol.name = SYMEX_DYNAMIC_PREFIX + id2string(symbol.base_name);
+  symbol.name = SYMEX_DYNAMIC_PREFIX "::" + id2string(symbol.base_name);
   symbol.is_lvalue=true;
   if(code.get(ID_statement)==ID_cpp_new_array ||
      code.get(ID_statement)==ID_cpp_new)

src/solvers/flattening/pointer_logic.cpp

@@ -27,7 +27,7 @@ bool pointer_logict::is_dynamic_object(const exprt &expr) const
          (expr.id() == ID_symbol &&
           has_prefix(
             id2string(to_symbol_expr(expr).get_identifier()),
-            SYMEX_DYNAMIC_PREFIX));
+            SYMEX_DYNAMIC_PREFIX "::"));
 }
 
 void pointer_logict::get_dynamic_objects(std::vector<std::size_t> &o) const

src/util/pointer_predicates.h

@@ -12,7 +12,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_UTIL_POINTER_PREDICATES_H
 #define CPROVER_UTIL_POINTER_PREDICATES_H
 
-#define SYMEX_DYNAMIC_PREFIX "symex_dynamic::"
+#define SYMEX_DYNAMIC_PREFIX "symex_dynamic"
 
 class exprt;
 class namespacet;

src/util/simplify_expr_pointer.cpp

@@ -553,7 +553,8 @@ bool simplify_exprt::simplify_dynamic_object(exprt &expr)
       const irep_idt identifier=to_symbol_expr(op.op0()).get_identifier();
 
       // this is for the benefit of symex
-      expr.make_bool(has_prefix(id2string(identifier), SYMEX_DYNAMIC_PREFIX));
+      expr.make_bool(
+        has_prefix(id2string(identifier), SYMEX_DYNAMIC_PREFIX "::"));
       return false;
     }
     else if(op.op0().id()==ID_string_constant)