Make going_to variable cprover-prefixed

qinheping · Jun 5, 2024 · f993f8c · f993f8c
1 parent 52c3dbb
commit f993f8c
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 9 deletions.
diff --git 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<comment_block>\/\/ [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<comment_block>\/\/ [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
@@ -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,