-
Notifications
You must be signed in to change notification settings - Fork 75
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #93 from lqd/factchecking
Error generation: add tests and fix Naive variant
- Loading branch information
Showing
52 changed files
with
828 additions
and
0 deletions.
There are no files selected for viewing
Empty file.
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,3 @@ | ||
| "Start(bb0[0])" "Mid(bb0[0])" | ||
| "Mid(bb0[0])" "Start(bb0[1])" | ||
| "Start(bb0[1])" "Mid(bb0[1])" |
Empty file.
Empty file.
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,27 @@ | ||
| "\'_#4r" "\'_#6r" "Mid(bb0[0])" | ||
| "\'_#8r" "\'_#4r" "Mid(bb0[0])" | ||
| "\'_#7r" "\'_#4r" "Mid(bb0[0])" | ||
| "\'_#7r" "\'_#1r" "Start(bb0[0])" | ||
| "\'_#7r" "\'_#1r" "Mid(bb0[0])" | ||
| "\'_#7r" "\'_#1r" "Start(bb0[1])" | ||
| "\'_#7r" "\'_#1r" "Mid(bb0[1])" | ||
| "\'_#1r" "\'_#7r" "Start(bb0[0])" | ||
| "\'_#1r" "\'_#7r" "Mid(bb0[0])" | ||
| "\'_#1r" "\'_#7r" "Start(bb0[1])" | ||
| "\'_#1r" "\'_#7r" "Mid(bb0[1])" | ||
| "\'_#8r" "\'_#2r" "Start(bb0[0])" | ||
| "\'_#8r" "\'_#2r" "Mid(bb0[0])" | ||
| "\'_#8r" "\'_#2r" "Start(bb0[1])" | ||
| "\'_#8r" "\'_#2r" "Mid(bb0[1])" | ||
| "\'_#2r" "\'_#8r" "Start(bb0[0])" | ||
| "\'_#2r" "\'_#8r" "Mid(bb0[0])" | ||
| "\'_#2r" "\'_#8r" "Start(bb0[1])" | ||
| "\'_#2r" "\'_#8r" "Mid(bb0[1])" | ||
| "\'_#6r" "\'_#1r" "Start(bb0[0])" | ||
| "\'_#6r" "\'_#1r" "Mid(bb0[0])" | ||
| "\'_#6r" "\'_#1r" "Start(bb0[1])" | ||
| "\'_#6r" "\'_#1r" "Mid(bb0[1])" | ||
| "\'_#1r" "\'_#6r" "Start(bb0[0])" | ||
| "\'_#1r" "\'_#6r" "Mid(bb0[0])" | ||
| "\'_#1r" "\'_#6r" "Start(bb0[1])" | ||
| "\'_#1r" "\'_#6r" "Mid(bb0[1])" |
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,4 @@ | ||
| "\'_#7r" "Start(bb0[0])" | ||
| "\'_#7r" "Mid(bb0[0])" | ||
| "\'_#8r" "Start(bb0[0])" | ||
| "\'_#8r" "Mid(bb0[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,4 @@ | ||
| "\'_#0r" | ||
| "\'_#1r" | ||
| "\'_#2r" | ||
| "\'_#3r" |
Empty file.
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,3 @@ | ||
| "Start(bb0[0])" "Mid(bb0[0])" | ||
| "Mid(bb0[0])" "Start(bb0[1])" | ||
| "Start(bb0[1])" "Mid(bb0[1])" |
Empty file.
Empty file.
Empty file.
Empty file.
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,2 @@ | ||
| "\'_#0r" | ||
| "\'_#1r" |
3 changes: 3 additions & 0 deletions
3
inputs/smoke-test/nll-facts/position_dependent_outlives/borrow_region.facts
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,3 @@ | ||
| "\'_#3r" "bw0" "Mid(bb0[2])" | ||
| "\'_#4r" "bw1" "Mid(bb1[0])" | ||
| "\'_#5r" "bw2" "Mid(bb2[1])" |
32 changes: 32 additions & 0 deletions
32
inputs/smoke-test/nll-facts/position_dependent_outlives/cfg_edge.facts
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,32 @@ | ||
| "Start(bb0[0])" "Mid(bb0[0])" | ||
| "Mid(bb0[0])" "Start(bb0[1])" | ||
| "Start(bb0[1])" "Mid(bb0[1])" | ||
| "Mid(bb0[1])" "Start(bb0[2])" | ||
| "Start(bb0[2])" "Mid(bb0[2])" | ||
| "Mid(bb0[2])" "Start(bb0[3])" | ||
| "Start(bb0[3])" "Mid(bb0[3])" | ||
| "Mid(bb0[3])" "Start(bb0[4])" | ||
| "Start(bb0[4])" "Mid(bb0[4])" | ||
| "Mid(bb0[4])" "Start(bb0[5])" | ||
| "Start(bb0[5])" "Mid(bb0[5])" | ||
| "Mid(bb0[5])" "Start(bb0[6])" | ||
| "Start(bb0[6])" "Mid(bb0[6])" | ||
| "Mid(bb0[6])" "Start(bb0[7])" | ||
| "Start(bb0[7])" "Mid(bb0[7])" | ||
| "Mid(bb0[7])" "Start(bb2[0])" | ||
| "Mid(bb0[7])" "Start(bb1[0])" | ||
| "Start(bb1[0])" "Mid(bb1[0])" | ||
| "Mid(bb1[0])" "Start(bb1[1])" | ||
| "Start(bb1[1])" "Mid(bb1[1])" | ||
| "Mid(bb1[1])" "Start(bb3[0])" | ||
| "Start(bb2[0])" "Mid(bb2[0])" | ||
| "Mid(bb2[0])" "Start(bb2[1])" | ||
| "Start(bb2[1])" "Mid(bb2[1])" | ||
| "Mid(bb2[1])" "Start(bb2[2])" | ||
| "Start(bb2[2])" "Mid(bb2[2])" | ||
| "Mid(bb2[2])" "Start(bb3[0])" | ||
| "Start(bb3[0])" "Mid(bb3[0])" | ||
| "Mid(bb3[0])" "Start(bb3[1])" | ||
| "Start(bb3[1])" "Mid(bb3[1])" | ||
| "Mid(bb3[1])" "Start(bb3[2])" | ||
| "Start(bb3[2])" "Mid(bb3[2])" |
8 changes: 8 additions & 0 deletions
8
inputs/smoke-test/nll-facts/position_dependent_outlives/invalidates.facts
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,8 @@ | ||
| "Start(bb0[2])" "bw0" | ||
| "Start(bb0[2])" "bw2" | ||
| "Start(bb0[3])" "bw1" | ||
| "Start(bb1[0])" "bw1" | ||
| "Start(bb2[0])" "bw0" | ||
| "Start(bb2[0])" "bw2" | ||
| "Start(bb2[1])" "bw0" | ||
| "Start(bb2[1])" "bw2" |
1 change: 1 addition & 0 deletions
1
inputs/smoke-test/nll-facts/position_dependent_outlives/killed.facts
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 @@ | ||
| "bw1" "Mid(bb0[2])" |
134 changes: 134 additions & 0 deletions
134
inputs/smoke-test/nll-facts/position_dependent_outlives/outlives.facts
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,134 @@ | ||
| "\'_#3r" "\'_#10r" "Mid(bb0[2])" | ||
| "\'_#8r" "\'_#3r" "Mid(bb0[2])" | ||
| "\'_#4r" "\'_#7r" "Mid(bb1[0])" | ||
| "\'_#10r" "\'_#4r" "Mid(bb1[0])" | ||
| "\'_#5r" "\'_#7r" "Mid(bb2[1])" | ||
| "\'_#8r" "\'_#5r" "Mid(bb2[1])" | ||
| "\'_#8r" "\'_#1r" "Start(bb0[0])" | ||
| "\'_#8r" "\'_#1r" "Mid(bb0[0])" | ||
| "\'_#8r" "\'_#1r" "Start(bb0[1])" | ||
| "\'_#8r" "\'_#1r" "Mid(bb0[1])" | ||
| "\'_#8r" "\'_#1r" "Start(bb0[2])" | ||
| "\'_#8r" "\'_#1r" "Mid(bb0[2])" | ||
| "\'_#8r" "\'_#1r" "Start(bb0[3])" | ||
| "\'_#8r" "\'_#1r" "Mid(bb0[3])" | ||
| "\'_#8r" "\'_#1r" "Start(bb0[4])" | ||
| "\'_#8r" "\'_#1r" "Mid(bb0[4])" | ||
| "\'_#8r" "\'_#1r" "Start(bb0[5])" | ||
| "\'_#8r" "\'_#1r" "Mid(bb0[5])" | ||
| "\'_#8r" "\'_#1r" "Start(bb0[6])" | ||
| "\'_#8r" "\'_#1r" "Mid(bb0[6])" | ||
| "\'_#8r" "\'_#1r" "Start(bb0[7])" | ||
| "\'_#8r" "\'_#1r" "Mid(bb0[7])" | ||
| "\'_#8r" "\'_#1r" "Start(bb1[0])" | ||
| "\'_#8r" "\'_#1r" "Mid(bb1[0])" | ||
| "\'_#8r" "\'_#1r" "Start(bb1[1])" | ||
| "\'_#8r" "\'_#1r" "Mid(bb1[1])" | ||
| "\'_#8r" "\'_#1r" "Start(bb2[0])" | ||
| "\'_#8r" "\'_#1r" "Mid(bb2[0])" | ||
| "\'_#8r" "\'_#1r" "Start(bb2[1])" | ||
| "\'_#8r" "\'_#1r" "Mid(bb2[1])" | ||
| "\'_#8r" "\'_#1r" "Start(bb2[2])" | ||
| "\'_#8r" "\'_#1r" "Mid(bb2[2])" | ||
| "\'_#8r" "\'_#1r" "Start(bb3[0])" | ||
| "\'_#8r" "\'_#1r" "Mid(bb3[0])" | ||
| "\'_#8r" "\'_#1r" "Start(bb3[1])" | ||
| "\'_#8r" "\'_#1r" "Mid(bb3[1])" | ||
| "\'_#8r" "\'_#1r" "Start(bb3[2])" | ||
| "\'_#8r" "\'_#1r" "Mid(bb3[2])" | ||
| "\'_#1r" "\'_#8r" "Start(bb0[0])" | ||
| "\'_#1r" "\'_#8r" "Mid(bb0[0])" | ||
| "\'_#1r" "\'_#8r" "Start(bb0[1])" | ||
| "\'_#1r" "\'_#8r" "Mid(bb0[1])" | ||
| "\'_#1r" "\'_#8r" "Start(bb0[2])" | ||
| "\'_#1r" "\'_#8r" "Mid(bb0[2])" | ||
| "\'_#1r" "\'_#8r" "Start(bb0[3])" | ||
| "\'_#1r" "\'_#8r" "Mid(bb0[3])" | ||
| "\'_#1r" "\'_#8r" "Start(bb0[4])" | ||
| "\'_#1r" "\'_#8r" "Mid(bb0[4])" | ||
| "\'_#1r" "\'_#8r" "Start(bb0[5])" | ||
| "\'_#1r" "\'_#8r" "Mid(bb0[5])" | ||
| "\'_#1r" "\'_#8r" "Start(bb0[6])" | ||
| "\'_#1r" "\'_#8r" "Mid(bb0[6])" | ||
| "\'_#1r" "\'_#8r" "Start(bb0[7])" | ||
| "\'_#1r" "\'_#8r" "Mid(bb0[7])" | ||
| "\'_#1r" "\'_#8r" "Start(bb1[0])" | ||
| "\'_#1r" "\'_#8r" "Mid(bb1[0])" | ||
| "\'_#1r" "\'_#8r" "Start(bb1[1])" | ||
| "\'_#1r" "\'_#8r" "Mid(bb1[1])" | ||
| "\'_#1r" "\'_#8r" "Start(bb2[0])" | ||
| "\'_#1r" "\'_#8r" "Mid(bb2[0])" | ||
| "\'_#1r" "\'_#8r" "Start(bb2[1])" | ||
| "\'_#1r" "\'_#8r" "Mid(bb2[1])" | ||
| "\'_#1r" "\'_#8r" "Start(bb2[2])" | ||
| "\'_#1r" "\'_#8r" "Mid(bb2[2])" | ||
| "\'_#1r" "\'_#8r" "Start(bb3[0])" | ||
| "\'_#1r" "\'_#8r" "Mid(bb3[0])" | ||
| "\'_#1r" "\'_#8r" "Start(bb3[1])" | ||
| "\'_#1r" "\'_#8r" "Mid(bb3[1])" | ||
| "\'_#1r" "\'_#8r" "Start(bb3[2])" | ||
| "\'_#1r" "\'_#8r" "Mid(bb3[2])" | ||
| "\'_#7r" "\'_#1r" "Start(bb0[0])" | ||
| "\'_#7r" "\'_#1r" "Mid(bb0[0])" | ||
| "\'_#7r" "\'_#1r" "Start(bb0[1])" | ||
| "\'_#7r" "\'_#1r" "Mid(bb0[1])" | ||
| "\'_#7r" "\'_#1r" "Start(bb0[2])" | ||
| "\'_#7r" "\'_#1r" "Mid(bb0[2])" | ||
| "\'_#7r" "\'_#1r" "Start(bb0[3])" | ||
| "\'_#7r" "\'_#1r" "Mid(bb0[3])" | ||
| "\'_#7r" "\'_#1r" "Start(bb0[4])" | ||
| "\'_#7r" "\'_#1r" "Mid(bb0[4])" | ||
| "\'_#7r" "\'_#1r" "Start(bb0[5])" | ||
| "\'_#7r" "\'_#1r" "Mid(bb0[5])" | ||
| "\'_#7r" "\'_#1r" "Start(bb0[6])" | ||
| "\'_#7r" "\'_#1r" "Mid(bb0[6])" | ||
| "\'_#7r" "\'_#1r" "Start(bb0[7])" | ||
| "\'_#7r" "\'_#1r" "Mid(bb0[7])" | ||
| "\'_#7r" "\'_#1r" "Start(bb1[0])" | ||
| "\'_#7r" "\'_#1r" "Mid(bb1[0])" | ||
| "\'_#7r" "\'_#1r" "Start(bb1[1])" | ||
| "\'_#7r" "\'_#1r" "Mid(bb1[1])" | ||
| "\'_#7r" "\'_#1r" "Start(bb2[0])" | ||
| "\'_#7r" "\'_#1r" "Mid(bb2[0])" | ||
| "\'_#7r" "\'_#1r" "Start(bb2[1])" | ||
| "\'_#7r" "\'_#1r" "Mid(bb2[1])" | ||
| "\'_#7r" "\'_#1r" "Start(bb2[2])" | ||
| "\'_#7r" "\'_#1r" "Mid(bb2[2])" | ||
| "\'_#7r" "\'_#1r" "Start(bb3[0])" | ||
| "\'_#7r" "\'_#1r" "Mid(bb3[0])" | ||
| "\'_#7r" "\'_#1r" "Start(bb3[1])" | ||
| "\'_#7r" "\'_#1r" "Mid(bb3[1])" | ||
| "\'_#7r" "\'_#1r" "Start(bb3[2])" | ||
| "\'_#7r" "\'_#1r" "Mid(bb3[2])" | ||
| "\'_#1r" "\'_#7r" "Start(bb0[0])" | ||
| "\'_#1r" "\'_#7r" "Mid(bb0[0])" | ||
| "\'_#1r" "\'_#7r" "Start(bb0[1])" | ||
| "\'_#1r" "\'_#7r" "Mid(bb0[1])" | ||
| "\'_#1r" "\'_#7r" "Start(bb0[2])" | ||
| "\'_#1r" "\'_#7r" "Mid(bb0[2])" | ||
| "\'_#1r" "\'_#7r" "Start(bb0[3])" | ||
| "\'_#1r" "\'_#7r" "Mid(bb0[3])" | ||
| "\'_#1r" "\'_#7r" "Start(bb0[4])" | ||
| "\'_#1r" "\'_#7r" "Mid(bb0[4])" | ||
| "\'_#1r" "\'_#7r" "Start(bb0[5])" | ||
| "\'_#1r" "\'_#7r" "Mid(bb0[5])" | ||
| "\'_#1r" "\'_#7r" "Start(bb0[6])" | ||
| "\'_#1r" "\'_#7r" "Mid(bb0[6])" | ||
| "\'_#1r" "\'_#7r" "Start(bb0[7])" | ||
| "\'_#1r" "\'_#7r" "Mid(bb0[7])" | ||
| "\'_#1r" "\'_#7r" "Start(bb1[0])" | ||
| "\'_#1r" "\'_#7r" "Mid(bb1[0])" | ||
| "\'_#1r" "\'_#7r" "Start(bb1[1])" | ||
| "\'_#1r" "\'_#7r" "Mid(bb1[1])" | ||
| "\'_#1r" "\'_#7r" "Start(bb2[0])" | ||
| "\'_#1r" "\'_#7r" "Mid(bb2[0])" | ||
| "\'_#1r" "\'_#7r" "Start(bb2[1])" | ||
| "\'_#1r" "\'_#7r" "Mid(bb2[1])" | ||
| "\'_#1r" "\'_#7r" "Start(bb2[2])" | ||
| "\'_#1r" "\'_#7r" "Mid(bb2[2])" | ||
| "\'_#1r" "\'_#7r" "Start(bb3[0])" | ||
| "\'_#1r" "\'_#7r" "Mid(bb3[0])" | ||
| "\'_#1r" "\'_#7r" "Start(bb3[1])" | ||
| "\'_#1r" "\'_#7r" "Mid(bb3[1])" | ||
| "\'_#1r" "\'_#7r" "Start(bb3[2])" | ||
| "\'_#1r" "\'_#7r" "Mid(bb3[2])" |
32 changes: 32 additions & 0 deletions
32
inputs/smoke-test/nll-facts/position_dependent_outlives/region_live_at.facts
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,32 @@ | ||
| "\'_#8r" "Start(bb0[0])" | ||
| "\'_#8r" "Mid(bb0[0])" | ||
| "\'_#8r" "Start(bb0[1])" | ||
| "\'_#8r" "Mid(bb0[1])" | ||
| "\'_#8r" "Start(bb0[2])" | ||
| "\'_#8r" "Mid(bb0[2])" | ||
| "\'_#8r" "Start(bb0[3])" | ||
| "\'_#8r" "Mid(bb0[3])" | ||
| "\'_#8r" "Start(bb0[4])" | ||
| "\'_#8r" "Mid(bb0[4])" | ||
| "\'_#8r" "Start(bb0[5])" | ||
| "\'_#8r" "Mid(bb0[5])" | ||
| "\'_#8r" "Start(bb0[6])" | ||
| "\'_#8r" "Mid(bb0[6])" | ||
| "\'_#8r" "Start(bb0[7])" | ||
| "\'_#8r" "Mid(bb0[7])" | ||
| "\'_#8r" "Start(bb2[0])" | ||
| "\'_#8r" "Mid(bb2[0])" | ||
| "\'_#8r" "Start(bb2[1])" | ||
| "\'_#8r" "Mid(bb2[1])" | ||
| "\'_#10r" "Start(bb0[3])" | ||
| "\'_#10r" "Mid(bb0[3])" | ||
| "\'_#10r" "Start(bb0[4])" | ||
| "\'_#10r" "Mid(bb0[4])" | ||
| "\'_#10r" "Start(bb0[5])" | ||
| "\'_#10r" "Mid(bb0[5])" | ||
| "\'_#10r" "Start(bb0[6])" | ||
| "\'_#10r" "Mid(bb0[6])" | ||
| "\'_#10r" "Start(bb0[7])" | ||
| "\'_#10r" "Mid(bb0[7])" | ||
| "\'_#10r" "Start(bb1[0])" | ||
| "\'_#10r" "Mid(bb1[0])" |
3 changes: 3 additions & 0 deletions
3
inputs/smoke-test/nll-facts/position_dependent_outlives/universal_region.facts
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,3 @@ | ||
| "\'_#0r" | ||
| "\'_#1r" | ||
| "\'_#2r" |
1 change: 1 addition & 0 deletions
1
inputs/smoke-test/nll-facts/return_ref_to_local/borrow_region.facts
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 @@ | ||
| "\'_#2r" "bw0" "Mid(bb0[4])" |
17 changes: 17 additions & 0 deletions
17
inputs/smoke-test/nll-facts/return_ref_to_local/cfg_edge.facts
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,17 @@ | ||
| "Start(bb0[0])" "Mid(bb0[0])" | ||
| "Mid(bb0[0])" "Start(bb0[1])" | ||
| "Start(bb0[1])" "Mid(bb0[1])" | ||
| "Mid(bb0[1])" "Start(bb0[2])" | ||
| "Start(bb0[2])" "Mid(bb0[2])" | ||
| "Mid(bb0[2])" "Start(bb0[3])" | ||
| "Start(bb0[3])" "Mid(bb0[3])" | ||
| "Mid(bb0[3])" "Start(bb0[4])" | ||
| "Start(bb0[4])" "Mid(bb0[4])" | ||
| "Mid(bb0[4])" "Start(bb0[5])" | ||
| "Start(bb0[5])" "Mid(bb0[5])" | ||
| "Mid(bb0[5])" "Start(bb0[6])" | ||
| "Start(bb0[6])" "Mid(bb0[6])" | ||
| "Mid(bb0[6])" "Start(bb0[7])" | ||
| "Start(bb0[7])" "Mid(bb0[7])" | ||
| "Mid(bb0[7])" "Start(bb0[8])" | ||
| "Start(bb0[8])" "Mid(bb0[8])" |
3 changes: 3 additions & 0 deletions
3
inputs/smoke-test/nll-facts/return_ref_to_local/invalidates.facts
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,3 @@ | ||
| "Start(bb0[1])" "bw0" | ||
| "Start(bb0[6])" "bw0" | ||
| "Start(bb0[8])" "bw0" |
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 @@ | ||
| "bw0" "Mid(bb0[1])" |
39 changes: 39 additions & 0 deletions
39
inputs/smoke-test/nll-facts/return_ref_to_local/outlives.facts
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,39 @@ | ||
| "\'_#2r" "\'_#6r" "Mid(bb0[4])" | ||
| "\'_#3r" "\'_#5r" "Mid(bb0[5])" | ||
| "\'_#6r" "\'_#3r" "Mid(bb0[5])" | ||
| "\'_#5r" "\'_#0r" "Start(bb0[0])" | ||
| "\'_#5r" "\'_#0r" "Mid(bb0[0])" | ||
| "\'_#5r" "\'_#0r" "Start(bb0[1])" | ||
| "\'_#5r" "\'_#0r" "Mid(bb0[1])" | ||
| "\'_#5r" "\'_#0r" "Start(bb0[2])" | ||
| "\'_#5r" "\'_#0r" "Mid(bb0[2])" | ||
| "\'_#5r" "\'_#0r" "Start(bb0[3])" | ||
| "\'_#5r" "\'_#0r" "Mid(bb0[3])" | ||
| "\'_#5r" "\'_#0r" "Start(bb0[4])" | ||
| "\'_#5r" "\'_#0r" "Mid(bb0[4])" | ||
| "\'_#5r" "\'_#0r" "Start(bb0[5])" | ||
| "\'_#5r" "\'_#0r" "Mid(bb0[5])" | ||
| "\'_#5r" "\'_#0r" "Start(bb0[6])" | ||
| "\'_#5r" "\'_#0r" "Mid(bb0[6])" | ||
| "\'_#5r" "\'_#0r" "Start(bb0[7])" | ||
| "\'_#5r" "\'_#0r" "Mid(bb0[7])" | ||
| "\'_#5r" "\'_#0r" "Start(bb0[8])" | ||
| "\'_#5r" "\'_#0r" "Mid(bb0[8])" | ||
| "\'_#0r" "\'_#5r" "Start(bb0[0])" | ||
| "\'_#0r" "\'_#5r" "Mid(bb0[0])" | ||
| "\'_#0r" "\'_#5r" "Start(bb0[1])" | ||
| "\'_#0r" "\'_#5r" "Mid(bb0[1])" | ||
| "\'_#0r" "\'_#5r" "Start(bb0[2])" | ||
| "\'_#0r" "\'_#5r" "Mid(bb0[2])" | ||
| "\'_#0r" "\'_#5r" "Start(bb0[3])" | ||
| "\'_#0r" "\'_#5r" "Mid(bb0[3])" | ||
| "\'_#0r" "\'_#5r" "Start(bb0[4])" | ||
| "\'_#0r" "\'_#5r" "Mid(bb0[4])" | ||
| "\'_#0r" "\'_#5r" "Start(bb0[5])" | ||
| "\'_#0r" "\'_#5r" "Mid(bb0[5])" | ||
| "\'_#0r" "\'_#5r" "Start(bb0[6])" | ||
| "\'_#0r" "\'_#5r" "Mid(bb0[6])" | ||
| "\'_#0r" "\'_#5r" "Start(bb0[7])" | ||
| "\'_#0r" "\'_#5r" "Mid(bb0[7])" | ||
| "\'_#0r" "\'_#5r" "Start(bb0[8])" | ||
| "\'_#0r" "\'_#5r" "Mid(bb0[8])" |
2 changes: 2 additions & 0 deletions
2
inputs/smoke-test/nll-facts/return_ref_to_local/region_live_at.facts
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,2 @@ | ||
| "\'_#6r" "Start(bb0[5])" | ||
| "\'_#6r" "Mid(bb0[5])" |
2 changes: 2 additions & 0 deletions
2
inputs/smoke-test/nll-facts/return_ref_to_local/universal_region.facts
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,2 @@ | ||
| "\'_#0r" | ||
| "\'_#1r" |
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 @@ | ||
| "\'_#2r" "bw0" "Mid(bb0[4])" |
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,35 @@ | ||
| "Start(bb0[0])" "Mid(bb0[0])" | ||
| "Mid(bb0[0])" "Start(bb0[1])" | ||
| "Start(bb0[1])" "Mid(bb0[1])" | ||
| "Mid(bb0[1])" "Start(bb0[2])" | ||
| "Start(bb0[2])" "Mid(bb0[2])" | ||
| "Mid(bb0[2])" "Start(bb0[3])" | ||
| "Start(bb0[3])" "Mid(bb0[3])" | ||
| "Mid(bb0[3])" "Start(bb0[4])" | ||
| "Start(bb0[4])" "Mid(bb0[4])" | ||
| "Mid(bb0[4])" "Start(bb0[5])" | ||
| "Start(bb0[5])" "Mid(bb0[5])" | ||
| "Mid(bb0[5])" "Start(bb0[6])" | ||
| "Start(bb0[6])" "Mid(bb0[6])" | ||
| "Mid(bb0[6])" "Start(bb0[7])" | ||
| "Start(bb0[7])" "Mid(bb0[7])" | ||
| "Mid(bb0[7])" "Start(bb0[8])" | ||
| "Start(bb0[8])" "Mid(bb0[8])" | ||
| "Mid(bb0[8])" "Start(bb0[9])" | ||
| "Start(bb0[9])" "Mid(bb0[9])" | ||
| "Mid(bb0[9])" "Start(bb0[10])" | ||
| "Start(bb0[10])" "Mid(bb0[10])" | ||
| "Mid(bb0[10])" "Start(bb0[11])" | ||
| "Start(bb0[11])" "Mid(bb0[11])" | ||
| "Mid(bb0[11])" "Start(bb0[12])" | ||
| "Start(bb0[12])" "Mid(bb0[12])" | ||
| "Mid(bb0[12])" "Start(bb0[13])" | ||
| "Start(bb0[13])" "Mid(bb0[13])" | ||
| "Mid(bb0[13])" "Start(bb0[14])" | ||
| "Start(bb0[14])" "Mid(bb0[14])" | ||
| "Mid(bb0[14])" "Start(bb0[15])" | ||
| "Start(bb0[15])" "Mid(bb0[15])" | ||
| "Mid(bb0[15])" "Start(bb0[16])" | ||
| "Start(bb0[16])" "Mid(bb0[16])" | ||
| "Mid(bb0[16])" "Start(bb0[17])" | ||
| "Start(bb0[17])" "Mid(bb0[17])" |
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,6 @@ | ||
| "Start(bb0[1])" "bw0" | ||
| "Start(bb0[2])" "bw0" | ||
| "Start(bb0[4])" "bw0" | ||
| "Start(bb0[7])" "bw0" | ||
| "Start(bb0[16])" "bw0" | ||
| "Start(bb0[17])" "bw0" |
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 @@ | ||
| "bw0" "Mid(bb0[1])" |
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,2 @@ | ||
| "\'_#2r" "\'_#3r" "Mid(bb0[4])" | ||
| "\'_#3r" "\'_#4r" "Mid(bb0[10])" |
Oops, something went wrong.