Add support for void loop invariant functions with ensures#537

Merged

andreistefanescu merged 17 commits intomainfrom

worktree-more-loop-inv

Feb 26, 2026

Commits on Feb 25, 2026

Add support for void loop invariant functions with ensures

andreistefanescu
and
claude
committed
Fix abort check for void loop invariant functions

andreistefanescu
and
claude
committed
Simplify void invariant inlining by fetching data on the fly

andreistefanescu
and
claude
committed
Remove unnecessary let bindings in inline_void_invariant

andreistefanescu
and
claude
committed
Use lowercase comments in inline_void_invariant

andreistefanescu
and
claude
committed
Skip end label when no early returns in void invariant inlining

andreistefanescu
and
claude
committed
Simplify early return detection in void invariant inlining

andreistefanescu
and
claude
committed
Defend against void functions without trailing Ret

andreistefanescu
and
claude
committed
Simplify early return detection to a slice check

andreistefanescu
and
claude
committed
Early return on empty code instead of saturating_sub

andreistefanescu
and
claude
committed
Move empty code early return to beginning of function

andreistefanescu
and
claude
committed
Reorder handle_targeted_loop_invariant_functions parameters

andreistefanescu
and
claude
committed
Merge branch 'main' into worktree-more-loop-inv
andreistefanescu
authored