Skip to content

Make going_to variable cprover-prefixed #8312

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jun 5, 2024
Merged

Make going_to variable cprover-prefixed #8312

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions regression/cbmc/destructors/enter_lexical_block.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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$
--
Expand All @@ -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

Expand Down
14 changes: 7 additions & 7 deletions src/ansi-c/goto-conversion/goto_convert.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
// }

Expand All @@ -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,
Expand Down
Loading