diff --git a/src/rustc/middle/tstate/annotate.rs b/src/rustc/middle/tstate/annotate.rs
deleted file mode 100644
index 000a93f7667..00000000000
--- a/src/rustc/middle/tstate/annotate.rs
+++ /dev/null
@@ -1,76 +0,0 @@
-
-use syntax::ast::*;
-use syntax::visit;
-use syntax::codemap::span;
-use syntax::print::pprust::stmt_to_str;
-use aux::{num_constraints, get_fn_info, crate_ctxt, add_node};
-use ann::empty_ann;
-use pat_util::pat_binding_ids;
-
-fn collect_ids_expr(e: @expr, rs: @mut ~[node_id]) { vec::push(*rs, e.id); }
-
-fn collect_ids_block(b: blk, rs: @mut ~[node_id]) {
-    vec::push(*rs, b.node.id);
-}
-
-fn collect_ids_stmt(s: @stmt, rs: @mut ~[node_id]) {
-    match s.node {
-      stmt_decl(_, id) | stmt_expr(_, id) | stmt_semi(_, id) {
-        debug!("node_id %s", int::str(id));
-        debug!("%s", stmt_to_str(*s));
-        vec::push(*rs, id);
-      }
-    }
-}
-
-fn collect_ids_local(tcx: ty::ctxt, l: @local, rs: @mut ~[node_id]) {
-    vec::push_all(*rs, pat_binding_ids(tcx.def_map, l.node.pat));
-}
-
-fn node_ids_in_fn(tcx: ty::ctxt, body: blk, rs: @mut ~[node_id]) {
-    let collect_ids =
-        visit::mk_simple_visitor(@{visit_expr: |a| collect_ids_expr(a, rs),
-                                   visit_block: |a| collect_ids_block(a, rs),
-                                   visit_stmt: |a| collect_ids_stmt(a, rs),
-                                   visit_local: |a|
-                                       collect_ids_local(tcx, a, rs)
-                                   with *visit::default_simple_visitor()});
-    collect_ids.visit_block(body, (), collect_ids);
-}
-
-fn init_vecs(ccx: crate_ctxt, node_ids: ~[node_id], len: uint) {
-    for node_ids.each |i| {
-        log(debug, int::str(i) + ~" |-> " + uint::str(len));
-        add_node(ccx, *i, empty_ann(len));
-    }
-}
-
-fn visit_fn(ccx: crate_ctxt, num_constraints: uint, body: blk) {
-    let node_ids: @mut ~[node_id] = @mut ~[];
-    node_ids_in_fn(ccx.tcx, body, node_ids);
-    let node_id_vec = *node_ids;
-    init_vecs(ccx, node_id_vec, num_constraints);
-}
-
-fn annotate_in_fn(ccx: crate_ctxt, _fk: visit::fn_kind, _decl: fn_decl,
-                  body: blk, _sp: span, id: node_id) {
-    let f_info = get_fn_info(ccx, id);
-    visit_fn(ccx, num_constraints(f_info), body);
-}
-
-fn annotate_crate(ccx: crate_ctxt, crate: crate) {
-    let do_ann =
-        visit::mk_simple_visitor(
-            @{visit_fn: |a,b,c,d,e| annotate_in_fn(ccx, a, b, c, d, e)
-              with *visit::default_simple_visitor()});
-    visit::visit_crate(crate, (), do_ann);
-}
-//
-// Local Variables:
-// mode: rust
-// fill-column: 78;
-// indent-tabs-mode: nil
-// c-basic-offset: 4
-// buffer-file-coding-system: utf-8-unix
-// End:
-//
diff --git a/src/rustc/middle/tstate/auxiliary.rs b/src/rustc/middle/tstate/auxiliary.rs
deleted file mode 100644
index f612ed40a9c..00000000000
--- a/src/rustc/middle/tstate/auxiliary.rs
+++ /dev/null
@@ -1,988 +0,0 @@
-use option::*;
-use pat_util::*;
-use syntax::ast::*;
-use syntax::ast_util::*;
-use syntax::{visit, codemap};
-use codemap::span;
-use std::map::{hashmap, int_hash};
-use syntax::print::pprust::path_to_str;
-use tstate::ann::{pre_and_post, pre_and_post_state, empty_ann, prestate,
-                     poststate, precond, postcond,
-                     set_prestate, set_poststate, set_in_poststate_,
-                     extend_prestate, extend_poststate, set_precondition,
-                     set_postcondition, ts_ann,
-                     clear_in_postcond,
-                     clear_in_poststate_};
-use driver::session::session;
-use dvec::{dvec, extensions};
-use tritv::{trit, tfalse, ttrue, dont_care, t};
-
-use syntax::print::pprust::{constr_args_to_str, lit_to_str};
-
-// Used to communicate which operands should be invalidated
-// to helper functions
-enum oper_type {
-    oper_move,
-    oper_swap,
-    oper_assign,
-    oper_assign_op,
-    oper_pure,
-}
-
-/* logging funs */
-fn def_id_to_str(d: def_id) -> ~str {
-    return int::str(d.crate) + ~"," + int::str(d.node);
-}
-
-fn comma_str(args: ~[@constr_arg_use]) -> ~str {
-    let mut rslt = ~"";
-    let mut comma = false;
-    for args.each |a| {
-        if comma { rslt += ~", "; } else { comma = true; }
-        match a.node {
-          carg_base { rslt += ~"*"; }
-          carg_ident(i) { rslt += *i.ident; }
-          carg_lit(l) { rslt += lit_to_str(l); }
-        }
-    }
-    return rslt;
-}
-
-fn constraint_to_str(tcx: ty::ctxt, c: sp_constr) -> ~str {
-    return fmt!("%s(%s) - arising from %s",
-             path_to_str(c.node.path),
-             comma_str(c.node.args),
-             codemap::span_to_str(c.span, tcx.sess.codemap));
-}
-
-fn tritv_to_str(fcx: fn_ctxt, v: tritv::t) -> ~str {
-    let mut s = ~"";
-    let mut comma = false;
-    for constraints(fcx).each |p| {
-        match v.get(p.bit_num) {
-          dont_care { }
-          tt {
-            s +=
-                if comma { ~", " } else { comma = true; ~"" } +
-                    if tt == tfalse { ~"!" } else { ~"" } +
-                    constraint_to_str(fcx.ccx.tcx, p.c);
-          }
-        }
-    }
-    return s;
-}
-
-fn log_tritv(fcx: fn_ctxt, v: tritv::t) {
-    log(debug, tritv_to_str(fcx, v));
-}
-
-fn first_difference_string(fcx: fn_ctxt, expected: tritv::t, actual: tritv::t)
-   -> ~str {
-    let mut s = ~"";
-    for constraints(fcx).each |c| {
-      if expected.get(c.bit_num) == ttrue &&
-         actual.get(c.bit_num) != ttrue {
-            s = constraint_to_str(fcx.ccx.tcx, c.c);
-            break;
-        }
-    }
-    return s;
-}
-
-fn log_tritv_err(fcx: fn_ctxt, v: tritv::t) {
-    log(error, tritv_to_str(fcx, v));
-}
-
-fn tos(v: ~[uint]) -> ~str {
-    let mut rslt = ~"";
-    for v.each |i| {
-        if i == 0u {
-            rslt += ~"0";
-        } else if i == 1u { rslt += ~"1"; } else { rslt += ~"?"; }
-    }
-    return rslt;
-}
-
-fn log_cond(v: ~[uint]) { log(debug, tos(v)); }
-
-fn log_cond_err(v: ~[uint]) { log(error, tos(v)); }
-
-fn log_pp(pp: pre_and_post) {
-    let p1 = pp.precondition.to_vec();
-    let p2 = pp.postcondition.to_vec();
-    debug!("pre:");
-    log_cond(p1);
-    debug!("post:");
-    log_cond(p2);
-}
-
-fn log_pp_err(pp: pre_and_post) {
-    let p1 = pp.precondition.to_vec();
-    let p2 = pp.postcondition.to_vec();
-    error!("pre:");
-    log_cond_err(p1);
-    error!("post:");
-    log_cond_err(p2);
-}
-
-fn log_states(pp: pre_and_post_state) {
-    let p1 = pp.prestate.to_vec();
-    let p2 = pp.poststate.to_vec();
-    debug!("prestate:");
-    log_cond(p1);
-    debug!("poststate:");
-    log_cond(p2);
-}
-
-fn log_states_err(pp: pre_and_post_state) {
-    let p1 = pp.prestate.to_vec();
-    let p2 = pp.poststate.to_vec();
-    error!("prestate:");
-    log_cond_err(p1);
-    error!("poststate:");
-    log_cond_err(p2);
-}
-
-fn print_ident(i: ident) { log(debug, ~" " + *i + ~" "); }
-
-fn print_idents(&idents: ~[ident]) {
-    if vec::len::<ident>(idents) == 0u { return; }
-    log(debug, ~"an ident: " + *vec::pop::<ident>(idents));
-    print_idents(idents);
-}
-
-
-/* data structures */
-
-/**********************************************************************/
-
-/* Two different data structures represent constraints in different
- contexts: constraint and norm_constraint.
-
-constraint gets used to record constraints in a table keyed by def_ids.  Each
-constraint has a single operator but a list of possible argument lists, and
-thus represents several constraints at once, one for each possible argument
-list.
-
-norm_constraint, in contrast, gets used when handling an instance of a
-constraint rather than a definition of a constraint. It has only a single
-argument list.
-
-The representation of constraints, where multiple instances of the
-same predicate are collapsed into one entry in the table, makes it
-easier to look up a specific instance.
-
-Both types are in constrast with the constraint type defined in
-syntax::ast, which is for predicate constraints only, and is what
-gets generated by the parser. aux and ast share the same type
-to represent predicate *arguments* however. This type
-(constr_arg_general) is parameterized (see comments in syntax::ast).
-
-Both types store an ident and span, for error-logging purposes.
-*/
-type pred_args_ = {args: ~[@constr_arg_use], bit_num: uint};
-
-type pred_args = spanned<pred_args_>;
-
-// The attached node ID is the *defining* node ID
-// for this local.
-type constr_arg_use = spanned<constr_arg_general_<inst>>;
-
-/* Predicate constraints refer to the truth value of a predicate on variables
-(definitely false, maybe true, or definitely true).  The <path> field (and the
-<def_id> field in the npred constructor) names a user-defined function that
-may be the operator in a "check" expression in the source.  */
-
-type constraint = {
-    path: @path,
-    // FIXME (#2539): really only want it to be mut during
-    // collect_locals.  freeze it after that.
-    descs: @dvec<pred_args>
-};
-
-type tsconstr = {
-    path: @path,
-    def_id: def_id,
-    args: ~[@constr_arg_use]
-};
-
-type sp_constr = spanned<tsconstr>;
-
-type norm_constraint = {bit_num: uint, c: sp_constr};
-
-type constr_map = std::map::hashmap<def_id, constraint>;
-
-/* Contains stuff that has to be computed up front */
-/* For easy access, the fn_info stores two special constraints for each
-function.  So we need context. And so it seems clearer to just have separate
-constraints. */
-type fn_info =
-    /* list, accumulated during pre/postcondition
-    computation, of all local variables that may be
-    used */
-    // Doesn't seem to work without the @ -- bug
-    {constrs: constr_map,
-     num_constraints: uint,
-     cf: ret_style,
-     used_vars: @mut ~[node_id],
-     ignore: bool};
-
-/* mapping from node ID to typestate annotation */
-type node_ann_table = @mut ~[mut ts_ann];
-
-
-/* mapping from function name to fn_info map */
-type fn_info_map = std::map::hashmap<node_id, fn_info>;
-
-type fn_ctxt =
-    {enclosing: fn_info, id: node_id, name: ident, ccx: crate_ctxt};
-
-type crate_ctxt = {tcx: ty::ctxt, node_anns: node_ann_table, fm: fn_info_map};
-
-fn get_fn_info(ccx: crate_ctxt, id: node_id) -> fn_info {
-    assert (ccx.fm.contains_key(id));
-    return ccx.fm.get(id);
-}
-
-fn add_node(ccx: crate_ctxt, i: node_id, a: ts_ann) {
-    let sz = vec::len(*ccx.node_anns);
-    if sz <= i as uint {
-        vec::grow(*ccx.node_anns, (i as uint) - sz + 1u, empty_ann(0u));
-    }
-    ccx.node_anns[i] = a;
-}
-
-fn get_ts_ann(ccx: crate_ctxt, i: node_id) -> Option<ts_ann> {
-    if i as uint < vec::len(*ccx.node_anns) {
-        return some::<ts_ann>(ccx.node_anns[i]);
-    } else { return none::<ts_ann>; }
-}
-
-
-/********* utils ********/
-fn node_id_to_ts_ann(ccx: crate_ctxt, id: node_id) -> ts_ann {
-    match get_ts_ann(ccx, id) {
-      none {
-        error!("node_id_to_ts_ann: no ts_ann for node_id %d", id);
-        fail;
-      }
-      Some(tt) { return tt; }
-    }
-}
-
-fn node_id_to_poststate(ccx: crate_ctxt, id: node_id) -> poststate {
-    debug!("node_id_to_poststate");
-    return node_id_to_ts_ann(ccx, id).states.poststate;
-}
-
-fn stmt_to_ann(ccx: crate_ctxt, s: stmt) -> ts_ann {
-    debug!("stmt_to_ann");
-    match s.node {
-      stmt_decl(_, id) | stmt_expr(_, id) | stmt_semi(_, id) {
-        return node_id_to_ts_ann(ccx, id);
-      }
-    }
-}
-
-
-/* fails if e has no annotation */
-fn expr_states(ccx: crate_ctxt, e: @expr) -> pre_and_post_state {
-    debug!("expr_states");
-    return node_id_to_ts_ann(ccx, e.id).states;
-}
-
-
-/* fails if e has no annotation */
-fn expr_pp(ccx: crate_ctxt, e: @expr) -> pre_and_post {
-    debug!("expr_pp");
-    return node_id_to_ts_ann(ccx, e.id).conditions;
-}
-
-fn stmt_pp(ccx: crate_ctxt, s: stmt) -> pre_and_post {
-    return stmt_to_ann(ccx, s).conditions;
-}
-
-
-/* fails if b has no annotation */
-fn block_pp(ccx: crate_ctxt, b: blk) -> pre_and_post {
-    debug!("block_pp");
-    return node_id_to_ts_ann(ccx, b.node.id).conditions;
-}
-
-fn clear_pp(pp: pre_and_post) {
-    ann::clear(pp.precondition);
-    ann::clear(pp.postcondition);
-}
-
-fn clear_precond(ccx: crate_ctxt, id: node_id) {
-    let pp = node_id_to_ts_ann(ccx, id);
-    ann::clear(pp.conditions.precondition);
-}
-
-fn block_states(ccx: crate_ctxt, b: blk) -> pre_and_post_state {
-    debug!("block_states");
-    return node_id_to_ts_ann(ccx, b.node.id).states;
-}
-
-fn stmt_states(ccx: crate_ctxt, s: stmt) -> pre_and_post_state {
-    return stmt_to_ann(ccx, s).states;
-}
-
-fn expr_precond(ccx: crate_ctxt, e: @expr) -> precond {
-    return expr_pp(ccx, e).precondition;
-}
-
-fn expr_postcond(ccx: crate_ctxt, e: @expr) -> postcond {
-    return expr_pp(ccx, e).postcondition;
-}
-
-fn expr_prestate(ccx: crate_ctxt, e: @expr) -> prestate {
-    return expr_states(ccx, e).prestate;
-}
-
-fn expr_poststate(ccx: crate_ctxt, e: @expr) -> poststate {
-    return expr_states(ccx, e).poststate;
-}
-
-fn stmt_precond(ccx: crate_ctxt, s: stmt) -> precond {
-    return stmt_pp(ccx, s).precondition;
-}
-
-fn stmt_postcond(ccx: crate_ctxt, s: stmt) -> postcond {
-    return stmt_pp(ccx, s).postcondition;
-}
-
-fn states_to_poststate(ss: pre_and_post_state) -> poststate {
-    return ss.poststate;
-}
-
-fn stmt_prestate(ccx: crate_ctxt, s: stmt) -> prestate {
-    return stmt_states(ccx, s).prestate;
-}
-
-fn stmt_poststate(ccx: crate_ctxt, s: stmt) -> poststate {
-    return stmt_states(ccx, s).poststate;
-}
-
-fn block_precond(ccx: crate_ctxt, b: blk) -> precond {
-    return block_pp(ccx, b).precondition;
-}
-
-fn block_postcond(ccx: crate_ctxt, b: blk) -> postcond {
-    return block_pp(ccx, b).postcondition;
-}
-
-fn block_prestate(ccx: crate_ctxt, b: blk) -> prestate {
-    return block_states(ccx, b).prestate;
-}
-
-fn block_poststate(ccx: crate_ctxt, b: blk) -> poststate {
-    return block_states(ccx, b).poststate;
-}
-
-fn set_prestate_ann(ccx: crate_ctxt, id: node_id, pre: prestate) -> bool {
-    debug!("set_prestate_ann");
-    return set_prestate(node_id_to_ts_ann(ccx, id), pre);
-}
-
-fn extend_prestate_ann(ccx: crate_ctxt, id: node_id, pre: prestate) -> bool {
-    debug!("extend_prestate_ann");
-    return extend_prestate(node_id_to_ts_ann(ccx, id).states.prestate, pre);
-}
-
-fn set_poststate_ann(ccx: crate_ctxt, id: node_id, post: poststate) -> bool {
-    debug!("set_poststate_ann");
-    return set_poststate(node_id_to_ts_ann(ccx, id), post);
-}
-
-fn extend_poststate_ann(ccx: crate_ctxt, id: node_id, post: poststate) ->
-   bool {
-    debug!("extend_poststate_ann");
-    return extend_poststate(
-        node_id_to_ts_ann(ccx, id).states.poststate, post);
-}
-
-fn set_pre_and_post(ccx: crate_ctxt, id: node_id, pre: precond,
-                    post: postcond) {
-    debug!("set_pre_and_post");
-    let tt = node_id_to_ts_ann(ccx, id);
-    set_precondition(tt, pre);
-    set_postcondition(tt, post);
-}
-
-fn copy_pre_post(ccx: crate_ctxt, id: node_id, sub: @expr) {
-    debug!("set_pre_and_post");
-    let p = expr_pp(ccx, sub);
-    copy_pre_post_(ccx, id, p.precondition, p.postcondition);
-}
-
-fn copy_pre_post_(ccx: crate_ctxt, id: node_id, pre: prestate,
-                  post: poststate) {
-    debug!("set_pre_and_post");
-    let tt = node_id_to_ts_ann(ccx, id);
-    set_precondition(tt, pre);
-    set_postcondition(tt, post);
-}
-
-/* sets all bits to *1* */
-fn set_postcond_false(ccx: crate_ctxt, id: node_id) {
-    let p = node_id_to_ts_ann(ccx, id);
-    ann::set(p.conditions.postcondition);
-}
-
-fn pure_exp(ccx: crate_ctxt, id: node_id, p: prestate) -> bool {
-    return set_prestate_ann(ccx, id, p) | set_poststate_ann(ccx, id, p);
-}
-
-fn num_constraints(m: fn_info) -> uint { return m.num_constraints; }
-
-fn new_crate_ctxt(cx: ty::ctxt) -> crate_ctxt {
-    let na: ~[mut ts_ann] = ~[mut];
-    return {tcx: cx, node_anns: @mut na, fm: int_hash::<fn_info>()};
-}
-
-/* Use e's type to determine whether it returns.
- If it has a function type with a ! annotation,
-the answer is noreturn. */
-fn controlflow_expr(ccx: crate_ctxt, e: @expr) -> ret_style {
-    match ty::get(ty::node_id_to_type(ccx.tcx, e.id)).struct {
-      ty::ty_fn(f) { return f.ret_style; }
-      _ { return return_val; }
-    }
-}
-
-fn constraints_expr(cx: ty::ctxt, e: @expr) -> ~[@ty::constr] {
-    match ty::get(ty::node_id_to_type(cx, e.id)).struct {
-      ty::ty_fn(f) { return f.constraints; }
-      _ { return ~[]; }
-    }
-}
-
-fn node_id_to_def_strict(cx: ty::ctxt, id: node_id) -> def {
-    match cx.def_map.find(id) {
-      none {
-        error!("node_id_to_def: node_id %d has no def", id);
-        fail;
-      }
-      Some(d) { return d; }
-    }
-}
-
-fn node_id_to_def(ccx: crate_ctxt, id: node_id) -> Option<def> {
-    return ccx.tcx.def_map.find(id);
-}
-
-fn norm_a_constraint(id: def_id, c: constraint) -> ~[norm_constraint] {
-    let mut rslt: ~[norm_constraint] = ~[];
-    for (*c.descs).each |pd| {
-        vec::push(rslt,
-                  {bit_num: pd.node.bit_num,
-                   c: respan(pd.span, {path: c.path,
-                                       def_id: id,
-                                       args: pd.node.args})});
-    }
-    return rslt;
-}
-
-
-// Tried to write this as an iterator, but I got a
-// non-exhaustive match in trans.
-fn constraints(fcx: fn_ctxt) -> ~[norm_constraint] {
-    let mut rslt: ~[norm_constraint] = ~[];
-    for fcx.enclosing.constrs.each |key, val| {
-        vec::push_all(rslt, norm_a_constraint(key, val));
-    };
-    return rslt;
-}
-
-// FIXME (#2539): Would rather take an immutable vec as an argument,
-// should freeze it at some earlier point.
-fn match_args(fcx: fn_ctxt, occs: @dvec<pred_args>,
-              occ: ~[@constr_arg_use]) -> uint {
-    debug!("match_args: looking at %s",
-           constr_args_to_str(fn@(i: inst) -> ~str { *i.ident }, occ));
-    for (*occs).each |pd| {
-        log(debug,
-                 ~"match_args: candidate " + pred_args_to_str(pd));
-        fn eq(p: inst, q: inst) -> bool { return p.node == q.node; }
-        if ty::args_eq(eq, pd.node.args, occ) { return pd.node.bit_num; }
-    }
-    fcx.ccx.tcx.sess.bug(~"match_args: no match for occurring args");
-}
-
-fn def_id_for_constr(tcx: ty::ctxt, t: node_id) -> def_id {
-    match tcx.def_map.find(t) {
-      none {
-        tcx.sess.bug(~"node_id_for_constr: bad node_id " + int::str(t));
-      }
-      Some(def_fn(i, _)) { return i; }
-      _ { tcx.sess.bug(~"node_id_for_constr: pred is not a function"); }
-    }
-}
-
-fn expr_to_constr_arg(tcx: ty::ctxt, e: @expr) -> @constr_arg_use {
-    match e.node {
-      expr_path(p) {
-        match tcx.def_map.find(e.id) {
-          Some(def_local(nid, _)) | Some(def_arg(nid, _)) |
-          Some(def_binding(nid, _)) | Some(def_upvar(nid, _, _, _)) {
-            return @respan(p.span,
-                        carg_ident({ident: p.idents[0], node: nid}));
-          }
-          Some(what) {
-              tcx.sess.span_bug(e.span,
-                 fmt!("exprs_to_constr_args: non-local variable %? \
-                                     as pred arg", what));
-          }
-          none {
-              tcx.sess.span_bug(e.span,
-                 ~"exprs_to_constr_args: unbound id as pred arg");
-
-          }
-        }
-      }
-      expr_lit(l) { return @respan(e.span, carg_lit(l)); }
-      _ {
-        tcx.sess.span_fatal(e.span,
-                            ~"arguments to constrained functions must be " +
-                                ~"literals or local variables");
-      }
-    }
-}
-
-fn exprs_to_constr_args(tcx: ty::ctxt,
-                        args: ~[@expr]) -> ~[@constr_arg_use] {
-    let f = |a| expr_to_constr_arg(tcx, a);
-    let mut rslt: ~[@constr_arg_use] = ~[];
-    for args.each |e| { vec::push(rslt, f(e)); }
-    rslt
-}
-
-fn expr_to_constr(tcx: ty::ctxt, e: @expr) -> sp_constr {
-    match e.node {
-      expr_call(operator, args, _) {
-        match operator.node {
-          expr_path(p) {
-            return respan(e.span,
-                       {path: p,
-                        def_id: def_id_for_constr(tcx, operator.id),
-                        args: exprs_to_constr_args(tcx, args)});
-          }
-          _ {
-            tcx.sess.span_bug(operator.span,
-                              ~"ill-formed operator in predicate");
-          }
-        }
-      }
-      _ {
-        tcx.sess.span_bug(e.span, ~"ill-formed predicate");
-      }
-    }
-}
-
-fn pred_args_to_str(p: pred_args) -> ~str {
-    ~"<" + uint::str(p.node.bit_num) + ~", " +
-        constr_args_to_str(fn@(i: inst) -> ~str {return *i.ident; },
-                           p.node.args)
-        + ~">"
-}
-
-fn substitute_constr_args(cx: ty::ctxt, actuals: ~[@expr], c: @ty::constr) ->
-   tsconstr {
-    let mut rslt: ~[@constr_arg_use] = ~[];
-    for c.node.args.each |a| {
-        vec::push(rslt, substitute_arg(cx, actuals, a));
-    }
-    return {path: c.node.path,
-         def_id: c.node.id,
-         args: rslt};
-}
-
-fn substitute_arg(cx: ty::ctxt, actuals: ~[@expr], a: @constr_arg) ->
-   @constr_arg_use {
-    let num_actuals = vec::len(actuals);
-    match a.node {
-      carg_ident(i) {
-        if i < num_actuals {
-            return expr_to_constr_arg(cx, actuals[i]);
-        } else {
-            cx.sess.span_fatal(a.span, ~"constraint argument out of bounds");
-        }
-      }
-      carg_base { return @respan(a.span, carg_base); }
-      carg_lit(l) { return @respan(a.span, carg_lit(l)); }
-    }
-}
-
-fn pred_args_matches(pattern: ~[constr_arg_general_<inst>],
-                     desc: pred_args) ->
-   bool {
-    let mut i = 0u;
-    for desc.node.args.each |c| {
-        let n = pattern[i];
-        match c.node {
-          carg_ident(p) {
-            match n {
-              carg_ident(q) { if p.node != q.node { return false; } }
-              _ { return false; }
-            }
-          }
-          carg_base { if n != carg_base { return false; } }
-          carg_lit(l) {
-            match n {
-              carg_lit(m) { if !const_eval::lit_eq(l, m) { return false; } }
-              _ { return false; }
-            }
-          }
-        }
-        i += 1u;
-    }
-    return true;
-}
-
-fn find_instance_(pattern: ~[constr_arg_general_<inst>],
-                  descs: ~[pred_args]) ->
-   Option<uint> {
-    for descs.each |d| {
-        if pred_args_matches(pattern, d) { return Some(d.node.bit_num); }
-    }
-    return none;
-}
-
-type inst = {ident: ident, node: node_id};
-
-enum dest {
-    local_dest(inst), // RHS is assigned to a local variable
-    call                        // RHS is passed to a function
-}
-
-type subst = ~[{from: inst, to: inst}];
-
-fn find_instances(_fcx: fn_ctxt, subst: subst,
-                  c: constraint) -> ~[{from: uint, to: uint}] {
-
-    if vec::len(subst) == 0u { return ~[]; }
-    let mut res = ~[];
-    do (*c.descs).swap |v| {
-        let v <- vec::from_mut(v);
-        for v.each |d| {
-            if args_mention(d.node.args, find_in_subst_bool, subst) {
-                let old_bit_num = d.node.bit_num;
-                let newv = replace(subst, d);
-                match find_instance_(newv, v) {
-                  Some(d1) {vec::push(res, {from: old_bit_num, to: d1})}
-                  _ {}
-                }
-            } else {}
-        }
-        vec::to_mut(v)
-    }
-    return res;
-}
-
-fn find_in_subst(id: node_id, s: subst) -> Option<inst> {
-    for s.each |p| {
-        if id == p.from.node { return Some(p.to); }
-    }
-    return none;
-}
-
-fn find_in_subst_bool(s: subst, id: node_id) -> bool {
-    is_some(find_in_subst(id, s))
-}
-
-fn insts_to_str(stuff: ~[constr_arg_general_<inst>]) -> ~str {
-    let mut rslt = ~"<";
-    for stuff.each |i| {
-        rslt +=
-            ~" " +
-                match i {
-                  carg_ident(p) { *p.ident }
-                  carg_base { ~"*" }
-                  carg_lit(_) { ~"~[lit]" }
-                } + ~" ";
-    }
-    rslt += ~">";
-    rslt
-}
-
-fn replace(subst: subst, d: pred_args) -> ~[constr_arg_general_<inst>] {
-    let mut rslt: ~[constr_arg_general_<inst>] = ~[];
-    for d.node.args.each |c| {
-        match c.node {
-          carg_ident(p) {
-            match find_in_subst(p.node, subst) {
-              Some(newv) { vec::push(rslt, carg_ident(newv)); }
-              _ { vec::push(rslt, c.node); }
-            }
-          }
-          _ {
-            vec::push(rslt, c.node);
-          }
-        }
-    }
-
-    return rslt;
-}
-
-enum if_ty { if_check, plain_if, }
-
-fn for_constraints_mentioning(fcx: fn_ctxt, id: node_id,
-                              f: fn(norm_constraint)) {
-    for constraints(fcx).each |c| {
-        if constraint_mentions(fcx, c, id) { f(c); }
-    };
-}
-
-fn local_node_id_to_def_id_strict(fcx: fn_ctxt, sp: span, i: node_id) ->
-   def_id {
-    match local_node_id_to_def(fcx, i) {
-      Some(def_local(nid, _)) | Some(def_arg(nid, _)) |
-      Some(def_upvar(nid, _, _)) {
-        return local_def(nid);
-      }
-      Some(_) {
-        fcx.ccx.tcx.sess.span_fatal(sp,
-                                    ~"local_node_id_to_def_id: id \
-               isn't a local");
-      }
-      none {
-        // should really be bug. span_bug()?
-        fcx.ccx.tcx.sess.span_fatal(sp,
-                                    ~"local_node_id_to_def_id: id \
-               is unbound");
-      }
-    }
-}
-
-fn local_node_id_to_def(fcx: fn_ctxt, i: node_id) -> Option<def> {
-    fcx.ccx.tcx.def_map.find(i)
-}
-
-fn local_node_id_to_def_id(fcx: fn_ctxt, i: node_id) -> Option<def_id> {
-    match local_node_id_to_def(fcx, i) {
-      Some(def_local(nid, _)) | Some(def_arg(nid, _)) |
-      Some(def_binding(nid, _)) | Some(def_upvar(nid, _, _)) {
-        Some(local_def(nid))
-      }
-      _ { none }
-    }
-}
-
-fn local_node_id_to_local_def_id(fcx: fn_ctxt, i: node_id) ->
-   Option<node_id> {
-    match local_node_id_to_def_id(fcx, i) {
-      Some(did) { Some(did.node) }
-      _ { none }
-    }
-}
-
-fn copy_in_postcond(fcx: fn_ctxt, parent_exp: node_id, dest: inst, src: inst,
-                    ty: oper_type) {
-    let post =
-        node_id_to_ts_ann(fcx.ccx, parent_exp).conditions.postcondition;
-    copy_in_poststate_two(fcx, post, post, dest, src, ty);
-}
-
-fn copy_in_poststate(fcx: fn_ctxt, post: poststate, dest: inst, src: inst,
-                     ty: oper_type) {
-    copy_in_poststate_two(fcx, post, post, dest, src, ty);
-}
-
-// In target_post, set the bits corresponding to copies of any
-// constraints mentioning src that are set in src_post, with
-// dest substituted for src.
-// (This doesn't create any new constraints. If a new, substituted
-// constraint isn't already in the bit vector, it's ignored.)
-fn copy_in_poststate_two(fcx: fn_ctxt, src_post: poststate,
-                         target_post: poststate, dest: inst, src: inst,
-                         ty: oper_type) {
-    let mut subst;
-    match ty {
-      oper_swap { subst = ~[{from: dest, to: src}, {from: src, to: dest}]; }
-      oper_assign_op {
-        return; // Don't do any propagation
-      }
-      _ { subst = ~[{from: src, to: dest}]; }
-    }
-
-
-    for fcx.enclosing.constrs.each_value |val| {
-        // replace any occurrences of the src def_id with the
-        // dest def_id
-        let insts = find_instances(fcx, subst, val);
-        for insts.each |p| {
-            if bitvectors::promises_(p.from, src_post) {
-                set_in_poststate_(p.to, target_post);
-            }
-        }
-    };
-}
-
-fn forget_in_postcond(fcx: fn_ctxt, parent_exp: node_id, dead_v: node_id) {
-    // In the postcondition given by parent_exp, clear the bits
-    // for any constraints mentioning dead_v
-    let d = local_node_id_to_local_def_id(fcx, dead_v);
-    do option::iter(d) |d_id| {
-        do for_constraints_mentioning(fcx, d_id) |c| {
-                debug!("clearing constraint %u %s",
-                       c.bit_num,
-                       constraint_to_str(fcx.ccx.tcx, c.c));
-                clear_in_postcond(c.bit_num,
-                                  node_id_to_ts_ann(fcx.ccx,
-                                                    parent_exp).conditions);
-        }
-    };
-}
-
-fn forget_in_poststate(fcx: fn_ctxt, p: poststate, dead_v: node_id) -> bool {
-    // In the poststate given by parent_exp, clear the bits
-    // for any constraints mentioning dead_v
-    let d = local_node_id_to_local_def_id(fcx, dead_v);
-    let mut changed = false;
-    do option::iter(d) |d_id| {
-        do for_constraints_mentioning(fcx, d_id) |c| {
-                changed |= clear_in_poststate_(c.bit_num, p);
-        }
-    }
-    return changed;
-}
-
-fn any_eq(v: ~[node_id], d: node_id) -> bool {
-    for v.each |i| { if i == d { return true; } }
-    false
-}
-
-fn constraint_mentions(_fcx: fn_ctxt, c: norm_constraint, v: node_id) ->
-   bool {
-    return args_mention(c.c.node.args, any_eq, ~[v]);
-}
-
-fn args_mention<T>(args: ~[@constr_arg_use],
-                   q: fn(~[T], node_id) -> bool,
-                   s: ~[T]) -> bool {
-
-    for args.each |a| {
-        match a.node {
-          carg_ident(p1) { if q(s, p1.node) { return true; } } _ { }
-        }
-    }
-    return false;
-}
-
-fn use_var(fcx: fn_ctxt, v: node_id) {
-    vec::push(*fcx.enclosing.used_vars, v);
-}
-
-fn op_to_oper_ty(io: init_op) -> oper_type {
-    match io { init_move { oper_move } _ { oper_assign } }
-}
-
-// default function visitor
-fn do_nothing<T>(_fk: visit::fn_kind, _decl: fn_decl, _body: blk,
-                 _sp: span, _id: node_id,
-                 _t: T, _v: visit::vt<T>) {
-}
-
-
-fn args_to_constr_args(tcx: ty::ctxt, args: ~[arg],
-                       indices: ~[@sp_constr_arg<uint>])
-    -> ~[@constr_arg_use] {
-    let mut actuals: ~[@constr_arg_use] = ~[];
-    let num_args = vec::len(args);
-    for indices.each |a| {
-        vec::push(
-            actuals,
-            @respan(a.span,
-                    match a.node {
-                        carg_base { carg_base }
-                        carg_ident(i) {
-                            if i < num_args {
-                                carg_ident({ident: args[i].ident,
-                                            node: args[i].id})
-                            } else {
-                                tcx.sess.span_bug(a.span,
-                                                  ~"index out of bounds in \
-                                                   constraint arg");
-                            }
-                        }
-                        carg_lit(l) { carg_lit(l) }
-                    }));
-    }
-    return actuals;
-}
-
-fn ast_constr_to_ts_constr(tcx: ty::ctxt, args: ~[arg], c: @constr) ->
-   tsconstr {
-    let tconstr = ty::ast_constr_to_constr(tcx, c);
-    return {path: tconstr.node.path,
-         def_id: tconstr.node.id,
-         args: args_to_constr_args(tcx, args, tconstr.node.args)};
-}
-
-fn ast_constr_to_sp_constr(tcx: ty::ctxt, args: ~[arg], c: @constr) ->
-   sp_constr {
-    let tconstr = ast_constr_to_ts_constr(tcx, args, c);
-    return respan(c.span, tconstr);
-}
-
-type binding = {lhs: ~[dest], rhs: Option<initializer>};
-
-fn local_to_bindings(tcx: ty::ctxt, loc: @local) -> binding {
-    let mut lhs = ~[];
-    do pat_bindings(tcx.def_map, loc.node.pat) |_bm, p_id, _s, name| {
-      vec::push(lhs, local_dest({ident: path_to_ident(name), node: p_id}));
-    };
-    {lhs: lhs, rhs: loc.node.init}
-}
-
-fn locals_to_bindings(tcx: ty::ctxt, locals: ~[@local]) -> ~[binding] {
-    let mut rslt = ~[];
-    for locals.each |loc| { vec::push(rslt, local_to_bindings(tcx, loc)); }
-    return rslt;
-}
-
-fn callee_modes(fcx: fn_ctxt, callee: node_id) -> ~[mode] {
-    let ty = ty::type_autoderef(fcx.ccx.tcx,
-                                ty::node_id_to_type(fcx.ccx.tcx, callee));
-    match ty::get(ty).struct {
-        ty::ty_fn(ref fn_ty) {
-            return fn_ty.sig.inputs.map(|input| input.mode);
-        }
-        _ {
-            // Shouldn't happen; callee should be ty_fn.
-            fcx.ccx.tcx.sess.bug(~"non-fn callee type in callee_modes: " +
-                                 util::ppaux::ty_to_str(fcx.ccx.tcx, ty));
-        }
-    }
-}
-
-fn callee_arg_init_ops(fcx: fn_ctxt, callee: node_id) -> ~[init_op] {
-    do vec::map(callee_modes(fcx, callee)) |m| {
-        match ty::resolved_mode(fcx.ccx.tcx, m) {
-          by_move { init_move }
-          by_copy | by_ref | by_val | by_mutbl_ref { init_assign }
-        }
-    }
-}
-
-fn arg_bindings(ops: ~[init_op], es: ~[@expr]) -> ~[binding] {
-    let mut bindings: ~[binding] = ~[];
-    let mut i = 0u;
-    for ops.each |op| {
-        vec::push(bindings,
-                  {lhs: ~[call], rhs: Some({op: op, expr: es[i]})});
-        i += 1u;
-    }
-    return bindings;
-}
-
-//
-// Local Variables:
-// mode: rust
-// fill-column: 78;
-// indent-tabs-mode: nil
-// c-basic-offset: 4
-// buffer-file-coding-system: utf-8-unix
-// End:
-//
diff --git a/src/rustc/middle/tstate/ck.rs b/src/rustc/middle/tstate/ck.rs
deleted file mode 100644
index b0b99fcf96c..00000000000
--- a/src/rustc/middle/tstate/ck.rs
+++ /dev/null
@@ -1,153 +0,0 @@
-
-use syntax::ast;
-use ast::{stmt, fn_ident, node_id, crate, return_val, noreturn, expr};
-use syntax::{visit, print};
-use syntax::codemap::span;
-use middle::ty;
-use tstate::ann::{precond, prestate,
-                     implies, ann_precond, ann_prestate};
-use aux::*;
-
-use util::ppaux::ty_to_str;
-use bitvectors::*;
-use annotate::annotate_crate;
-use collect_locals::mk_f_to_fn_info;
-use pre_post_conditions::fn_pre_post;
-use states::find_pre_post_state_fn;
-use syntax::print::pprust::expr_to_str;
-use driver::session::session;
-use std::map::hashmap;
-
-fn check_states_expr(e: @expr, fcx: fn_ctxt, v: visit::vt<fn_ctxt>) {
-    visit::visit_expr(e, fcx, v);
-
-    let prec: precond = expr_precond(fcx.ccx, e);
-    let pres: prestate = expr_prestate(fcx.ccx, e);
-
-    if !implies(pres, prec) {
-        let mut s = ~"";
-        let diff = first_difference_string(fcx, prec, pres);
-        s +=
-            ~"unsatisfied precondition constraint (for example, " + diff +
-                ~") for expression:\n";
-        s += syntax::print::pprust::expr_to_str(e);
-        s += ~"\nprecondition:\n";
-        s += tritv_to_str(fcx, prec);
-        s += ~"\nprestate:\n";
-        s += tritv_to_str(fcx, pres);
-        fcx.ccx.tcx.sess.span_fatal(e.span, s);
-    }
-}
-
-fn check_states_stmt(s: @stmt, fcx: fn_ctxt, v: visit::vt<fn_ctxt>) {
-    visit::visit_stmt(s, fcx, v);
-
-    let a = stmt_to_ann(fcx.ccx, *s);
-    let prec: precond = ann_precond(a);
-    let pres: prestate = ann_prestate(a);
-
-    debug!("check_states_stmt:");
-    log(debug, print::pprust::stmt_to_str(*s));
-    debug!("prec = ");
-    log_tritv(fcx, prec);
-    debug!("pres = ");
-    log_tritv(fcx, pres);
-
-    if !implies(pres, prec) {
-        let mut ss = ~"";
-        let diff = first_difference_string(fcx, prec, pres);
-        ss +=
-            ~"unsatisfied precondition constraint (for example, " + diff +
-                ~") for statement:\n";
-        ss += syntax::print::pprust::stmt_to_str(*s);
-        ss += ~"\nprecondition:\n";
-        ss += tritv_to_str(fcx, prec);
-        ss += ~"\nprestate: \n";
-        ss += tritv_to_str(fcx, pres);
-        fcx.ccx.tcx.sess.span_fatal(s.span, ss);
-    }
-}
-
-fn check_states_against_conditions(fcx: fn_ctxt,
-                                   fk: visit::fn_kind,
-                                   f_decl: ast::fn_decl,
-                                   f_body: ast::blk,
-                                   sp: span,
-                                   id: node_id) {
-    /* Postorder traversal instead of pre is important
-       because we want the smallest possible erroneous statement
-       or expression. */
-    let visitor = visit::mk_vt(
-        @{visit_stmt: check_states_stmt,
-          visit_expr: check_states_expr,
-          visit_fn: |a,b,c,d,e,f,g| {
-              do_nothing::<fn_ctxt>(a, b, c, d, e, f, g)
-          }
-          with *visit::default_visitor::<fn_ctxt>()});
-    visit::visit_fn(fk, f_decl, f_body, sp, id, fcx, visitor);
-}
-
-fn check_fn_states(fcx: fn_ctxt,
-                   fk: visit::fn_kind,
-                   f_decl: ast::fn_decl,
-                   f_body: ast::blk,
-                   sp: span,
-                   id: node_id) {
-    /* Compute the pre- and post-states for this function */
-
-    // Fixpoint iteration
-    while find_pre_post_state_fn(fcx, f_decl, f_body) { }
-
-    /* Now compare each expr's pre-state to its precondition
-       and post-state to its postcondition */
-
-    check_states_against_conditions(fcx, fk, f_decl, f_body, sp, id);
-}
-
-fn fn_states(fk: visit::fn_kind, f_decl: ast::fn_decl, f_body: ast::blk,
-             sp: span, id: node_id,
-             ccx: crate_ctxt, v: visit::vt<crate_ctxt>) {
-
-    visit::visit_fn(fk, f_decl, f_body, sp, id, ccx, v);
-
-    // We may not care about typestate for this function if it contains
-    // no constrained calls
-    if !ccx.fm.get(id).ignore {
-        /* Look up the var-to-bit-num map for this function */
-
-        let f_info = ccx.fm.get(id);
-        let name = visit::name_of_fn(fk);
-        let fcx = {enclosing: f_info, id: id, name: name, ccx: ccx};
-        check_fn_states(fcx, fk, f_decl, f_body, sp, id)
-    }
-}
-
-fn check_crate(cx: ty::ctxt, crate: @crate) {
-    let ccx: crate_ctxt = new_crate_ctxt(cx);
-    /* Build the global map from function id to var-to-bit-num-map */
-
-    mk_f_to_fn_info(ccx, crate);
-    /* Add a blank ts_ann for every statement (and expression) */
-
-    annotate_crate(ccx, *crate);
-    /* Compute the pre and postcondition for every subexpression */
-
-    let vtor = visit::default_visitor::<crate_ctxt>();
-    let vtor = @{visit_fn: fn_pre_post with *vtor};
-    visit::visit_crate(*crate, ccx, visit::mk_vt(vtor));
-
-    /* Check the pre- and postcondition against the pre- and poststate
-       for every expression */
-    let vtor = visit::default_visitor::<crate_ctxt>();
-    let vtor = @{visit_fn: fn_states with *vtor};
-    visit::visit_crate(*crate, ccx, visit::mk_vt(vtor));
-}
-//
-// Local Variables:
-// mode: rust
-// fill-column: 78;
-// indent-tabs-mode: nil
-// c-basic-offset: 4
-// buffer-file-coding-system: utf-8-unix
-// End:
-//
diff --git a/src/rustc/middle/tstate/collect_locals.rs b/src/rustc/middle/tstate/collect_locals.rs
deleted file mode 100644
index 3a1a54b7946..00000000000
--- a/src/rustc/middle/tstate/collect_locals.rs
+++ /dev/null
@@ -1,165 +0,0 @@
-use option::*;
-use pat_util::*;
-use syntax::ast::*;
-use syntax::ast_util::*;
-use syntax::visit;
-use syntax::codemap::span;
-use syntax::ast_util::respan;
-use driver::session::session;
-use aux::*;
-use std::map::hashmap;
-use dvec::{dvec, extensions};
-
-type ctxt = {cs: @mut ~[sp_constr], tcx: ty::ctxt};
-
-fn collect_pred(e: @expr, cx: ctxt, v: visit::vt<ctxt>) {
-    match e.node {
-      expr_check(_, ch) { vec::push(*cx.cs, expr_to_constr(cx.tcx, ch)); }
-      expr_if_check(ex, _, _) {
-        vec::push(*cx.cs, expr_to_constr(cx.tcx, ex));
-      }
-
-      // If it's a call, generate appropriate instances of the
-      // call's constraints.
-      expr_call(operator, operands, _) {
-        for constraints_expr(cx.tcx, operator).each |c| {
-            let ct: sp_constr =
-                respan(c.span,
-                       aux::substitute_constr_args(cx.tcx, operands, c));
-            vec::push(*cx.cs, ct);
-        }
-      }
-      _ { }
-    }
-    // visit subexpressions
-    visit::visit_expr(e, cx, v);
-}
-
-fn find_locals(tcx: ty::ctxt,
-               fk: visit::fn_kind,
-               f_decl: fn_decl,
-               f_body: blk,
-               sp: span,
-               id: node_id) -> ctxt {
-    let cx: ctxt = {cs: @mut ~[], tcx: tcx};
-    let visitor = visit::default_visitor::<ctxt>();
-    let visitor =
-        @{visit_expr: collect_pred,
-          visit_fn: do_nothing
-          with *visitor};
-    visit::visit_fn(fk, f_decl, f_body, sp,
-                    id, cx, visit::mk_vt(visitor));
-    return cx;
-}
-
-fn add_constraint(tcx: ty::ctxt, c: sp_constr, next: uint, tbl: constr_map) ->
-   uint {
-    log(debug,
-             constraint_to_str(tcx, c) + ~" |-> " + uint::str(next));
-
-    let {path: p, def_id: d_id, args: args} = c.node;
-    match tbl.find(d_id) {
-      Some(ct) {
-        (*ct.descs).push(respan(c.span, {args: args, bit_num: next}));
-      }
-      None {
-        let rslt = @dvec();
-        (*rslt).push(respan(c.span, {args: args, bit_num: next}));
-        tbl.insert(d_id, {path:p, descs:rslt});
-      }
-    }
-    return next + 1u;
-}
-
-fn contains_constrained_calls(tcx: ty::ctxt, body: blk) -> bool {
-    type cx = @{
-        tcx: ty::ctxt,
-        mut has: bool
-    };
-    let cx = @{
-        tcx: tcx,
-        mut has: false
-    };
-    let vtor = visit::default_visitor::<cx>();
-    let vtor = @{visit_expr: visit_expr with *vtor};
-    visit::visit_block(body, cx, visit::mk_vt(vtor));
-    return cx.has;
-
-    fn visit_expr(e: @expr, &&cx: cx, v: visit::vt<cx>) {
-        import syntax::print::pprust;
-        debug!("visiting %?", pprust::expr_to_str(e));
-
-        visit::visit_expr(e, cx, v);
-
-        if constraints_expr(cx.tcx, e).is_not_empty() {
-            debug!("has constraints");
-            cx.has = true;
-        } else {
-            debug!("has not constraints");
-        }
-    }
-}
-
-/* builds a table mapping each local var defined in f
-   to a bit number in the precondition/postcondition vectors */
-fn mk_fn_info(ccx: crate_ctxt,
-              fk: visit::fn_kind,
-              f_decl: fn_decl,
-              f_body: blk,
-              f_sp: span,
-              id: node_id) {
-    let name = visit::name_of_fn(fk);
-    let res_map = new_def_hash::<constraint>();
-    let mut next: uint = 0u;
-
-    let cx: ctxt = find_locals(ccx.tcx, fk, f_decl, f_body, f_sp, id);
-    /* now we have to add bit nums for both the constraints
-       and the variables... */
-
-    let ignore = !contains_constrained_calls(ccx.tcx, f_body);
-
-    if !ignore {
-        let mut i = 0u, l = vec::len(*cx.cs);
-        while i < l {
-            next = add_constraint(cx.tcx, copy cx.cs[i], next, res_map);
-            i += 1u;
-        }
-        /* if this function has any constraints, instantiate them to the
-        argument names and add them */
-        for f_decl.constraints.each |c| {
-            let sc = ast_constr_to_sp_constr(cx.tcx, f_decl.inputs, c);
-            next = add_constraint(cx.tcx, sc, next, res_map);
-        }
-    }
-
-    let v: @mut ~[node_id] = @mut ~[];
-    let rslt =
-        {constrs: res_map,
-         num_constraints: next,
-         cf: f_decl.cf,
-         used_vars: v,
-         ignore: ignore};
-    ccx.fm.insert(id, rslt);
-    debug!("%s has %u constraints", *name, num_constraints(rslt));
-}
-
-
-/* initializes the global fn_info_map (mapping each function ID, including
-   nested locally defined functions, onto a mapping from local variable name
-   to bit number) */
-fn mk_f_to_fn_info(ccx: crate_ctxt, c: @crate) {
-    let visitor =
-        visit::mk_simple_visitor(@{
-            visit_fn: |a,b,c,d,e| mk_fn_info(ccx, a, b, c, d, e)
-            with *visit::default_simple_visitor()});
-    visit::visit_crate(*c, (), visitor);
-}
-//
-// Local Variables:
-// mode: rust
-// fill-column: 78;
-// indent-tabs-mode: nil
-// c-basic-offset: 4
-// buffer-file-coding-system: utf-8-unix
-// End:
-//
diff --git a/src/rustc/middle/tstate/pre_post_conditions.rs b/src/rustc/middle/tstate/pre_post_conditions.rs
deleted file mode 100644
index 5314a0a3d54..00000000000
--- a/src/rustc/middle/tstate/pre_post_conditions.rs
+++ /dev/null
@@ -1,617 +0,0 @@
-use tstate::ann::*;
-use aux::*;
-use bitvectors::{bit_num, seq_preconds, seq_postconds,
-                    intersect_states,
-                    relax_precond_block, gen};
-use tritv::*;
-
-use pat_util::*;
-use syntax::ast::*;
-use syntax::ast_util::*;
-use syntax::print::pprust::{expr_to_str, stmt_to_str};
-use syntax::visit;
-use util::common::{field_exprs, has_nonlocal_exits};
-use syntax::codemap::span;
-use driver::session::session;
-use std::map::hashmap;
-
-fn find_pre_post_mod(_m: _mod) -> _mod {
-    debug!("implement find_pre_post_mod!");
-    fail;
-}
-
-fn find_pre_post_foreign_mod(_m: foreign_mod) -> foreign_mod {
-    debug!("implement find_pre_post_foreign_mod");
-    fail;
-}
-
-fn find_pre_post_method(ccx: crate_ctxt, m: @method) {
-    assert (ccx.fm.contains_key(m.id));
-    let fcx: fn_ctxt =
-        {enclosing: ccx.fm.get(m.id),
-         id: m.id,
-         name: m.ident,
-         ccx: ccx};
-    find_pre_post_fn(fcx, m.body);
-}
-
-fn find_pre_post_item(ccx: crate_ctxt, i: item) {
-    match i.node {
-      item_const(_, e) {
-          // do nothing -- item_consts don't refer to local vars
-      }
-      item_fn(_, _, body) {
-        assert (ccx.fm.contains_key(i.id));
-        let fcx =
-            {enclosing: ccx.fm.get(i.id), id: i.id, name: i.ident, ccx: ccx};
-        find_pre_post_fn(fcx, body);
-      }
-      item_mod(m) { find_pre_post_mod(m); }
-      item_foreign_mod(nm) { find_pre_post_foreign_mod(nm); }
-      item_ty(*) | item_enum(*) | item_trait(*) { return; }
-      item_class(*) {
-          fail ~"find_pre_post_item: shouldn't be called on item_class";
-      }
-      item_impl(_, _, _, ms) {
-        for ms.each |m| { find_pre_post_method(ccx, m); }
-      }
-      item_mac(*) { fail ~"item macros unimplemented" }
-    }
-}
-
-
-/* Finds the pre and postcondition for each expr in <args>;
-   sets the precondition in a to be the result of combining
-   the preconditions for <args>, and the postcondition in a to
-   be the union of all postconditions for <args> */
-fn find_pre_post_exprs(fcx: fn_ctxt, args: ~[@expr], id: node_id) {
-    if vec::len::<@expr>(args) > 0u {
-        debug!("find_pre_post_exprs: oper = %s", expr_to_str(args[0]));
-    }
-    fn do_one(fcx: fn_ctxt, e: @expr) { find_pre_post_expr(fcx, e); }
-    for args.each |e| { do_one(fcx, e); }
-
-    fn get_pp(ccx: crate_ctxt, &&e: @expr) -> pre_and_post {
-        return expr_pp(ccx, e);
-    }
-    let pps = vec::map(args, |a| get_pp(fcx.ccx, a) );
-
-    set_pre_and_post(fcx.ccx, id, seq_preconds(fcx, pps),
-                     seq_postconds(fcx, vec::map(pps, get_post)));
-}
-
-fn find_pre_post_loop(fcx: fn_ctxt, index: @expr, body: blk, id: node_id) {
-    find_pre_post_expr(fcx, index);
-    find_pre_post_block(fcx, body);
-
-    let loop_precond =
-        seq_preconds(fcx, ~[expr_pp(fcx.ccx, index),
-                           block_pp(fcx.ccx, body)]);
-    let loop_postcond =
-        intersect_states(expr_postcond(fcx.ccx, index),
-                         block_postcond(fcx.ccx, body));
-    copy_pre_post_(fcx.ccx, id, loop_precond, loop_postcond);
-}
-
-// Generates a pre/post assuming that a is the
-// annotation for an if-expression with consequent conseq
-// and alternative maybe_alt
-fn join_then_else(fcx: fn_ctxt, antec: @expr, conseq: blk,
-                  maybe_alt: Option<@expr>, id: node_id, chck: if_ty) {
-    find_pre_post_expr(fcx, antec);
-    find_pre_post_block(fcx, conseq);
-    match maybe_alt {
-      none {
-        match chck {
-          if_check {
-            let c: sp_constr = expr_to_constr(fcx.ccx.tcx, antec);
-            gen(fcx, antec.id, c.node);
-          }
-          _ { }
-        }
-
-        let precond_res =
-            seq_preconds(fcx,
-                         ~[expr_pp(fcx.ccx, antec),
-                          block_pp(fcx.ccx, conseq)]);
-        set_pre_and_post(fcx.ccx, id, precond_res,
-                         expr_poststate(fcx.ccx, antec));
-      }
-      Some(altern) {
-        /*
-          if check = if_check, then
-          be sure that the predicate implied by antec
-          is *not* true in the alternative
-         */
-        find_pre_post_expr(fcx, altern);
-        let precond_false_case =
-            seq_preconds(fcx,
-                         ~[expr_pp(fcx.ccx, antec),
-                          expr_pp(fcx.ccx, altern)]);
-        let postcond_false_case =
-            seq_postconds(fcx,
-                          ~[expr_postcond(fcx.ccx, antec),
-                           expr_postcond(fcx.ccx, altern)]);
-
-        /* Be sure to set the bit for the check condition here,
-         so that it's *not* set in the alternative. */
-        match chck {
-          if_check {
-            let c: sp_constr = expr_to_constr(fcx.ccx.tcx, antec);
-            gen(fcx, antec.id, c.node);
-          }
-          _ { }
-        }
-        let precond_true_case =
-            seq_preconds(fcx,
-                         ~[expr_pp(fcx.ccx, antec),
-                          block_pp(fcx.ccx, conseq)]);
-        let postcond_true_case =
-            seq_postconds(fcx,
-                          ~[expr_postcond(fcx.ccx, antec),
-                           block_postcond(fcx.ccx, conseq)]);
-
-        let precond_res =
-            seq_postconds(fcx, ~[precond_true_case, precond_false_case]);
-        let postcond_res =
-            intersect_states(postcond_true_case, postcond_false_case);
-        set_pre_and_post(fcx.ccx, id, precond_res, postcond_res);
-      }
-    }
-}
-
-fn gen_if_local(fcx: fn_ctxt, lhs: @expr, rhs: @expr, larger_id: node_id,
-                new_var: node_id) {
-    match node_id_to_def(fcx.ccx, new_var) {
-      Some(d) {
-        match d {
-          def_local(nid, _) {
-            find_pre_post_expr(fcx, rhs);
-            let p = expr_pp(fcx.ccx, rhs);
-            set_pre_and_post(fcx.ccx, larger_id, p.precondition,
-                             p.postcondition);
-          }
-          _ { find_pre_post_exprs(fcx, ~[lhs, rhs], larger_id); }
-        }
-      }
-      _ { find_pre_post_exprs(fcx, ~[lhs, rhs], larger_id); }
-    }
-}
-
-fn handle_update(fcx: fn_ctxt, parent: @expr, lhs: @expr, rhs: @expr,
-                 ty: oper_type) {
-    find_pre_post_expr(fcx, rhs);
-    match lhs.node {
-      expr_path(p) {
-        let post = expr_postcond(fcx.ccx, parent);
-        let tmp = post.clone();
-
-        match ty {
-          oper_move {
-            if is_path(rhs) { forget_in_postcond(fcx, parent.id, rhs.id); }
-          }
-          oper_swap {
-            forget_in_postcond(fcx, parent.id, lhs.id);
-            forget_in_postcond(fcx, parent.id, rhs.id);
-          }
-          oper_assign {
-            forget_in_postcond(fcx, parent.id, lhs.id);
-          }
-          _ { }
-        }
-
-        gen_if_local(fcx, lhs, rhs, parent.id, lhs.id);
-        match rhs.node {
-          expr_path(p1) {
-            let d = local_node_id_to_local_def_id(fcx, lhs.id);
-            let d1 = local_node_id_to_local_def_id(fcx, rhs.id);
-            match d {
-              Some(id) {
-                match d1 {
-                  Some(id1) {
-                    let instlhs =
-                        {ident: path_to_ident(p), node: id};
-                    let instrhs =
-                        {ident: path_to_ident(p1), node: id1};
-                    copy_in_poststate_two(fcx, tmp, post, instlhs, instrhs,
-                                          ty);
-                  }
-                  _ { }
-                }
-              }
-              _ { }
-            }
-          }
-          _ {/* do nothing */ }
-        }
-      }
-      _ { find_pre_post_expr(fcx, lhs); }
-    }
-}
-
-fn forget_args_moved_in(fcx: fn_ctxt, parent: @expr, modes: ~[mode],
-                        operands: ~[@expr]) {
-    do vec::iteri(modes) |i,mode| {
-        match ty::resolved_mode(fcx.ccx.tcx, mode) {
-          by_move { forget_in_postcond(fcx, parent.id, operands[i].id); }
-          by_ref | by_val | by_mutbl_ref | by_copy { }
-        }
-    }
-}
-
-fn find_pre_post_expr_fn_upvars(fcx: fn_ctxt, e: @expr) {
-    let rslt = expr_pp(fcx.ccx, e);
-    clear_pp(rslt);
-}
-
-/* Fills in annotations as a side effect. Does not rebuild the expr */
-fn find_pre_post_expr(fcx: fn_ctxt, e: @expr) {
-    let enclosing = fcx.enclosing;
-    let num_local_vars = num_constraints(enclosing);
-    fn do_rand_(fcx: fn_ctxt, e: @expr) { find_pre_post_expr(fcx, e); }
-
-
-    match e.node {
-      expr_call(operator, operands, _) {
-        /* copy */
-
-        let mut args = operands;
-        vec::push(args, operator);
-
-        find_pre_post_exprs(fcx, args, e.id);
-        /* see if the call has any constraints on its type */
-        for constraints_expr(fcx.ccx.tcx, operator).each |c| {
-            let i =
-                bit_num(fcx, substitute_constr_args(fcx.ccx.tcx, args, c));
-            require(i, expr_pp(fcx.ccx, e));
-        }
-
-        forget_args_moved_in(fcx, e, callee_modes(fcx, operator.id),
-                             operands);
-
-        /* if this is a failing call, its postcondition sets everything */
-        match controlflow_expr(fcx.ccx, operator) {
-          noreturn { set_postcond_false(fcx.ccx, e.id); }
-          _ { }
-        }
-      }
-      expr_vstore(ee, _) {
-        find_pre_post_expr(fcx, ee);
-        let p = expr_pp(fcx.ccx, ee);
-        set_pre_and_post(fcx.ccx, e.id, p.precondition, p.postcondition);
-      }
-      expr_vec(args, _) {
-        find_pre_post_exprs(fcx, args, e.id);
-      }
-      expr_path(p) {
-        let rslt = expr_pp(fcx.ccx, e);
-        clear_pp(rslt);
-      }
-      expr_new(p, _, v) {
-        find_pre_post_exprs(fcx, ~[p, v], e.id);
-      }
-      expr_log(_, lvl, arg) {
-        find_pre_post_exprs(fcx, ~[lvl, arg], e.id);
-      }
-      expr_fn(_, _, _, cap_clause) | expr_fn_block(_, _, cap_clause) {
-        find_pre_post_expr_fn_upvars(fcx, e);
-
-        for (*cap_clause).each |cap_item| {
-            let d = local_node_id_to_local_def_id(fcx, cap_item.id);
-            option::iter(d, |id| use_var(fcx, id) );
-        }
-
-        for (*cap_clause).each |cap_item| {
-            if cap_item.is_move {
-                log(debug, (~"forget_in_postcond: ", cap_item));
-                forget_in_postcond(fcx, e.id, cap_item.id);
-            }
-        }
-      }
-      expr_block(b) {
-        find_pre_post_block(fcx, b);
-        let p = block_pp(fcx.ccx, b);
-        set_pre_and_post(fcx.ccx, e.id, p.precondition, p.postcondition);
-      }
-      expr_rec(fields, maybe_base) {
-        let mut es = field_exprs(fields);
-        match maybe_base { none {/* no-op */ } Some(b) { vec::push(es, b); } }
-        find_pre_post_exprs(fcx, es, e.id);
-      }
-      expr_tup(elts) { find_pre_post_exprs(fcx, elts, e.id); }
-      expr_move(lhs, rhs) { handle_update(fcx, e, lhs, rhs, oper_move); }
-      expr_swap(lhs, rhs) { handle_update(fcx, e, lhs, rhs, oper_swap); }
-      expr_assign(lhs, rhs) { handle_update(fcx, e, lhs, rhs, oper_assign); }
-      expr_assign_op(_, lhs, rhs) {
-        /* Different from expr_assign in that the lhs *must*
-           already be initialized */
-
-        find_pre_post_exprs(fcx, ~[lhs, rhs], e.id);
-        forget_in_postcond(fcx, e.id, lhs.id);
-      }
-      expr_lit(_) { clear_pp(expr_pp(fcx.ccx, e)); }
-      expr_ret(maybe_val) {
-        match maybe_val {
-          none {
-            clear_precond(fcx.ccx, e.id);
-            set_postcond_false(fcx.ccx, e.id);
-          }
-          Some(ret_val) {
-            find_pre_post_expr(fcx, ret_val);
-            set_precondition(node_id_to_ts_ann(fcx.ccx, e.id),
-                             expr_precond(fcx.ccx, ret_val));
-            set_postcond_false(fcx.ccx, e.id);
-          }
-        }
-      }
-      expr_if(antec, conseq, maybe_alt) {
-        join_then_else(fcx, antec, conseq, maybe_alt, e.id, plain_if);
-      }
-      expr_binary(bop, l, r) {
-        if lazy_binop(bop) {
-            find_pre_post_expr(fcx, l);
-            find_pre_post_expr(fcx, r);
-            let overall_pre =
-                seq_preconds(fcx,
-                             ~[expr_pp(fcx.ccx, l), expr_pp(fcx.ccx, r)]);
-            set_precondition(node_id_to_ts_ann(fcx.ccx, e.id), overall_pre);
-            set_postcondition(node_id_to_ts_ann(fcx.ccx, e.id),
-                              expr_postcond(fcx.ccx, l));
-        } else { find_pre_post_exprs(fcx, ~[l, r], e.id); }
-      }
-      expr_addr_of(_, x) | expr_cast(x, _) | expr_unary(_, x) |
-      expr_loop_body(x) | expr_do_body(x) | expr_assert(x) | expr_copy(x) {
-        find_pre_post_expr(fcx, x);
-        copy_pre_post(fcx.ccx, e.id, x);
-      }
-      expr_while(test, body) {
-        find_pre_post_expr(fcx, test);
-        find_pre_post_block(fcx, body);
-        set_pre_and_post(fcx.ccx, e.id,
-                         seq_preconds(fcx,
-                                      ~[expr_pp(fcx.ccx, test),
-                                       block_pp(fcx.ccx, body)]),
-                         intersect_states(expr_postcond(fcx.ccx, test),
-                                          block_postcond(fcx.ccx, body)));
-      }
-      expr_loop(body) {
-        find_pre_post_block(fcx, body);
-        /* Infinite loop: if control passes it, everything is true. */
-        let mut loop_postcond = false_postcond(num_local_vars);
-        /* Conservative approximation: if the body has any nonlocal exits,
-         the poststate is blank since we don't know what parts of it
-          execute. */
-        if has_nonlocal_exits(body) {
-            loop_postcond = empty_poststate(num_local_vars);
-        }
-        set_pre_and_post(fcx.ccx, e.id, block_precond(fcx.ccx, body),
-                         loop_postcond);
-      }
-      expr_index(val, sub) { find_pre_post_exprs(fcx, ~[val, sub], e.id); }
-      expr_match(ex, alts, _) {
-        find_pre_post_expr(fcx, ex);
-        fn do_an_alt(fcx: fn_ctxt, an_alt: arm) -> pre_and_post {
-            match an_alt.guard {
-              Some(e) { find_pre_post_expr(fcx, e); }
-              _ {}
-            }
-            find_pre_post_block(fcx, an_alt.body);
-            return block_pp(fcx.ccx, an_alt.body);
-        }
-        let mut alt_pps = ~[];
-        for alts.each |a| { vec::push(alt_pps, do_an_alt(fcx, a)); }
-        fn combine_pp(antec: pre_and_post, fcx: fn_ctxt, &&pp: pre_and_post,
-                      &&next: pre_and_post) -> pre_and_post {
-            union(pp.precondition, seq_preconds(fcx, ~[antec, next]));
-            intersect(pp.postcondition, next.postcondition);
-            return pp;
-        }
-        let antec_pp = pp_clone(expr_pp(fcx.ccx, ex));
-        let e_pp =
-            {precondition: empty_prestate(num_local_vars),
-             postcondition: false_postcond(num_local_vars)};
-        let g = |a,b| combine_pp(antec_pp, fcx, a, b);
-        let alts_overall_pp =
-            vec::foldl(e_pp, alt_pps, g);
-        set_pre_and_post(fcx.ccx, e.id, alts_overall_pp.precondition,
-                         alts_overall_pp.postcondition);
-      }
-      expr_field(operator, _, _) {
-        find_pre_post_expr(fcx, operator);
-        copy_pre_post(fcx.ccx, e.id, operator);
-      }
-      expr_fail(maybe_val) {
-        let mut prestate;
-        match maybe_val {
-          none { prestate = empty_prestate(num_local_vars); }
-          Some(fail_val) {
-            find_pre_post_expr(fcx, fail_val);
-            prestate = expr_precond(fcx.ccx, fail_val);
-          }
-        }
-        set_pre_and_post(fcx.ccx, e.id,
-                         /* if execution continues after fail,
-                            then everything is true! */
-                         prestate, false_postcond(num_local_vars));
-      }
-      expr_check(_, p) {
-        find_pre_post_expr(fcx, p);
-        copy_pre_post(fcx.ccx, e.id, p);
-        /* predicate p holds after this expression executes */
-
-        let c: sp_constr = expr_to_constr(fcx.ccx.tcx, p);
-        gen(fcx, e.id, c.node);
-      }
-      expr_if_check(p, conseq, maybe_alt) {
-        join_then_else(fcx, p, conseq, maybe_alt, e.id, if_check);
-      }
-      expr_break { clear_pp(expr_pp(fcx.ccx, e)); }
-      expr_again { clear_pp(expr_pp(fcx.ccx, e)); }
-      expr_mac(_) { fcx.ccx.tcx.sess.bug(~"unexpanded macro"); }
-    }
-}
-
-fn find_pre_post_stmt(fcx: fn_ctxt, s: stmt) {
-    debug!("stmt = %s", stmt_to_str(s));
-    match s.node {
-      stmt_decl(adecl, id) {
-        match adecl.node {
-          decl_local(alocals) {
-            let prev_pp = empty_pre_post(num_constraints(fcx.enclosing));
-            for alocals.each |alocal| {
-                match alocal.node.init {
-                  Some(an_init) {
-                    /* LHS always becomes initialized,
-                     whether or not this is a move */
-                    find_pre_post_expr(fcx, an_init.expr);
-                    do pat_bindings(fcx.ccx.tcx.def_map, alocal.node.pat)
-                        |p_id, _s, _n| {
-                        copy_pre_post(fcx.ccx, p_id, an_init.expr);
-                    };
-                    /* Inherit ann from initializer, and add var being
-                       initialized to the postcondition */
-                    copy_pre_post(fcx.ccx, id, an_init.expr);
-
-                    let mut p = none;
-                    match an_init.expr.node {
-                      expr_path(_p) { p = Some(_p); }
-                      _ { }
-                    }
-
-                    do pat_bindings(fcx.ccx.tcx.def_map, alocal.node.pat)
-                        |p_id, _s, n| {
-                        let ident = path_to_ident(n);
-                        match p {
-                          Some(p) {
-                            copy_in_postcond(fcx, id,
-                                             {ident: ident, node: p_id},
-                                             {ident:
-                                                  path_to_ident(p),
-                                              node: an_init.expr.id},
-                                             op_to_oper_ty(an_init.op));
-                          }
-                          none { }
-                        }
-                    };
-
-                    /* Clear out anything that the previous initializer
-                    guaranteed */
-                    let e_pp = expr_pp(fcx.ccx, an_init.expr);
-                    prev_pp.precondition.become(
-                               seq_preconds(fcx, ~[prev_pp, e_pp]));
-
-                    /* Include the LHSs too, since those aren't in the
-                     postconds of the RHSs themselves */
-                    copy_pre_post_(fcx.ccx, id, prev_pp.precondition,
-                                   prev_pp.postcondition);
-                  }
-                  none {
-                    do pat_bindings(fcx.ccx.tcx.def_map, alocal.node.pat)
-                        |p_id, _s, _n| {
-                        clear_pp(node_id_to_ts_ann(fcx.ccx, p_id).conditions);
-                    };
-                    clear_pp(node_id_to_ts_ann(fcx.ccx, id).conditions);
-                  }
-                }
-            }
-          }
-          decl_item(anitem) {
-            clear_pp(node_id_to_ts_ann(fcx.ccx, id).conditions);
-            find_pre_post_item(fcx.ccx, *anitem);
-          }
-        }
-      }
-      stmt_expr(e, id) | stmt_semi(e, id) {
-        find_pre_post_expr(fcx, e);
-        copy_pre_post(fcx.ccx, id, e);
-      }
-    }
-}
-
-fn find_pre_post_block(fcx: fn_ctxt, b: blk) {
-    /* Want to say that if there is a break or cont in this
-     block, then that invalidates the poststate upheld by
-    any of the stmts after it.
-    Given that the typechecker has run, we know any break will be in
-    a block that forms a loop body. So that's ok. There'll never be an
-    expr_break outside a loop body, therefore, no expr_break outside a block.
-    */
-
-    /* Conservative approximation for now: This says that if a block contains
-     *any* breaks or conts, then its postcondition doesn't promise anything.
-     This will mean that:
-     x = 0;
-     break;
-
-     won't have a postcondition that says x is initialized, but that's ok.
-     */
-
-    let nv = num_constraints(fcx.enclosing);
-    fn do_one_(fcx: fn_ctxt, s: @stmt) {
-        find_pre_post_stmt(fcx, *s);
-    }
-    for b.node.stmts.each |s| { do_one_(fcx, s); }
-    fn do_inner_(fcx: fn_ctxt, &&e: @expr) { find_pre_post_expr(fcx, e); }
-    let do_inner = |a| do_inner_(fcx, a);
-    option::map::<@expr, ()>(b.node.expr, do_inner);
-
-    let mut pps: ~[pre_and_post] = ~[];
-    for b.node.stmts.each |s| { vec::push(pps, stmt_pp(fcx.ccx, *s)); }
-    match b.node.expr {
-      none {/* no-op */ }
-      Some(e) { vec::push(pps, expr_pp(fcx.ccx, e)); }
-    }
-
-    let block_precond = seq_preconds(fcx, pps);
-
-    let mut postconds = ~[];
-    for pps.each |pp| { vec::push(postconds, get_post(pp)); }
-
-    /* A block may be empty, so this next line ensures that the postconds
-       vector is non-empty. */
-    vec::push(postconds, block_precond);
-
-    let mut block_postcond = empty_poststate(nv);
-    /* conservative approximation */
-
-    if !has_nonlocal_exits(b) {
-        block_postcond = seq_postconds(fcx, postconds);
-    }
-    set_pre_and_post(fcx.ccx, b.node.id, block_precond, block_postcond);
-}
-
-fn find_pre_post_fn(fcx: fn_ctxt, body: blk) {
-    find_pre_post_block(fcx, body);
-
-    // Treat the tail expression as a return statement
-    match body.node.expr {
-      Some(tailexpr) { set_postcond_false(fcx.ccx, tailexpr.id); }
-      none {/* fallthrough */ }
-    }
-}
-
-fn fn_pre_post(fk: visit::fn_kind, decl: fn_decl, body: blk, sp: span,
-               id: node_id,
-               ccx: crate_ctxt, v: visit::vt<crate_ctxt>) {
-
-    visit::visit_fn(fk, decl, body, sp, id, ccx, v);
-    assert (ccx.fm.contains_key(id));
-    if !ccx.fm.get(id).ignore {
-        let fcx =
-            {enclosing: ccx.fm.get(id),
-             id: id,
-             name: visit::name_of_fn(fk),
-             ccx: ccx};
-        find_pre_post_fn(fcx, body);
-    }
-}
-
-//
-// Local Variables:
-// mode: rust
-// fill-column: 78;
-// indent-tabs-mode: nil
-// c-basic-offset: 4
-// buffer-file-coding-system: utf-8-unix
-// End:
-//
diff --git a/src/rustc/middle/tstate/states.rs b/src/rustc/middle/tstate/states.rs
deleted file mode 100644
index 369f328a72b..00000000000
--- a/src/rustc/middle/tstate/states.rs
+++ /dev/null
@@ -1,623 +0,0 @@
-use ann::*;
-use aux::*;
-use tritv::*;
-
-use syntax::print::pprust::block_to_str;
-use bitvectors::*;
-use pat_util::*;
-use syntax::ast::*;
-use syntax::ast_util::*;
-use syntax::print::pprust::{expr_to_str, stmt_to_str};
-use syntax::codemap::span;
-use middle::ty::{expr_ty, type_is_bot};
-use util::common::{field_exprs, has_nonlocal_exits, may_break};
-use driver::session::session;
-use std::map::hashmap;
-
-fn forbid_upvar(fcx: fn_ctxt, rhs_id: node_id, sp: span, t: oper_type) {
-    match t {
-      oper_move {
-        match local_node_id_to_def(fcx, rhs_id) {
-          Some(def_upvar(_, _, _)) {
-            fcx.ccx.tcx.sess.span_err(sp,
-                                      ~"tried to deinitialize a variable \
-              declared in a different scope");
-          }
-          _ { }
-        }
-      }
-      _ {/* do nothing */ }
-    }
-}
-
-fn handle_move_or_copy(fcx: fn_ctxt, post: poststate, rhs_path: @path,
-                       rhs_id: node_id, destlhs: dest, init_op: init_op) {
-    forbid_upvar(fcx, rhs_id, rhs_path.span, op_to_oper_ty(init_op));
-
-    let rhs_d_id = local_node_id_to_def_id(fcx, rhs_id);
-    match rhs_d_id {
-      Some(rhsid) {
-        // RHS is a local var
-        let instrhs =
-            {ident: path_to_ident(rhs_path), node: rhsid.node};
-        match destlhs {
-          local_dest(instlhs) {
-             copy_in_poststate(fcx, post, instlhs, instrhs,
-                               op_to_oper_ty(init_op));
-          }
-          _ {}
-        }
-      }
-      _ {
-        // not a local -- do nothing
-      }
-    }
-}
-
-fn seq_states(fcx: fn_ctxt, pres: prestate, bindings: ~[binding]) ->
-   {changed: bool, post: poststate} {
-    let mut changed = false;
-    let mut post = pres.clone();
-    for bindings.each |b| {
-        match b.rhs {
-          Some(an_init) {
-            // an expression, with or without a destination
-            changed |=
-                find_pre_post_state_expr(fcx, post, an_init.expr) || changed;
-            post = expr_poststate(fcx.ccx, an_init.expr).clone();
-            for b.lhs.each |d| {
-                match an_init.expr.node {
-                  expr_path(p) {
-                    handle_move_or_copy(fcx, post, p, an_init.expr.id, d,
-                                        an_init.op);
-                  }
-                  _ { }
-                }
-            }
-
-            // Forget the RHS if we just moved it.
-            if an_init.op == init_move {
-                forget_in_poststate(fcx, post, an_init.expr.id);
-            }
-          }
-          none {
-          }
-        }
-    }
-    return {changed: changed, post: post};
-}
-
-fn find_pre_post_state_sub(fcx: fn_ctxt, pres: prestate, e: @expr,
-                           parent: node_id, c: Option<tsconstr>) -> bool {
-    let mut changed = find_pre_post_state_expr(fcx, pres, e);
-
-    changed = set_prestate_ann(fcx.ccx, parent, pres) || changed;
-
-    let post = expr_poststate(fcx.ccx, e).clone();
-    match c {
-      none { }
-      Some(c1) { set_in_poststate_(bit_num(fcx, c1), post); }
-    }
-
-    changed = set_poststate_ann(fcx.ccx, parent, post) || changed;
-    return changed;
-}
-
-fn find_pre_post_state_two(fcx: fn_ctxt, pres: prestate, lhs: @expr,
-                           rhs: @expr, parent: node_id, ty: oper_type) ->
-   bool {
-    let mut changed = set_prestate_ann(fcx.ccx, parent, pres);
-    changed = find_pre_post_state_expr(fcx, pres, lhs) || changed;
-    changed =
-        find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, lhs), rhs) ||
-            changed;
-    forbid_upvar(fcx, rhs.id, rhs.span, ty);
-
-    let post = expr_poststate(fcx.ccx, rhs).clone();
-
-    match lhs.node {
-      expr_path(p) {
-        // for termination, need to make sure intermediate changes don't set
-        // changed flag
-        // tmp remembers "old" constraints we'd otherwise forget,
-        // for substitution purposes
-        let tmp = post.clone();
-
-        match ty {
-          oper_move {
-            if is_path(rhs) { forget_in_poststate(fcx, post, rhs.id); }
-            forget_in_poststate(fcx, post, lhs.id);
-          }
-          oper_swap {
-            forget_in_poststate(fcx, post, lhs.id);
-            forget_in_poststate(fcx, post, rhs.id);
-          }
-          _ { forget_in_poststate(fcx, post, lhs.id); }
-        }
-
-        match rhs.node {
-          expr_path(p1) {
-            let d = local_node_id_to_local_def_id(fcx, lhs.id);
-            let d1 = local_node_id_to_local_def_id(fcx, rhs.id);
-            match d {
-              Some(id) {
-                match d1 {
-                  Some(id1) {
-                    let instlhs =
-                        {ident: path_to_ident(p), node: id};
-                    let instrhs =
-                        {ident: path_to_ident(p1), node: id1};
-                    copy_in_poststate_two(fcx, tmp, post, instlhs, instrhs,
-                                          ty);
-                  }
-                  _ { }
-                }
-              }
-              _ { }
-            }
-          }
-          _ {/* do nothing */ }
-        }
-      }
-      _ { }
-    }
-    changed = set_poststate_ann(fcx.ccx, parent, post) || changed;
-    return changed;
-}
-
-fn find_pre_post_state_call(fcx: fn_ctxt, pres: prestate, a: @expr,
-                            id: node_id, ops: ~[init_op], bs: ~[@expr],
-                            cf: ret_style) -> bool {
-    let mut changed = find_pre_post_state_expr(fcx, pres, a);
-    // FIXME (#2178): This could be a typestate constraint (except we're
-    // not using them inside the compiler, I guess... see discussion in
-    // bug)
-    if vec::len(bs) != vec::len(ops) {
-        fcx.ccx.tcx.sess.span_bug(a.span,
-                                  fmt!("mismatched arg lengths: \
-                                        %u exprs vs. %u ops",
-                                       vec::len(bs), vec::len(ops)));
-    }
-    return find_pre_post_state_exprs(fcx, pres, id, ops,
-                                   bs, cf) || changed;
-}
-
-fn find_pre_post_state_exprs(fcx: fn_ctxt, pres: prestate, id: node_id,
-                             ops: ~[init_op], es: ~[@expr],
-                             cf: ret_style) -> bool {
-    let rs = seq_states(fcx, pres, arg_bindings(ops, es));
-    let mut changed = rs.changed | set_prestate_ann(fcx.ccx, id, pres);
-    /* if this is a failing call, it sets everything as initialized */
-    match cf {
-      noreturn {
-        let post = false_postcond(num_constraints(fcx.enclosing));
-        changed |= set_poststate_ann(fcx.ccx, id, post);
-      }
-      _ { changed |= set_poststate_ann(fcx.ccx, id, rs.post); }
-    }
-    return changed;
-}
-
-fn join_then_else(fcx: fn_ctxt, antec: @expr, conseq: blk,
-                  maybe_alt: Option<@expr>, id: node_id, chk: if_ty,
-                  pres: prestate) -> bool {
-    let mut changed =
-        set_prestate_ann(fcx.ccx, id, pres) |
-            find_pre_post_state_expr(fcx, pres, antec);
-
-    match maybe_alt {
-      none {
-        match chk {
-          if_check {
-            let c: sp_constr = expr_to_constr(fcx.ccx.tcx, antec);
-            let conseq_prestate = expr_poststate(fcx.ccx, antec).clone();
-            conseq_prestate.set(bit_num(fcx, c.node), ttrue);
-            changed |=
-                find_pre_post_state_block(fcx, conseq_prestate, conseq) |
-                    set_poststate_ann(fcx.ccx, id,
-                                      expr_poststate(fcx.ccx, antec));
-          }
-          _ {
-            changed |=
-                find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, antec),
-                                          conseq) |
-                    set_poststate_ann(fcx.ccx, id,
-                                      expr_poststate(fcx.ccx, antec));
-          }
-        }
-      }
-      Some(altern) {
-        changed |=
-            find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, antec),
-                                     altern);
-
-        let mut conseq_prestate = expr_poststate(fcx.ccx, antec);
-        match chk {
-          if_check {
-            let c: sp_constr = expr_to_constr(fcx.ccx.tcx, antec);
-            conseq_prestate = conseq_prestate.clone();
-            conseq_prestate.set(bit_num(fcx, c.node),  ttrue);
-          }
-          _ { }
-        }
-
-
-        changed |= find_pre_post_state_block(fcx, conseq_prestate, conseq);
-
-        let poststate_res =
-            intersect_states(block_poststate(fcx.ccx, conseq),
-                             expr_poststate(fcx.ccx, altern));
-        /*
-           fcx.ccx.tcx.sess.span_note(antec.span,
-           "poststate_res = " + aux::tritv_to_str(fcx, poststate_res));
-        fcx.ccx.tcx.sess.span_note(antec.span,
-           "altern poststate = " +
-            aux::tritv_to_str(fcx, expr_poststate(fcx.ccx, altern)));
-        fcx.ccx.tcx.sess.span_note(antec.span,
-        "conseq poststate = " + aux::tritv_to_str(fcx,
-           block_poststate(fcx.ccx, conseq)));
-        */
-
-        changed |= set_poststate_ann(fcx.ccx, id, poststate_res);
-      }
-    }
-    return changed;
-}
-
-fn find_pre_post_state_cap_clause(fcx: fn_ctxt, e_id: node_id,
-                                  pres: prestate, cap_clause: capture_clause)
-    -> bool
-{
-    let ccx = fcx.ccx;
-    let pres_changed = set_prestate_ann(ccx, e_id, pres);
-    let post = pres.clone();
-    for (*cap_clause).each |cap_item| {
-        if cap_item.is_move {
-            forget_in_poststate(fcx, post, cap_item.id);
-        }
-    }
-    return set_poststate_ann(ccx, e_id, post) || pres_changed;
-}
-
-fn find_pre_post_state_expr(fcx: fn_ctxt, pres: prestate, e: @expr) -> bool {
-    let num_constrs = num_constraints(fcx.enclosing);
-
-    match e.node {
-      expr_new(p, _, v) {
-        return find_pre_post_state_two(fcx, pres, p, v, e.id, oper_pure);
-      }
-      expr_vstore(ee, _) {
-        let mut changed = find_pre_post_state_expr(fcx, pres, ee);
-        set_prestate_ann(fcx.ccx, e.id, expr_prestate(fcx.ccx, ee));
-        set_poststate_ann(fcx.ccx, e.id, expr_poststate(fcx.ccx, ee));
-        return changed;
-      }
-      expr_vec(elts, _) {
-        return find_pre_post_state_exprs(fcx, pres, e.id,
-                                      vec::from_elem(vec::len(elts),
-                                                    init_assign), elts,
-                                      return_val);
-      }
-      expr_call(operator, operands, _) {
-        debug!("hey it's a call: %s", expr_to_str(e));
-        return find_pre_post_state_call(fcx, pres, operator, e.id,
-                                     callee_arg_init_ops(fcx, operator.id),
-                                     operands,
-                                     controlflow_expr(fcx.ccx, operator));
-      }
-      expr_path(_) { return pure_exp(fcx.ccx, e.id, pres); }
-      expr_log(_, lvl, ex) {
-        return find_pre_post_state_two(fcx, pres, lvl, ex, e.id, oper_pure);
-      }
-      expr_mac(_) { fcx.ccx.tcx.sess.bug(~"unexpanded macro"); }
-      expr_lit(l) { return pure_exp(fcx.ccx, e.id, pres); }
-      expr_fn(_, _, _, cap_clause) {
-        return find_pre_post_state_cap_clause(fcx, e.id, pres, cap_clause);
-      }
-      expr_fn_block(_, _, cap_clause) {
-        return find_pre_post_state_cap_clause(fcx, e.id, pres, cap_clause);
-      }
-      expr_block(b) {
-        return find_pre_post_state_block(fcx, pres, b) |
-                set_prestate_ann(fcx.ccx, e.id, pres) |
-                set_poststate_ann(fcx.ccx, e.id, block_poststate(fcx.ccx, b));
-      }
-      expr_rec(fields, maybe_base) {
-        let exs = field_exprs(fields);
-        let mut changed =
-            find_pre_post_state_exprs(fcx, pres, e.id,
-                                      vec::from_elem(vec::len(fields),
-                                                    init_assign),
-                                      exs, return_val);
-
-        let base_pres = match vec::last_opt(exs) { none { pres }
-                          Some(f) { expr_poststate(fcx.ccx, f) }};
-        option::iter(maybe_base, |base| {
-            changed |= find_pre_post_state_expr(fcx, base_pres, base) |
-                set_poststate_ann(fcx.ccx, e.id,
-                                  expr_poststate(fcx.ccx, base))
-        });
-        return changed;
-      }
-      expr_tup(elts) {
-        return find_pre_post_state_exprs(fcx, pres, e.id,
-                                      vec::from_elem(vec::len(elts),
-                                                    init_assign), elts,
-                                      return_val);
-      }
-      expr_move(lhs, rhs) {
-        return find_pre_post_state_two(fcx, pres, lhs, rhs, e.id, oper_move);
-      }
-      expr_assign(lhs, rhs) {
-        return find_pre_post_state_two(
-            fcx, pres, lhs, rhs, e.id, oper_assign);
-      }
-      expr_swap(lhs, rhs) {
-        return find_pre_post_state_two(fcx, pres, lhs, rhs, e.id, oper_swap);
-        // Could be more precise and actually swap the role of
-        // lhs and rhs in constraints
-      }
-      expr_ret(maybe_ret_val) {
-        let mut changed = set_prestate_ann(fcx.ccx, e.id, pres);
-        /* everything is true if execution continues after
-           a return expression (since execution never continues locally
-           after a return expression */
-        let post = false_postcond(num_constrs);
-
-        set_poststate_ann(fcx.ccx, e.id, post);
-
-        match maybe_ret_val {
-          none {/* do nothing */ }
-          Some(ret_val) {
-            changed |= find_pre_post_state_expr(fcx, pres, ret_val);
-          }
-        }
-        return changed;
-      }
-      expr_if(antec, conseq, maybe_alt) {
-        return join_then_else(fcx, antec, conseq, maybe_alt, e.id, plain_if,
-                           pres);
-      }
-      expr_binary(bop, l, r) {
-        if lazy_binop(bop) {
-            let mut changed = find_pre_post_state_expr(fcx, pres, l);
-            changed |=
-                find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, l), r);
-            return changed | set_prestate_ann(fcx.ccx, e.id, pres) |
-                    set_poststate_ann(fcx.ccx, e.id,
-                                      expr_poststate(fcx.ccx, l));
-        } else {
-            return find_pre_post_state_two(fcx, pres, l, r, e.id, oper_pure);
-        }
-      }
-      expr_assign_op(op, lhs, rhs) {
-        return find_pre_post_state_two(fcx, pres, lhs, rhs, e.id,
-                                    oper_assign_op);
-      }
-      expr_while(test, body) {
-        let loop_pres =
-            intersect_states(block_poststate(fcx.ccx, body), pres);
-
-        let mut changed =
-            set_prestate_ann(fcx.ccx, e.id, loop_pres) |
-                find_pre_post_state_expr(fcx, loop_pres, test) |
-                find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, test),
-                                          body);
-
-        /* conservative approximation: if a loop contains a break
-           or cont, we assume nothing about the poststate */
-        /* which is still unsound -- see ~[Break-unsound] */
-        if has_nonlocal_exits(body) {
-            return changed | set_poststate_ann(fcx.ccx, e.id, pres);
-        } else {
-            let e_post = expr_poststate(fcx.ccx, test);
-            let b_post = block_poststate(fcx.ccx, body);
-            return changed |
-                    set_poststate_ann(fcx.ccx, e.id,
-                                      intersect_states(e_post, b_post));
-        }
-      }
-      expr_loop(body) {
-        let loop_pres =
-            intersect_states(block_poststate(fcx.ccx, body), pres);
-        let mut changed = set_prestate_ann(fcx.ccx, e.id, loop_pres)
-              | find_pre_post_state_block(fcx, loop_pres, body);
-        /* conservative approximation: if a loop contains a break
-           or cont, we assume nothing about the poststate (so, we
-           set all predicates to "don't know" */
-        /* which is still unsound -- see ~[Break-unsound] */
-        if may_break(body) {
-                /* Only do this if there are *breaks* not conts.
-                 An infinite loop with conts is still an infinite loop.
-                We assume all preds are FALSE, not '?' -- because in the
-                worst case, the body could invalidate all preds and
-                deinitialize everything before breaking */
-            let post = empty_poststate(num_constrs);
-            post.kill();
-            return changed | set_poststate_ann(fcx.ccx, e.id, post);
-        } else {
-            return changed | set_poststate_ann(fcx.ccx, e.id,
-                                            false_postcond(num_constrs));
-        }
-      }
-      expr_index(val, sub) {
-        return find_pre_post_state_two(fcx, pres, val, sub, e.id, oper_pure);
-      }
-      expr_match(val, alts, _) {
-        let mut changed =
-            set_prestate_ann(fcx.ccx, e.id, pres) |
-                find_pre_post_state_expr(fcx, pres, val);
-        let e_post = expr_poststate(fcx.ccx, val);
-        let mut a_post;
-        if vec::len(alts) > 0u {
-            a_post = false_postcond(num_constrs);
-            for alts.each |an_alt| {
-                match an_alt.guard {
-                  Some(e) {
-                    changed |= find_pre_post_state_expr(fcx, e_post, e);
-                  }
-                  _ {}
-                }
-                changed |=
-                    find_pre_post_state_block(fcx, e_post, an_alt.body);
-                intersect(a_post, block_poststate(fcx.ccx, an_alt.body));
-                // We deliberately do *not* update changed here, because
-                // we'd go into an infinite loop that way, and the change
-                // gets made after the if expression.
-
-            }
-        } else {
-            // No alts; poststate is the poststate of the test
-
-            a_post = e_post;
-        }
-        return changed | set_poststate_ann(fcx.ccx, e.id, a_post);
-      }
-      expr_field(x, _, _) | expr_loop_body(x) | expr_do_body(x) |
-      expr_unary(_, x) |
-      expr_addr_of(_, x) | expr_assert(x) | expr_cast(x, _) |
-      expr_copy(x) {
-        return find_pre_post_state_sub(fcx, pres, x, e.id, None);
-      }
-      expr_fail(maybe_fail_val) {
-        /* if execution continues after fail, then everything is true!
-        woo! */
-        let post = false_postcond(num_constrs);
-        return set_prestate_ann(fcx.ccx, e.id, pres) |
-                set_poststate_ann(fcx.ccx, e.id, post) |
-                option::map_default(
-                    maybe_fail_val, false,
-                    |fail_val|
-                    find_pre_post_state_expr(fcx, pres, fail_val) );
-      }
-      expr_check(_, p) {
-        /* predicate p holds after this expression executes */
-        let c: sp_constr = expr_to_constr(fcx.ccx.tcx, p);
-        return find_pre_post_state_sub(fcx, pres, p, e.id, Some(c.node));
-      }
-      expr_if_check(p, conseq, maybe_alt) {
-        return join_then_else(
-            fcx, p, conseq, maybe_alt, e.id, if_check, pres);
-      }
-      expr_break { return pure_exp(fcx.ccx, e.id, pres); }
-      expr_again { return pure_exp(fcx.ccx, e.id, pres); }
-    }
-}
-
-fn find_pre_post_state_stmt(fcx: fn_ctxt, pres: prestate, s: @stmt) -> bool {
-    let stmt_ann = stmt_to_ann(fcx.ccx, *s);
-
-    debug!("[ %s ]", *fcx.name);
-    debug!("*At beginning: stmt = %s", stmt_to_str(*s));
-    debug!("*prestate = %s", stmt_ann.states.prestate.to_str());
-    debug!("*poststate = %s", stmt_ann.states.prestate.to_str());
-
-    match s.node {
-      stmt_decl(adecl, id) {
-        match adecl.node {
-          decl_local(alocals) {
-            set_prestate(stmt_ann, pres);
-            let c_and_p = seq_states(fcx, pres,
-                  locals_to_bindings(fcx.ccx.tcx, alocals));
-            /* important to do this in one step to ensure
-            termination (don't want to set changed to true
-            for intermediate changes) */
-
-            let mut changed =
-                set_poststate(stmt_ann, c_and_p.post) | c_and_p.changed;
-
-            debug!("Summary: stmt = %s", stmt_to_str(*s));
-            debug!("prestate = %s", stmt_ann.states.prestate.to_str());
-            debug!("poststate = %s", stmt_ann.states.poststate.to_str());
-            debug!("changed = %s", bool::to_str(changed));
-
-            return changed;
-          }
-          decl_item(an_item) {
-            return set_prestate(stmt_ann, pres)
-                | set_poststate(stmt_ann, pres);
-            /* the outer visitor will recurse into the item */
-          }
-        }
-      }
-      stmt_expr(ex, _) | stmt_semi(ex, _) {
-        let mut changed =
-            find_pre_post_state_expr(fcx, pres, ex) |
-                set_prestate(stmt_ann, expr_prestate(fcx.ccx, ex)) |
-                set_poststate(stmt_ann, expr_poststate(fcx.ccx, ex));
-
-
-        debug!("Finally: %s", stmt_to_str(*s));
-        debug!("prestate = %s", stmt_ann.states.prestate.to_str());
-        debug!("poststate = %s", stmt_ann.states.poststate.to_str());
-        debug!("changed = %s", bool::to_str(changed));
-
-        return changed;
-      }
-    }
-}
-
-
-/* Updates the pre- and post-states of statements in the block,
-   returns a boolean flag saying whether any pre- or poststates changed */
-fn find_pre_post_state_block(fcx: fn_ctxt, pres0: prestate, b: blk) -> bool {
-    /* First, set the pre-states and post-states for every expression */
-
-    let mut pres = pres0;
-    /* Iterate over each stmt. The new prestate is <pres>. The poststate
-     consist of improving <pres> with whatever variables this stmt
-     initializes.  Then <pres> becomes the new poststate. */
-
-    let mut changed = false;
-    for b.node.stmts.each |s| {
-        changed |= find_pre_post_state_stmt(fcx, pres, s);
-        pres = stmt_poststate(fcx.ccx, *s);
-    }
-    let mut post = pres;
-    match b.node.expr {
-      none { }
-      Some(e) {
-        changed |= find_pre_post_state_expr(fcx, pres, e);
-        post = expr_poststate(fcx.ccx, e);
-      }
-    }
-
-    set_prestate_ann(fcx.ccx, b.node.id, pres0);
-    set_poststate_ann(fcx.ccx, b.node.id, post);
-
-    return changed;
-}
-
-fn find_pre_post_state_fn(fcx: fn_ctxt,
-                          f_decl: fn_decl,
-                          f_body: blk) -> bool {
-    // All constraints are considered false until proven otherwise.
-    // This ensures that intersect works correctly.
-    kill_all_prestate(fcx, f_body.node.id);
-
-    // Instantiate any constraints on the arguments so we can use them
-    let block_pre = block_prestate(fcx.ccx, f_body);
-    for f_decl.constraints.each |c| {
-        let tsc = ast_constr_to_ts_constr(fcx.ccx.tcx, f_decl.inputs, c);
-        set_in_prestate_constr(fcx, tsc, block_pre);
-    }
-
-    let mut changed = find_pre_post_state_block(fcx, block_pre, f_body);
-
-    /*
-        error!("find_pre_post_state_fn");
-        log(error, changed);
-        fcx.ccx.tcx.sess.span_note(f_body.span, fcx.name);
-    */
-
-    return changed;
-}
-//
-// Local Variables:
-// mode: rust
-// fill-column: 78;
-// indent-tabs-mode: nil
-// c-basic-offset: 4
-// buffer-file-coding-system: utf-8-unix
-// End:
-//