Handle infinite-loop poststate correctly in typestate

If control passes an infinite loop (that doesn't have non-local
exits), then everything is true.
This commit is contained in:
Tim Chevalier 2012-03-10 16:21:34 -08:00
parent e34fad7503
commit 98260a2a22
2 changed files with 2 additions and 2 deletions

View file

@ -554,7 +554,7 @@ fn find_pre_post_state_expr(fcx: fn_ctxt, pres: prestate, e: @expr) -> bool {
ret changed | set_poststate_ann(fcx.ccx, e.id, pres); ret changed | set_poststate_ann(fcx.ccx, e.id, pres);
} else { } else {
ret changed | set_poststate_ann(fcx.ccx, e.id, ret changed | set_poststate_ann(fcx.ccx, e.id,
block_poststate(fcx.ccx, body)); false_postcond(num_constrs));
} }
} }
expr_for(d, index, body) { expr_for(d, index, body) {

View file

@ -11,6 +11,6 @@ fn main() {
check (even(y)); check (even(y));
loop { loop {
print_even(y); print_even(y);
loop { loop { loop { y += x; } } } while true { while true { while true { y += x; } } }
} }
} }