From f993f8c52d79036429d7622379701d472d1538c1 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Tue, 4 Jun 2024 23:13:25 -0500 Subject: [PATCH] Make going_to variable cprover-prefixed --- .../cbmc/destructors/enter_lexical_block.desc | 4 ++-- src/ansi-c/goto-conversion/goto_convert.cpp | 14 +++++++------- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/regression/cbmc/destructors/enter_lexical_block.desc b/regression/cbmc/destructors/enter_lexical_block.desc index e8d6cdbafb8..f16f71c5a33 100644 --- a/regression/cbmc/destructors/enter_lexical_block.desc +++ b/regression/cbmc/destructors/enter_lexical_block.desc @@ -2,7 +2,7 @@ CORE main.c --unwind 10 --show-goto-functions activate-multi-line-match -(?P\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*6: .*newAlloc4 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc4 := \{ 4 \}[\s]*(?P>comment_block)[\s]*.*newAlloc6 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc6 := \{ 6 \}[\s]*(?P>comment_block)[\s]*.*newAlloc7 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc7 := \{ 7 \}[\s]*(?P>comment_block)[\s]*.*DEAD main::1::2::2::newAlloc7[\s]*(?P>comment_block)[\s]*.*DEAD main::1::2::2::newAlloc6[\s]*(?P>comment_block)[\s]*.*DEAD main::1::2::2::newAlloc4[\s]*(?P>comment_block)[\s]*.*ASSIGN going_to::nested_if := true[\s]*(?P>comment_block)[\s]*.*GOTO 3 +(?P\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*6: .*newAlloc4 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc4 := \{ 4 \}[\s]*(?P>comment_block)[\s]*.*newAlloc6 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc6 := \{ 6 \}[\s]*(?P>comment_block)[\s]*.*newAlloc7 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc7 := \{ 7 \}[\s]*(?P>comment_block)[\s]*.*DEAD main::1::2::2::newAlloc7[\s]*(?P>comment_block)[\s]*.*DEAD main::1::2::2::newAlloc6[\s]*(?P>comment_block)[\s]*.*DEAD main::1::2::2::newAlloc4[\s]*(?P>comment_block)[\s]*.*ASSIGN __CPROVER_going_to::nested_if := true[\s]*(?P>comment_block)[\s]*.*GOTO 3 ^EXIT=0$ ^SIGNAL=0$ -- @@ -28,7 +28,7 @@ Checks for: // 49 file main.c line 39 function main DEAD main::1::2::2::newAlloc4 // 50 file main.c line 39 function main - ASSIGN going_to::nested_if := true + ASSIGN __CPROVER_going_to::nested_if := true // 51 file main.c line 39 function main GOTO 3 diff --git a/src/ansi-c/goto-conversion/goto_convert.cpp b/src/ansi-c/goto-conversion/goto_convert.cpp index f7e2961a1e6..dd5bc30c8a2 100644 --- a/src/ansi-c/goto-conversion/goto_convert.cpp +++ b/src/ansi-c/goto-conversion/goto_convert.cpp @@ -127,27 +127,27 @@ void goto_convertt::build_declaration_hops( // } // to code which looks like - // { - // __CPROVER_bool going_to::user_label; - // going_to::user_label = false; + // __CPROVER_bool __CPROVER_going_to::user_label; + // __CPROVER_going_to::user_label = false; // statement_block_a(); // if(...) // { - // going_to::user_label = true; + // __CPROVER_going_to::user_label = true; // goto scope_x_label; // } // statement_block_b(); // scope_x_label: // int x; - // if going_to::user_label goto scope_y_label: + // if __CPROVER_going_to::user_label goto scope_y_label: // x = 0; // statement_block_c(); // scope_y_label: // int y; - // if going_to::user_label goto user_label: + // if __CPROVER_going_to::user_label goto user_label: // y = 0; // statement_block_d(); // user_label: - // going_to::user_label = false; + // __CPROVER_going_to::user_label = false; // statement_block_e(); // } @@ -162,7 +162,7 @@ void goto_convertt::build_declaration_hops( label_location.set_hide(); const symbolt &new_flag = get_fresh_aux_symbol( bool_typet{}, - "going_to", + CPROVER_PREFIX "going_to", id2string(inputs.label), label_location, inputs.mode,