-
Notifications
You must be signed in to change notification settings - Fork 269
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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 #8091 would, thus, result in a spurious loop back to the declaration to put it in scope before following the goto edge.
- Loading branch information
1 parent
5ae5499
commit 4827dd4
Showing
4 changed files
with
31 additions
and
3 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,16 @@ | ||
int foo() | ||
{ | ||
return 1; | ||
} | ||
|
||
int main() | ||
{ | ||
if(foo()) | ||
goto out; | ||
|
||
return 1; | ||
|
||
out: | ||
__CPROVER_assert(0, "false"); | ||
return 0; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
CORE | ||
no-duplicate-decl.c | ||
--show-goto-functions | ||
^[[:space:]]*DECL main::\$tmp::return_value_foo | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
-- | ||
^[[:space:]]*DECL going_to::out | ||
^[[:space:]]*\d+: DECL main::\$tmp::return_value_foo | ||
-- | ||
Test that no loop back to the declaration is generated. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters