Skip to content

Don't ignore switch exits that are also loop exits #974

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

Closed
Nadrieril wants to merge 3 commits into from
Closed

Don't ignore switch exits that are also loop exits #974

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
fea8d5a
Don't ignore switch exits that are also loop exits
Nadrieril Jan 14, 2026
5725954
Cleanup
Nadrieril Jan 14, 2026
8cdb6f1
Cleanup a bit more
Nadrieril Jan 14, 2026
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
440 changes: 141 additions & 299 deletions charon/src/transform/control_flow/ullbc_to_llbc.rs
View file
Open in desktop

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion charon/tests/ui/control-flow/issue-297-cfg.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -622,7 +622,6 @@ fn f2<'_0, '_1>(@1: &'_0 [u8], @2: &'_1 mut [i16]) -> usize
storage_dead(_9)
match _8 {
Option::None => {
break 0
},
Option::Some => {
storage_live(bytes_11)
Expand Down Expand Up @@ -768,6 +767,7 @@ fn f2<'_0, '_1>(@1: &'_0 [u8], @2: &'_1 mut [i16]) -> usize
continue 0
},
}
break 0
}
storage_dead(_10)
storage_dead(_8)
Expand Down
3 changes: 1 addition & 2 deletions charon/tests/ui/control-flow/loop-break.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,18 +70,17 @@ fn main()
storage_live(_3)
_3 = foo()
if move _3 {
break 0
} else {
storage_live(_4)
_4 = bar()
if move _4 {
break 0
} else {
storage_dead(_4)
storage_dead(_3)
continue 0
}
}
break 0
}
storage_dead(_4)
storage_dead(_3)
Expand Down
8 changes: 4 additions & 4 deletions charon/tests/ui/control-flow/loops.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1634,7 +1634,6 @@ pub fn nested_loops_enum(@1: usize, @2: usize) -> usize
storage_dead(_8)
match _7 {
Option::None => {
break 0
},
Option::Some => {
_10 = copy s_3 panic.+ const 1 : usize
Expand All @@ -1644,6 +1643,7 @@ pub fn nested_loops_enum(@1: usize, @2: usize) -> usize
continue 0
},
}
break 0
}
storage_dead(_9)
storage_dead(_7)
Expand All @@ -1669,7 +1669,6 @@ pub fn nested_loops_enum(@1: usize, @2: usize) -> usize
storage_dead(_16)
match _15 {
Option::None => {
break 0
},
Option::Some => {
storage_live(_18)
Expand All @@ -1692,7 +1691,6 @@ pub fn nested_loops_enum(@1: usize, @2: usize) -> usize
storage_dead(_23)
match _22 {
Option::None => {
break 0
},
Option::Some => {
_25 = copy s_3 panic.+ const 1 : usize
Expand All @@ -1702,6 +1700,7 @@ pub fn nested_loops_enum(@1: usize, @2: usize) -> usize
continue 0
},
}
break 0
}
storage_dead(_24)
storage_dead(_22)
Expand All @@ -1712,6 +1711,7 @@ pub fn nested_loops_enum(@1: usize, @2: usize) -> usize
continue 0
},
}
break 0
}
storage_dead(_17)
storage_dead(_15)
Expand Down Expand Up @@ -1767,7 +1767,6 @@ pub fn loop_inside_if(@1: bool, @2: u32) -> u32
storage_dead(_10)
match _9 {
Option::None => {
break 0
},
Option::Some => {
storage_live(i_12)
Expand All @@ -1783,6 +1782,7 @@ pub fn loop_inside_if(@1: bool, @2: u32) -> u32
continue 0
},
}
break 0
}
storage_dead(_11)
storage_dead(_9)
Expand Down
2 changes: 1 addition & 1 deletion charon/tests/ui/gosim-demo.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -574,7 +574,6 @@ where
storage_dead(_6)
match _5 {
Option::None => {
break 0
},
Option::Some => {
storage_live(x_8)
Expand Down Expand Up @@ -622,6 +621,7 @@ where
continue 0
},
}
break 0
}
_0 = ()
storage_dead(_7)
Expand Down
2 changes: 1 addition & 1 deletion charon/tests/ui/issue-45-misc.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -687,7 +687,6 @@ fn cbd(@1: [u8; 33 : usize])
storage_dead(_6)
match _5 {
Option::None => {
break 0
},
Option::Some => {
storage_live(i_8)
Expand All @@ -709,6 +708,7 @@ fn cbd(@1: [u8; 33 : usize])
continue 0
},
}
break 0
}
_0 = ()
storage_dead(_7)
Expand Down
8 changes: 4 additions & 4 deletions charon/tests/ui/iterator.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5253,7 +5253,6 @@ fn main()
storage_dead(_8)
match _7 {
Option::None => {
break 0
},
Option::Some => {
storage_live(v_10)
Expand All @@ -5269,6 +5268,7 @@ fn main()
continue 0
},
}
break 0
}
storage_dead(_9)
storage_dead(_7)
Expand Down Expand Up @@ -5299,7 +5299,6 @@ fn main()
storage_dead(_19)
match _18 {
Option::None => {
break 0
},
Option::Some => {
storage_live(v_21)
Expand All @@ -5319,6 +5318,7 @@ fn main()
continue 0
},
}
break 0
}
storage_dead(_20)
storage_dead(_18)
Expand Down Expand Up @@ -5347,7 +5347,6 @@ fn main()
storage_dead(_31)
match _30 {
Option::None => {
break 0
},
Option::Some => {
_33 = copy i_2 panic.+ const 1 : i32
Expand All @@ -5357,6 +5356,7 @@ fn main()
continue 0
},
}
break 0
}
storage_dead(_32)
storage_dead(_30)
Expand Down Expand Up @@ -5385,7 +5385,6 @@ fn main()
storage_dead(_40)
match _39 {
Option::None => {
break 0
},
Option::Some => {
_42 = copy i_2 panic.+ const 1 : i32
Expand All @@ -5395,6 +5394,7 @@ fn main()
continue 0
},
}
break 0
}
storage_dead(_41)
storage_dead(_39)
Expand Down
2 changes: 1 addition & 1 deletion charon/tests/ui/simple/range-iter.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -464,7 +464,6 @@ fn iter(@1: usize)
storage_dead(_7)
match _6 {
Option::None => {
break 0
},
Option::Some => {
storage_live(i_9)
Expand All @@ -475,6 +474,7 @@ fn iter(@1: usize)
continue 0
},
}
break 0
}
_0 = ()
storage_dead(_8)
Expand Down
Loading