Remove "::" from SYMEX_DYNAMIC_PREFIX

This is to prepare use in combination with get_fresh_aux_symbol.

Author: tautschnig

src/ansi-c/expr2c.cpp

@@ -1648,7 +1648,7 @@ std::string expr2ct::convert_symbol(const exprt &src)
     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-programs/graphml_witness.cpp

@@ -459,9 +459,9 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
         }
         else if(
           !contains_symbol_prefix(
-            it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
+            it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "::dynamic_object") &&
           !contains_symbol_prefix(
-            it->full_lhs, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
+            it->full_lhs, SYMEX_DYNAMIC_PREFIX "::dynamic_object") &&
           lhs_id.find("thread") == std::string::npos &&
           lhs_id.find("mutex") == std::string::npos &&
           (!it->full_lhs_value.is_constant() ||

src/goto-symex/symex_builtin_functions.cpp

@@ -142,7 +142,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);
@@ -161,7 +161,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);
@@ -489,7 +490,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

@@ -28,7 +28,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<mp_integer> &o) const

src/util/pointer_predicates.h

@@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "std_expr.h"
 
-#define SYMEX_DYNAMIC_PREFIX "symex_dynamic::"
+#define SYMEX_DYNAMIC_PREFIX "symex_dynamic"
 
 exprt same_object(const exprt &p1, const exprt &p2);
 exprt deallocated(const exprt &pointer, const namespacet &);

src/util/simplify_expr_pointer.cpp

@@ -594,7 +594,7 @@ simplify_exprt::simplify_is_dynamic_object(const unary_exprt &expr)
 
       // this is for the benefit of symex
       return make_boolean_expr(
-        has_prefix(id2string(identifier), SYMEX_DYNAMIC_PREFIX));
+        has_prefix(id2string(identifier), SYMEX_DYNAMIC_PREFIX "::"));
     }
     else if(op_object.id() == ID_string_constant)
     {