From 9ba013df1d4d01b9c50fd41afbc0d15b74f4ba91 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 11 Jan 2022 21:16:03 +0000 Subject: [PATCH] CONTRACTS: remove redundant "::" in generated symbol names This is just a beautification of goto programs generated for contracts checking: get_fresh_aux_symbol will add "::" in this place already, so we ended up with "::::" in symbol names. --- regression/contracts/history-pointer-replace-01/test.desc | 2 +- regression/contracts/history-pointer-replace-02/test.desc | 2 +- src/goto-instrument/contracts/utils.cpp | 7 +------ 3 files changed, 3 insertions(+), 8 deletions(-) diff --git a/regression/contracts/history-pointer-replace-01/test.desc b/regression/contracts/history-pointer-replace-01/test.desc index c71a3568bcb..d4ed769e2b5 100644 --- a/regression/contracts/history-pointer-replace-01/test.desc +++ b/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: diff --git a/regression/contracts/history-pointer-replace-02/test.desc b/regression/contracts/history-pointer-replace-02/test.desc index fe20ba680c5..10010d78476 100644 --- a/regression/contracts/history-pointer-replace-02/test.desc +++ b/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: diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 607038d9e87..8757502b873 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/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; }