Handle predicates that recurse in a check() expression

typestate was using the enclosing function ID for the "this function
returns" constraint, which meant confusion and panic in the case
where a predicate p includes "check p()". Fixed it to use a fresh
ID.

Closes #933
This commit is contained in:
Tim Chevalier 2012-01-19 19:07:29 -08:00
parent b9d517296a
commit d242edb57b
3 changed files with 12 additions and 9 deletions

View file

@ -136,24 +136,25 @@ fn mk_fn_info(ccx: crate_ctxt,
/* add the special i_diverge and i_return constraints
(see the type definition for auxiliary::fn_info for an explanation) */
// use the name of the function for the "return" constraint
// use the function name for the "returns" constraint"
let returns_id = ccx.tcx.sess.next_node_id();
let returns_constr = ninit(returns_id, name);
next =
add_constraint(cx.tcx, respan(f_sp, ninit(id, name)), next, res_map);
add_constraint(cx.tcx, respan(f_sp, returns_constr), next, res_map);
// and the name of the function, with a '!' appended to it, for the
// "diverges" constraint
let diverges_id = ccx.tcx.sess.next_node_id();
let diverges_name = name + "!";
next = add_constraint(cx.tcx, respan(f_sp, ninit(diverges_id,
diverges_name)),
next, res_map);
let diverges_constr = ninit(diverges_id, name + "!");
next = add_constraint(cx.tcx, respan(f_sp, diverges_constr), next,
res_map);
let v: @mutable [node_id] = @mutable [];
let rslt =
{constrs: res_map,
num_constraints: next,
cf: f_decl.cf,
i_return: ninit(id, name),
i_diverge: ninit(diverges_id, diverges_name),
i_return: returns_constr,
i_diverge: diverges_constr,
used_vars: v};
ccx.fm.insert(id, rslt);
#debug("%s has %u constraints", name, num_constraints(rslt));

View file

@ -585,7 +585,7 @@ fn find_pre_post_state_expr(fcx: fn_ctxt, pres: prestate, e: @expr) -> bool {
woo! */
let post = false_postcond(num_constrs);
alt fcx.enclosing.cf {
noreturn { kill_poststate_(fcx, ninit(fcx.id, fcx.name), post); }
noreturn { kill_poststate_(fcx, fcx.enclosing.i_return, post); }
_ { }
}
ret set_prestate_ann(fcx.ccx, e.id, pres) |

View file

@ -0,0 +1,2 @@
pure fn c() -> bool { check c(); true }
fn main() {}