Skip to content

Commit 1f5950c

Browse files
committed
Goto crossing scopes: fix scope tree entry of conditions
We must convert the condition of an if/then/else first to make sure any declarations produced by converting the condition have a suitable scope-tree node. Previously, gotos in either branch of the if-then-else were led to believe that declarations resulting from condition were not yet in scope. The feature from diffblue#8091 would, thus, result in a spurious loop back to the declaration to put it in scope before following the goto edge.
1 parent bc46c88 commit 1f5950c

File tree

4 files changed

+31
-3
lines changed

4 files changed

+31
-3
lines changed
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
int foo()
2+
{
3+
return 1;
4+
}
5+
6+
int main()
7+
{
8+
if(foo())
9+
goto out;
10+
11+
return 1;
12+
13+
out:
14+
__CPROVER_assert(0, "false");
15+
return 0;
16+
}
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
no-duplicate-decl.c
3+
--show-goto-functions
4+
^[[:space:]]*DECL main::\$tmp::return_value_foo
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^[[:space:]]*DECL going_to::out
9+
^[[:space:]]*\d+: DECL main::\$tmp::return_value_foo
10+
--
11+
Test that no loop back to the declaration is generated.

regression/validate-trace-xml-schema/check.py

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@
2323
['xml-interface1', 'test_wrong_flag.desc'],
2424
# these want --show-goto-functions instead of producing a trace
2525
['integer-assignments1', 'integer-typecheck.desc'],
26+
['declaration-goto', 'no-duplicate-decl.desc'],
2627
['destructors', 'compound_literal.desc'],
2728
['destructors', 'enter_lexical_block.desc'],
2829
['enum_is_in_range', 'enum_test3-simplified.desc'],

src/ansi-c/goto-conversion/goto_convert.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1597,6 +1597,9 @@ void goto_convertt::convert_ifthenelse(
15971597
return convert_ifthenelse(new_if0, dest, mode);
15981598
}
15991599

1600+
exprt tmp_guard = code.cond();
1601+
clean_expr(tmp_guard, dest, mode);
1602+
16001603
// convert 'then'-branch
16011604
goto_programt tmp_then;
16021605
convert(code.then_case(), tmp_then, mode);
@@ -1616,9 +1619,6 @@ void goto_convertt::convert_ifthenelse(
16161619
: code.else_case().source_location();
16171620
}
16181621

1619-
exprt tmp_guard = code.cond();
1620-
clean_expr(tmp_guard, dest, mode);
1621-
16221622
generate_ifthenelse(
16231623
tmp_guard,
16241624
source_location,

0 commit comments

Comments
 (0)