Merge pull request #6567 from tautschnig/contracts/four-colons

CONTRACTS: remove redundant "::" in generated symbol names

Author: tautschnig

regression/contracts/history-pointer-replace-01/test.desc

@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 ASSERT \*\(address_of.*n.*\) > 0
-ASSUME \*\(address_of.*n.*\) = .*::tmp_cc[\$\d]? \+ 2
+ASSUME \*\(address_of.*n.*\) = tmp_cc[\$\d]? \+ 2
 --
 --
 Verification:

regression/contracts/history-pointer-replace-02/test.desc

@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 ASSERT \*\(address_of.*n.*\) = 0
-ASSUME \*\(address_of.*n.*\) ≥ .*::tmp_cc[\$\d]? \+ 2
+ASSUME \*\(address_of.*n.*\) ≥ tmp_cc[\$\d]? \+ 2
 --
 --
 Verification:

src/goto-instrument/contracts/utils.cpp

@@ -151,12 +151,7 @@ const symbolt &new_tmp_symbol(
   bool is_auxiliary)
 {
   symbolt &new_symbol = get_fresh_aux_symbol(
-    type,
-    id2string(location.get_function()) + "::",
-    suffix,
-    location,
-    mode,
-    symtab);
+    type, id2string(location.get_function()), suffix, location, mode, symtab);
   new_symbol.is_auxiliary = is_auxiliary;
   return new_symbol;
 }