diff --git a/src/boot/me/trans.ml b/src/boot/me/trans.ml
index 1b3ad5d45440f..d34d19d8dc63d 100644
--- a/src/boot/me/trans.ml
+++ b/src/boot/me/trans.ml
@@ -4793,18 +4793,28 @@ let trans_visitor
     let trans_arm arm : quad_idx =
       let (pat, block) = arm.node in
 
-      (* Translates the pattern and returns the addresses of the branch
-       * instructions that are taken if the match fails.
+      (* Translates the pattern and returns a pair where the first
+          component is a list of the addresses of the branch
+          instructions that are taken if the match fails,
+          and the second component is a thunk that, when invoked,
+          emits initialization code for the variables bound in this pattern.
+
+          trans_pat can't just emit the initialization code itself, because
+          then, pattern-bound variables could be taken without ever being 
+          dropped if a nested pattern fails partway through (because the 
+          drop code is part of the action for the pattern).
        *)
       let rec trans_pat
           (pat:Ast.pat)
           (src_cell:Il.cell)
           (src_ty:Ast.ty)
-          : quad_idx list =
+          : (quad_idx list *
+             (unit -> unit)) =
 
         match pat with
             Ast.PAT_lit lit ->
-              trans_compare_simple Il.JNE (trans_lit lit) (Il.Cell src_cell)
+              (trans_compare_simple Il.JNE (trans_lit lit) (Il.Cell src_cell),
+               fun _ -> ())
 
           | Ast.PAT_tag (lval, pats) ->
               let tag_ident =
@@ -4815,7 +4825,7 @@ let trans_visitor
                   | Ast.LVAL_base { node = Ast.BASE_app (id, _); id = _ } ->
                       id
                   | _ -> bug cx "expected lval ending in ident"
-              in
+              in 
               let ttag =
                 match strip_mutable_or_constrained_ty src_ty with
                     Ast.TY_tag ttag -> ttag
@@ -4843,7 +4853,8 @@ let trans_visitor
 
               let tup_cell:Il.cell = get_variant_ptr union_cell i in
 
-              let trans_elem_pat i elem_pat : quad_idx list =
+              let trans_elem_pat i elem_pat :
+                    (quad_idx list * (unit -> unit)) =
                 let elem_cell =
                   get_element_ptr_dyn_in_current_frame tup_cell i
                 in
@@ -4852,24 +4863,31 @@ let trans_visitor
               in
 
               let elem_jumps =
-                List.concat (Array.to_list (Array.mapi trans_elem_pat pats))
+                (Array.to_list (Array.mapi trans_elem_pat pats)) in
+              let (elem_jump_addrs, ks) = List.split elem_jumps
               in
-                next_jumps @ elem_jumps
+                (next_jumps @ (List.concat elem_jump_addrs),
+                 (* Compose all the var-initialization thunks together
+                    to make one thunk that initializes all the vars *)
+                 List.fold_left (fun g f -> (fun x -> f (g x)))
+                   (fun _ -> ()) ks)
 
           | Ast.PAT_slot (dst, _) ->
               let dst_slot = get_slot cx dst.id in
               let dst_cell = cell_of_block_slot dst.id in
-                trans_init_slot_from_cell
-                  (get_ty_params_of_current_frame())
-                  CLONE_none dst_cell dst_slot
-                  src_cell src_ty;
-                []                 (* irrefutable *)
-
-          | Ast.PAT_wild -> []     (* irrefutable *)
+              (* irrefutable *)
+                ([], (fun () -> (* init the slot later, inside the block,
+                                   once we know we had a match *)
+                                  trans_init_slot_from_cell 
+                                  (get_ty_params_of_current_frame())
+                                  CLONE_none dst_cell dst_slot
+                                  src_cell src_ty))
+          | Ast.PAT_wild -> ([], fun _ -> ())     (* irrefutable *)
       in
 
       let (lval_cell, lval_ty) = trans_lval at.Ast.alt_tag_lval in
-      let next_jumps = trans_pat pat lval_cell lval_ty in
+      let (next_jumps, prologue) = trans_pat pat lval_cell lval_ty in
+        prologue (); (* binds any pattern-bound variables *)
         trans_block block;
         let last_jump = mark() in
           emit (Il.jmp Il.JMP Il.CodeNone);
diff --git a/src/comp/driver/rustc.rs b/src/comp/driver/rustc.rs
index c321b3a09738a..99c736025db8e 100644
--- a/src/comp/driver/rustc.rs
+++ b/src/comp/driver/rustc.rs
@@ -80,12 +80,11 @@ fn compile_input(session.session sess,
     crate = resolve.resolve_crate(sess, crate);
     capture.check_for_captures(sess, crate);
 
-    auto ty_cx = ty.mk_ctxt();
-    auto typeck_result = typeck.check_crate(sess, ty_cx, crate);
+    auto ty_cx = ty.mk_ctxt(sess);
+    auto typeck_result = typeck.check_crate(ty_cx, crate);
     crate = typeck_result._0;
     auto type_cache = typeck_result._1;
-    // FIXME: uncomment once typestate_check works
-    // crate = typestate_check.check_crate(crate);
+    crate = typestate_check.check_crate(crate);
     trans.trans_crate(sess, crate, ty_cx, type_cache, output, shared,
                       optimize, verify, save_temps, ot);
 }
diff --git a/src/comp/middle/trans.rs b/src/comp/middle/trans.rs
index 3e316ab4a244f..776ef53531cd4 100644
--- a/src/comp/middle/trans.rs
+++ b/src/comp/middle/trans.rs
@@ -3772,6 +3772,8 @@ fn trans_pat_match(@block_ctxt cx, @ast.pat pat, ValueRef llval,
                     auto subpat_res = trans_pat_match(matched_cx, subpat,
                                                       llsubval, next_cx);
                     matched_cx = subpat_res.bcx;
+
+                    i += 1;
                 }
             }
 
diff --git a/src/comp/middle/ty.rs b/src/comp/middle/ty.rs
index f5cea365d9232..47442f2b8035f 100644
--- a/src/comp/middle/ty.rs
+++ b/src/comp/middle/ty.rs
@@ -46,7 +46,7 @@ type mt = rec(t ty, ast.mutability mut);
 
 // Contains information needed to resolve types and (in the future) look up
 // the types of AST nodes.
-type ctxt = rec(@type_store ts);
+type ctxt = rec(@type_store ts, session.session sess);
 type ty_ctxt = ctxt;    // Needed for disambiguation from Unify.ctxt.
 
 // Convert from method type to function type.  Pretty easy; we just drop
@@ -200,7 +200,7 @@ fn mk_type_store() -> @type_store {
              others=map.mk_hashmap[t,t](hasher, eqer));
 }
 
-fn mk_ctxt() -> ctxt { ret rec(ts=mk_type_store()); }
+fn mk_ctxt(session.session s) -> ctxt { ret rec(ts=mk_type_store(), sess=s); }
 
 // Type constructors
 
diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs
index ce22999969562..3354fe46ad963 100644
--- a/src/comp/middle/typeck.rs
+++ b/src/comp/middle/typeck.rs
@@ -106,7 +106,7 @@ fn substitute_ty_params(&@crate_ctxt ccx,
 
 
 // Returns the type parameter count and the type for the given definition.
-fn ty_param_count_and_ty_for_def(@fn_ctxt fcx, &ast.def defn)
+fn ty_param_count_and_ty_for_def(@fn_ctxt fcx, &ast.span sp, &ast.def defn)
         -> ty_param_count_and_ty {
     alt (defn) {
         case (ast.def_arg(?id)) {
@@ -157,7 +157,7 @@ fn ty_param_count_and_ty_for_def(@fn_ctxt fcx, &ast.def defn)
         }
 
         case (ast.def_ty(_)) {
-            fcx.ccx.sess.err("expected value but found type");
+            fcx.ccx.sess.span_err(sp, "expected value but found type");
             fail;
         }
 
@@ -308,7 +308,10 @@ fn ast_ty_to_ty(ty.ctxt tcx, ty_getter getter, &@ast.ty ast_ty) -> ty.t {
                     typ = instantiate(tcx, getter, id, path.node.types);
                 }
                 case (ast.def_ty_arg(?id)) { typ = ty.mk_param(tcx, id); }
-                case (_)                   { fail; }
+                case (_)                   { 
+                    tcx.sess.span_err(ast_ty.span,
+                       "found type name used as a variable");
+                    fail; }
             }
 
             cname = some(path_to_str(path));
@@ -1839,7 +1842,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
             check (defopt != none[ast.def]);
             auto defn = option.get[ast.def](defopt);
 
-            auto tpt = ty_param_count_and_ty_for_def(fcx, defn);
+            auto tpt = ty_param_count_and_ty_for_def(fcx, expr.span, defn);
 
             if (ty.def_has_ty_params(defn)) {
                 auto ann = instantiate_path(fcx, pth, tpt, expr.span);
@@ -2623,22 +2626,27 @@ fn check_stmt(&@fn_ctxt fcx, &@ast.stmt stmt) -> @ast.stmt {
                 case (ast.decl_local(_)) {
                     auto decl_1 = check_decl_local(fcx, decl);
                     ret @fold.respan[ast.stmt_](stmt.span,
-                                                ast.stmt_decl(decl_1, a));
+                           ast.stmt_decl(decl_1,
+                             plain_ann(fcx.ccx.tcx)));
                 }
 
                 case (ast.decl_item(_)) {
                     // Ignore for now. We'll return later.
+                    ret @fold.respan[ast.stmt_](stmt.span,
+                           ast.stmt_decl(decl,
+                             plain_ann(fcx.ccx.tcx)));
                 }
             }
 
-            ret stmt;
+            //         ret stmt;
         }
 
         case (ast.stmt_expr(?expr,?a)) {
             auto expr_t = check_expr(fcx, expr);
             expr_t = Pushdown.pushdown_expr(fcx, expr_ty(fcx.ccx.tcx, expr_t),
                                             expr_t);
-            ret @fold.respan[ast.stmt_](stmt.span, ast.stmt_expr(expr_t, a));
+            ret @fold.respan[ast.stmt_](stmt.span,
+                   ast.stmt_expr(expr_t, plain_ann(fcx.ccx.tcx)));
         }
     }
 
@@ -2787,8 +2795,9 @@ fn eq_unify_cache_entry(&unify_cache_entry a, &unify_cache_entry b) -> bool {
 
 type typecheck_result = tup(@ast.crate, ty.type_cache);
 
-fn check_crate(session.session sess, ty.ctxt tcx, @ast.crate crate)
+fn check_crate(ty.ctxt tcx, @ast.crate crate)
         -> typecheck_result {
+    auto sess = tcx.sess;
     auto result = Collect.collect_item_types(sess, tcx, crate);
 
     let vec[ast.obj_field] fields = vec();
diff --git a/src/comp/middle/typestate_check.rs b/src/comp/middle/typestate_check.rs
index 8a6e840a4284e..d08ae82d603d7 100644
--- a/src/comp/middle/typestate_check.rs
+++ b/src/comp/middle/typestate_check.rs
@@ -101,14 +101,22 @@ import util.common.uistr;
 import util.common.elt_exprs;
 import util.common.field_exprs;
 import util.common.log_expr;
+import util.common.log_expr_err;
 import util.common.log_stmt;
 import util.common.log_block;
+import util.common.log_stmt_err;
+import util.common.log_fn_err;
+import util.common.log_fn;
+import util.common.log_block_err;
+import util.common.has_nonlocal_exits;
+import util.common.decl_lhs;
 import util.typestate_ann;
 import util.typestate_ann.ts_ann;
 import util.typestate_ann.empty_pre_post;
 import util.typestate_ann.empty_poststate;
 import util.typestate_ann.true_precond;
 import util.typestate_ann.true_postcond;
+import util.typestate_ann.false_postcond;
 import util.typestate_ann.postcond;
 import util.typestate_ann.precond;
 import util.typestate_ann.poststate;
@@ -131,8 +139,10 @@ import util.typestate_ann.empty_prestate;
 import util.typestate_ann.empty_ann;
 import util.typestate_ann.extend_prestate;
 import util.typestate_ann.extend_poststate;
+import util.typestate_ann.relax_prestate;
 import util.typestate_ann.intersect;
 import util.typestate_ann.pp_clone;
+import util.typestate_ann.clone;
 
 import middle.ty;
 import middle.ty.ann_to_type;
@@ -156,6 +166,7 @@ import std._vec.push;
 import std._vec.slice;
 import std._vec.unzip;
 import std._vec.plus_option;
+import std._vec.cat_options;
 import std.option;
 import std.option.t;
 import std.option.some;
@@ -184,7 +195,7 @@ import util.typestate_ann.require_and_preserve;
 
 /**** debugging junk  ****/
 
-fn log_bitv(fn_info enclosing, bitv.t v) {
+fn bitv_to_str(fn_info enclosing, bitv.t v) -> str {
   auto s = "";
 
   for each (@tup(def_id, tup(uint, ident)) p in enclosing.items()) {
@@ -192,11 +203,18 @@ fn log_bitv(fn_info enclosing, bitv.t v) {
       s += " " + p._1._1 + " ";
     }
   }
+  ret s;
+}
 
-  log(s);
+fn log_bitv(fn_info enclosing, bitv.t v) {
+    log(bitv_to_str(enclosing, v));
 }
 
-fn log_cond(vec[uint] v) -> () {
+fn log_bitv_err(fn_info enclosing, bitv.t v) {
+    log_err(bitv_to_str(enclosing, v));
+}
+
+fn tos (vec[uint] v) -> str {
   auto res = "";
   for (uint i in v) {
     if (i == 0u) {
@@ -206,8 +224,16 @@ fn log_cond(vec[uint] v) -> () {
       res += "1";
     }
   }
-  log(res);
+  ret res;
 }
+
+fn log_cond(vec[uint] v) -> () {
+    log(tos(v));
+}
+fn log_cond_err(vec[uint] v) -> () {
+    log_err(tos(v));
+}
+
 fn log_pp(&pre_and_post pp) -> () {
   auto p1 = bitv.to_vec(pp.precondition);
   auto p2 = bitv.to_vec(pp.postcondition);
@@ -217,6 +243,33 @@ fn log_pp(&pre_and_post pp) -> () {
   log_cond(p2);
 }
 
+fn log_pp_err(&pre_and_post pp) -> () {
+  auto p1 = bitv.to_vec(pp.precondition);
+  auto p2 = bitv.to_vec(pp.postcondition);
+  log_err("pre:");
+  log_cond_err(p1);
+  log_err("post:");
+  log_cond_err(p2);
+}
+
+fn log_states(&pre_and_post_state pp) -> () {
+  auto p1 = bitv.to_vec(pp.prestate);
+  auto p2 = bitv.to_vec(pp.poststate);
+  log("prestate:");
+  log_cond(p1);
+  log("poststate:");
+  log_cond(p2);
+}
+
+fn log_states_err(&pre_and_post_state pp) -> () {
+  auto p1 = bitv.to_vec(pp.prestate);
+  auto p2 = bitv.to_vec(pp.poststate);
+  log_err("prestate:");
+  log_cond_err(p1);
+  log_err("poststate:");
+  log_cond_err(p2);
+}
+
 fn print_ident(&ident i) -> () {
   log(" " + i + " ");
 }
@@ -256,18 +309,19 @@ fn num_locals(fn_info m) -> uint {
   ret m.size();
 }
 
-fn find_locals(_fn f) -> vec[tup(ident,def_id)] {
-  auto res = _vec.alloc[tup(ident,def_id)](0u);
+fn collect_local(&@vec[tup(ident, def_id)] vars, &span sp, @ast.local loc) 
+    -> @decl {
+    log("collect_local: pushing " + loc.ident);
+    _vec.push[tup(ident, def_id)](*vars, tup(loc.ident, loc.id));
+    ret @respan(sp, decl_local(loc));
+}
 
-  for each (@tup(ident, block_index_entry) p
-          in f.body.node.index.items()) {
-    alt (p._1) {
-      case (ast.bie_local(?loc)) {
-        res += vec(tup(loc.ident,loc.id));
-      }
-      case (_) { }
-    }
-  }
+fn find_locals(_fn f) -> @vec[tup(ident,def_id)] {
+  auto res = @_vec.alloc[tup(ident,def_id)](0u);
+
+  auto fld = fold.new_identity_fold[@vec[tup(ident, def_id)]]();
+  fld = @rec(fold_decl_local = bind collect_local(_,_,_) with *fld);
+  auto ignore = fold.fold_fn[@vec[tup(ident, def_id)]](res, fld, f);
 
   ret res;
 }
@@ -285,12 +339,12 @@ fn mk_fn_info(_fn f) -> fn_info {
   let uint next = 0u;
   let vec[ast.arg] f_args = f.decl.inputs;
 
-  for (ast.arg v in f_args) {
-    next = add_var(v.id, v.ident, next, res);
-  }
+  /* ignore args, which we know are initialized;
+     just collect locally declared vars */
 
-  let vec[tup(ident,def_id)] locals = find_locals(f);
-  for (tup(ident,def_id) p in locals) {
+  let @vec[tup(ident,def_id)] locals = find_locals(f);
+  log(uistr(_vec.len[tup(ident, def_id)](*locals)) + " locals");
+  for (tup(ident,def_id) p in *locals) {
     next = add_var(p._1, p._0, next, res);
   }
 
@@ -313,8 +367,6 @@ fn mk_fn_info_item_obj(&fn_info_map fi, &span sp, ident i, &ast._obj o,
     auto all_methods = _vec.clone[@method](o.methods);
     plus_option[@method](all_methods, o.dtor);
     for (@method m in all_methods) {
-        /* FIXME: also need to pass in fields so we can say
-           they're initialized? */
         fi.insert(m.node.id, mk_fn_info(m.node.meth));
         log(m.node.ident + " has " +
             uistr(num_locals(mk_fn_info(m.node.meth))) + " local vars");
@@ -435,6 +487,15 @@ fn expr_ann(&expr e) -> ann {
     case (ast.expr_chan(_,?a)) {
       ret a;
     }
+    case (expr_break(?a)) {
+        ret a;
+    }
+    case (expr_cont(?a)) {
+        ret a;
+    }
+    case (expr_self_method(_, ?a)) {
+        ret a;
+    }
   }
 }
 
@@ -670,17 +731,28 @@ fn with_pp(ann a, pre_and_post p) -> ann {
 // return the precondition for evaluating each expr in order.
 // So, if e0's post is {x} and e1's pre is {x, y, z}, the entire
 // precondition shouldn't include x.
-fn seq_preconds(uint num_vars, vec[pre_and_post] pps) -> precond {
+fn seq_preconds(fn_info enclosing, vec[pre_and_post] pps) -> precond {
   let uint sz = len[pre_and_post](pps);
- 
+  let uint num_vars = num_locals(enclosing);
+
   if (sz >= 1u) {
     auto first   = pps.(0);
     check (pps_len(first) == num_vars);
-    let precond rest = seq_preconds(num_vars,
+    let precond rest = seq_preconds(enclosing,
                          slice[pre_and_post](pps, 1u, sz));
     difference(rest, first.postcondition);
-    union(first.precondition, rest);
-    ret first.precondition;
+    auto res = clone(first.precondition);
+    union(res, rest);
+
+    log("seq_preconds:");
+    log("first.postcondition =");
+    log_bitv(enclosing, first.postcondition);
+    log("rest =");
+    log_bitv(enclosing, rest);
+    log("returning");
+    log_bitv(enclosing, res);
+
+    ret res;
   }
   else {
       ret true_precond(num_vars);
@@ -701,10 +773,13 @@ fn union_postconds_go(&postcond first, &vec[postcond] rest) -> postcond {
   ret first;
 }
 
-fn union_postconds(&vec[postcond] pcs) -> postcond {
-  check (len[postcond](pcs) > 0u);
-
-  ret union_postconds_go(bitv.clone(pcs.(0)), pcs);
+fn union_postconds(uint nv, &vec[postcond] pcs) -> postcond {
+  if (len[postcond](pcs) > 0u) {
+      ret union_postconds_go(bitv.clone(pcs.(0)), pcs);
+  }
+  else {
+      ret empty_prestate(nv);
+  }
 }
 
 /* Gee, maybe we could use foldl or something */
@@ -804,6 +879,8 @@ fn find_pre_post_item(fn_info_map fm, fn_info enclosing, &item i) -> () {
    be the union of all postconditions for <args> */
 fn find_pre_post_exprs(&fn_info_map fm, &fn_info enclosing,
                        &vec[@expr] args, ann a) {
+    auto nv = num_locals(enclosing);
+
     fn do_one(fn_info_map fm, fn_info enclosing,
               &@expr e) -> () {
         find_pre_post_expr(fm, enclosing, *e);
@@ -820,9 +897,22 @@ fn find_pre_post_exprs(&fn_info_map fm, &fn_info enclosing,
     auto h = get_post;
 
     set_pre_and_post(a,
-       rec(precondition=seq_preconds(num_locals(enclosing), pps),
+       rec(precondition=seq_preconds(enclosing, pps),
            postcondition=union_postconds
-           (_vec.map[pre_and_post, postcond](h, pps))));
+           (nv, (_vec.map[pre_and_post, postcond](h, pps)))));
+}
+
+fn find_pre_post_loop(&fn_info_map fm, &fn_info enclosing, &@decl d,
+     &@expr index, &block body, &ann a) -> () {
+    find_pre_post_expr(fm, enclosing, *index);
+    find_pre_post_block(fm, enclosing, body);
+    auto loop_precond = declare_var(enclosing, decl_lhs(d),
+           seq_preconds(enclosing, vec(expr_pp(*index),
+                                                   block_pp(body))));
+    auto loop_postcond = intersect_postconds
+        (vec(expr_postcond(*index), block_postcond(body)));
+    set_pre_and_post(a, rec(precondition=loop_precond,
+                            postcondition=loop_postcond));
 }
 
 /* Fills in annotations as a side effect. Does not rebuild the expr */
@@ -833,21 +923,31 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () {
         find_pre_post_expr(fm, enclosing, *e);
     }
     fn pp_one(&@expr e) -> pre_and_post {
-        be expr_pp(*e);
+        ret expr_pp(*e);
     }
-
-    /*    log("find_pre_post_expr (num_locals =" +
+    
+        log("find_pre_post_expr (num_locals =" +
              uistr(num_local_vars) + "):");
-          log_expr(e);
-    */
-
-    alt(e.node) {
-        case(expr_call(?operator, ?operands, ?a)) {
+        log_expr(e);
+    
+    alt (e.node) {
+        case (expr_call(?operator, ?operands, ?a)) {
             auto args = _vec.clone[@expr](operands);
             _vec.push[@expr](args, operator);
             find_pre_post_exprs(fm, enclosing, args, a);
         }
-        case(expr_path(?p, ?maybe_def, ?a)) {
+        case (expr_spawn(_, _, ?operator, ?operands, ?a)) {
+            auto args = _vec.clone[@expr](operands);
+            _vec.push[@expr](args, operator);
+            find_pre_post_exprs(fm, enclosing, args, a);
+        }
+        case (expr_vec(?args, _, ?a)) {
+            find_pre_post_exprs(fm, enclosing, args, a);
+        }
+        case (expr_tup(?elts, ?a)) {
+            find_pre_post_exprs(fm, enclosing, elt_exprs(elts), a);
+        }
+        case (expr_path(?p, ?maybe_def, ?a)) {
             auto df;
             alt (maybe_def) {
                 case (none[def])
@@ -868,10 +968,30 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () {
             // Otherwise, variable is global, so it must be initialized
             set_pre_and_post(a, res);
         }
+        case (expr_self_method(?v, ?a)) {
+            /* v is a method of the enclosing obj, so it must be
+               initialized, right? */
+            set_pre_and_post(a, empty_pre_post(num_local_vars));
+        }
         case(expr_log(_, ?arg, ?a)) {
             find_pre_post_expr(fm, enclosing, *arg);
             set_pre_and_post(a, expr_pp(*arg));
         }
+        case (expr_chan(?arg, ?a)) {
+            find_pre_post_expr(fm, enclosing, *arg);
+            set_pre_and_post(a, expr_pp(*arg));
+        }
+        case(expr_put(?opt, ?a)) {
+            alt (opt) {
+                case (some[@expr](?arg)) {
+                    find_pre_post_expr(fm, enclosing, *arg);
+                    set_pre_and_post(a, expr_pp(*arg));
+                }
+                case (none[@expr]) {
+                    set_pre_and_post(a, empty_pre_post(num_local_vars));
+                }
+            }
+        }
         case (expr_block(?b, ?a)) {
             find_pre_post_block(fm, enclosing, b);
             set_pre_and_post(a, block_pp(b));
@@ -886,6 +1006,8 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () {
                 case (expr_path(?p, some[def](def_local(?d_id)), ?a_lhs)) {
                     find_pre_post_expr(fm, enclosing, *rhs);
                     set_pre_and_post(a, expr_pp(*rhs));
+                    log("gen:");
+                    log_expr(e);
                     gen(enclosing, a, d_id);
                 }
                 case (_) {
@@ -895,29 +1017,57 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () {
                 }
             }
         }
+        case (expr_recv(?lhs, ?rhs, ?a)) {
+            alt (lhs.node) {
+                case (expr_path(?p, some[def](def_local(?d_id)), ?a_lhs)) {
+                    find_pre_post_expr(fm, enclosing, *rhs);
+                    set_pre_and_post(a, expr_pp(*rhs));
+                    log("gen:");
+                    log_expr(e);
+                    gen(enclosing, a, d_id);
+                }
+                case (_) {
+                    // doesn't check that lhs is an lval, but
+                    // that's probably ok
+                    find_pre_post_exprs(fm, enclosing, vec(lhs, rhs), a);
+                }
+            }
+        }
+        case (expr_assign_op(_, ?lhs, ?rhs, ?a)) {
+            /* Different from expr_assign in that the lhs *must*
+               already be initialized */
+            find_pre_post_exprs(fm, enclosing, vec(lhs, rhs), a);
+        }
         case (expr_lit(_,?a)) {
             set_pre_and_post(a, empty_pre_post(num_local_vars));
         }
         case (expr_ret(?maybe_val, ?a)) {
             alt (maybe_val) {
                 case (none[@expr]) {
-                    set_pre_and_post(a, empty_pre_post(num_local_vars));
+                    set_pre_and_post(a,
+                      rec(precondition=true_precond(num_local_vars),
+                          postcondition=false_postcond(num_local_vars)));
                 }
                 case (some[@expr](?ret_val)) {
                     find_pre_post_expr(fm, enclosing, *ret_val);
                     let pre_and_post pp =
                         rec(precondition=expr_precond(*ret_val),
-                            postcondition=empty_poststate(num_local_vars));
+                            postcondition=false_postcond(num_local_vars));
                     set_pre_and_post(a, pp);
                 }
             }
         }
+        case (expr_be(?e, ?a)) {
+            find_pre_post_expr(fm, enclosing, *e);
+            set_pre_and_post(a, rec(precondition=expr_prestate(*e),
+                          postcondition=false_postcond(num_local_vars)));
+        }
         case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) {
             find_pre_post_expr(fm, enclosing, *antec);
             find_pre_post_block(fm, enclosing, conseq);
             alt (maybe_alt) {
                 case (none[@expr]) {
-                    auto precond_res = seq_preconds(num_local_vars,
+                    auto precond_res = seq_preconds(enclosing,
                                                     vec(expr_pp(*antec),
                                                         block_pp(conseq)));
                     set_pre_and_post(a, rec(precondition=precond_res,
@@ -927,17 +1077,20 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () {
                 case (some[@expr](?altern)) {
                     find_pre_post_expr(fm, enclosing, *altern);
                     auto precond_true_case =
-                        seq_preconds(num_local_vars,
+                        seq_preconds(enclosing,
                                      vec(expr_pp(*antec), block_pp(conseq)));
                     auto postcond_true_case = union_postconds
-                        (vec(expr_postcond(*antec), block_postcond(conseq)));
-                    auto precond_false_case = seq_preconds
                         (num_local_vars,
+                         vec(expr_postcond(*antec), block_postcond(conseq)));
+                    auto precond_false_case = seq_preconds
+                        (enclosing,
                          vec(expr_pp(*antec), expr_pp(*altern)));
                     auto postcond_false_case = union_postconds
-                        (vec(expr_postcond(*antec), expr_postcond(*altern)));
-                    auto precond_res = union_postconds(vec(precond_true_case,
-                                                       precond_false_case));
+                        (num_local_vars,
+                         vec(expr_postcond(*antec), expr_postcond(*altern)));
+                    auto precond_res = union_postconds
+                        (num_local_vars,
+                         vec(precond_true_case, precond_false_case));
                     auto postcond_res = intersect_postconds
                         (vec(postcond_true_case, postcond_false_case));
                     set_pre_and_post(a, rec(precondition=precond_res,
@@ -950,22 +1103,53 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () {
              FIXME */
             find_pre_post_exprs(fm, enclosing, vec(l, r), a);
         }
+        case (expr_send(?l, ?r, ?a)) {
+            find_pre_post_exprs(fm, enclosing, vec(l, r), a);
+        }
         case (expr_unary(_,?operand,?a)) {
             find_pre_post_expr(fm, enclosing, *operand);
             set_pre_and_post(a, expr_pp(*operand));
         }
+        case (expr_cast(?operand, _, ?a)) {
+            find_pre_post_expr(fm, enclosing, *operand);
+            set_pre_and_post(a, expr_pp(*operand));
+        }
         case (expr_while(?test, ?body, ?a)) {
             find_pre_post_expr(fm, enclosing, *test);
             find_pre_post_block(fm, enclosing, body);
             set_pre_and_post(a,
               rec(precondition=
-                    seq_preconds(num_local_vars,
+                  seq_preconds(enclosing,
                                  vec(expr_pp(*test), 
                                      block_pp(body))),
                   postcondition=
                   intersect_postconds(vec(expr_postcond(*test),
                                           block_postcond(body)))));
         }
+        case (expr_do_while(?body, ?test, ?a)) {
+            find_pre_post_block(fm, enclosing, body);
+            find_pre_post_expr(fm, enclosing, *test);
+   
+            auto loop_postcond = union_postconds(num_local_vars,
+                            vec(block_postcond(body), expr_postcond(*test)));
+            /* conservative approximination: if the body
+               could break or cont, the test may never be executed */
+            if (has_nonlocal_exits(body)) {
+                loop_postcond = empty_poststate(num_local_vars);
+            }
+
+            set_pre_and_post(a, 
+                             rec(precondition=seq_preconds(enclosing,
+                                             vec(block_pp(body),
+                                                 expr_pp(*test))),
+                   postcondition=loop_postcond));
+        }
+        case (expr_for(?d, ?index, ?body, ?a)) {
+            find_pre_post_loop(fm, enclosing, d, index, body, a);
+        }
+        case (expr_for_each(?d, ?index, ?body, ?a)) {
+            find_pre_post_loop(fm, enclosing, d, index, body, a);
+        }
         case (expr_index(?e, ?sub, ?a)) {
             find_pre_post_exprs(fm, enclosing, vec(e, sub), a);
         }
@@ -979,18 +1163,22 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () {
             auto f = bind do_an_alt(fm, enclosing, _);
             auto alt_pps = _vec.map[arm, pre_and_post](f, alts);
             fn combine_pp(pre_and_post antec, 
-                          uint num_local_vars, &pre_and_post pp,
+                          fn_info enclosing, &pre_and_post pp,
                           &pre_and_post next) -> pre_and_post {
-                union(pp.precondition, seq_preconds(num_local_vars,
+                union(pp.precondition, seq_preconds(enclosing,
                                          vec(antec, next)));
                 intersect(pp.postcondition, next.postcondition);
                 ret pp;
             }
-            auto e_pp1 = expr_pp(*e);
-            auto e_pp  = pp_clone(e_pp1);
-            auto g = bind combine_pp(e_pp, num_local_vars, _, _);
-            set_pre_and_post(a, _vec.foldl[pre_and_post, pre_and_post]
-                             (g, e_pp, alt_pps));
+            auto antec_pp = pp_clone(expr_pp(*e)); 
+            auto e_pp  = rec(precondition=empty_prestate(num_local_vars),
+                             postcondition=false_postcond(num_local_vars));
+            auto g = bind combine_pp(antec_pp, enclosing, _, _);
+
+            auto alts_overall_pp = _vec.foldl[pre_and_post, pre_and_post]
+                                    (g, e_pp, alt_pps);
+
+            set_pre_and_post(a, alts_overall_pp);
         }
         case (expr_field(?operator, _, ?a)) {
             find_pre_post_expr(fm, enclosing, *operator);
@@ -998,13 +1186,33 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () {
         }
         case (expr_fail(?a)) {
             set_pre_and_post(a,
+                             /* if execution continues after fail,
+                                then everything is true! */
                rec(precondition=empty_prestate(num_local_vars),
-                   postcondition=true_postcond(num_local_vars)));
+                   postcondition=false_postcond(num_local_vars)));
         }
-        case(_) {
-            log("this sort of expr isn't implemented!");
-            log_expr(e);
-            fail;
+        case (expr_check_expr(?p, ?a)) {
+            /* will need to change when we support arbitrary predicates... */
+            find_pre_post_expr(fm, enclosing, *p);
+            set_pre_and_post(a, expr_pp(*p));
+        }
+        case(expr_bind(?operator, ?maybe_args, ?a)) {
+            auto args = _vec.cat_options[@expr](maybe_args);
+            _vec.push[@expr](args, operator); /* ??? order of eval? */
+            find_pre_post_exprs(fm, enclosing, args, a);
+        }
+        case (expr_break(?a)) {
+            set_pre_and_post(a, empty_pre_post(num_local_vars));
+        }
+        case (expr_cont(?a)) {
+            set_pre_and_post(a, empty_pre_post(num_local_vars));
+        }
+        case (expr_port(?a)) {
+            set_pre_and_post(a, empty_pre_post(num_local_vars));
+        }
+        case (expr_ext(_, _, _, ?expanded, ?a)) {
+            find_pre_post_expr(fm, enclosing, *expanded);
+            set_pre_and_post(a, expr_pp(*expanded));
         }
     }
 }
@@ -1012,10 +1220,18 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () {
 fn gen(&fn_info enclosing, &ann a, def_id id) -> bool {
   check(enclosing.contains_key(id));
   let uint i = (enclosing.get(id))._0;
-
   ret set_in_postcond(i, (ann_to_ts_ann_fail_more(a)).conditions);
 }
 
+fn declare_var(&fn_info enclosing, def_id id, prestate pre)
+   -> prestate {
+    check(enclosing.contains_key(id));
+    let uint i = (enclosing.get(id))._0;
+    auto res = clone(pre);
+    relax_prestate(i, res);
+    ret res;
+}
+
 fn gen_poststate(&fn_info enclosing, &ann a, def_id id) -> bool {
   check(enclosing.contains_key(id));
   let uint i = (enclosing.get(id))._0;
@@ -1025,6 +1241,9 @@ fn gen_poststate(&fn_info enclosing, &ann a, def_id id) -> bool {
 
 fn find_pre_post_stmt(fn_info_map fm, &fn_info enclosing, &ast.stmt s)
     -> () {
+    log("stmt =");
+    log_stmt(s);
+
   auto num_local_vars = num_locals(enclosing);
   alt(s.node) {
     case(ast.stmt_decl(?adecl, ?a)) {
@@ -1039,7 +1258,13 @@ fn find_pre_post_stmt(fn_info_map fm, &fn_info enclosing, &ast.stmt s)
                         /* Inherit ann from initializer, and add var being
                            initialized to the postcondition */
                         set_pre_and_post(a, rhs_pp);
+                        /*  log("gen (decl):");
+                            log_stmt(s); */
                         gen(enclosing, a, alocal.id); 
+                        /*                     log_err("for stmt");
+                        log_stmt(s);
+                        log_err("pp = ");
+                        log_pp(stmt_pp(s)); */
                     }
                     case(none[ast.initializer]) {
                         auto pp = empty_pre_post(num_local_vars);
@@ -1064,8 +1289,30 @@ fn find_pre_post_stmt(fn_info_map fm, &fn_info enclosing, &ast.stmt s)
 
 fn find_pre_post_block(&fn_info_map fm, &fn_info enclosing, block b)
     -> () {
+    /* 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.
+     */
+    auto nv = num_locals(enclosing);
+
     fn do_one_(fn_info_map fm, fn_info i, &@stmt s) -> () {
         find_pre_post_stmt(fm, i, *s);
+        log("pre_post for stmt:");
+        log_stmt(*s);
+        log("is:");
+        log_pp(stmt_pp(*s));
     }
     auto do_one = bind do_one_(fm, enclosing, _);
     
@@ -1089,13 +1336,19 @@ fn find_pre_post_block(&fn_info_map fm, &fn_info enclosing, block b)
     auto g = get_pp_expr;
     plus_option[pre_and_post](pps,
        option.map[@expr, pre_and_post](g, b.node.expr));
-    auto block_precond  = seq_preconds(num_locals(enclosing), pps);
+
+    auto block_precond  = seq_preconds(enclosing, pps);
     auto h = get_post;
     auto postconds =  _vec.map[pre_and_post, postcond](h, pps);
     /* A block may be empty, so this next line ensures that the postconds
        vector is non-empty. */
     _vec.push[postcond](postconds, block_precond);
-    auto block_postcond = union_postconds(postconds);
+    auto block_postcond = empty_poststate(nv);
+    /* conservative approximation */
+    if (! has_nonlocal_exits(b)) {
+        block_postcond = union_postconds(nv, postconds);
+    }
+
     set_pre_and_post(b.node.a, rec(precondition=block_precond,
                                    postcondition=block_postcond));
 }
@@ -1107,6 +1360,9 @@ fn find_pre_post_fn(&fn_info_map fm, &fn_info fi, &_fn f) -> () {
 fn check_item_fn(&fn_info_map fm, &span sp, ident i, &ast._fn f,
                  vec[ast.ty_param] ty_params, def_id id, ann a) -> @item {
 
+    log("check_item_fn:");
+    log_fn(f, i, ty_params);
+
   check (fm.contains_key(id));
   find_pre_post_fn(fm, fm.get(id), f);  
 
@@ -1142,11 +1398,11 @@ fn find_pre_post_state_item(fn_info_map fm, fn_info enclosing, @item i)
   }
 }
 
-fn set_prestate_ann(ann a, prestate pre) -> bool {
-  alt (a) {
+fn set_prestate_ann(@ann a, prestate pre) -> bool {
+  alt (*a) {
     case (ann_type(_,_,?ts_a)) {
       check (! is_none[@ts_ann](ts_a));
-      ret set_prestate(*get[@ts_ann](ts_a), pre);
+      ret set_prestate(get[@ts_ann](ts_a), pre);
     }
     case (ann_none) {
       log("set_prestate_ann: expected an ann_type here");
@@ -1209,7 +1465,7 @@ fn set_pre_and_post(&ann a, pre_and_post pp) -> () {
             set_postcondition(t, pp.postcondition);
         }
         case (ann_none) {
-            log("set_pre_and_post: expected an ann_type here");
+            log_err("set_pre_and_post: expected an ann_type here");
             fail;
         }
     }
@@ -1246,17 +1502,37 @@ fn pure_exp(&ann a, &prestate p) -> bool {
   ret changed;
 }
 
+fn find_pre_post_state_loop(fn_info_map fm, fn_info enclosing,
+   prestate pres, &@decl d, &@expr index, &block body, &ann a) -> bool {
+    auto changed = false;
+
+    /* same issues as while */
+    changed = extend_prestate_ann(a, pres) || changed;
+    changed = find_pre_post_state_expr(fm, enclosing, pres, index)
+        || changed;
+    /* in general, would need the intersection of
+       (poststate of index, poststate of body) */
+    changed = find_pre_post_state_block(fm, enclosing,
+                expr_poststate(*index), body) || changed;
+    auto res_p = intersect_postconds(vec(expr_poststate(*index),
+                                         block_poststate(body)));
+  
+    changed = extend_poststate_ann(a, res_p) || changed;
+    ret changed;
+}
+
 fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing,
                             &prestate pres, &@expr e) -> bool {
   auto changed = false;
   auto num_local_vars = num_locals(enclosing);
 
+  /* FIXME could get rid of some of the copy/paste */
   alt (e.node) {
     case (expr_vec(?elts, _, ?a)) {
-      be find_pre_post_state_exprs(fm, enclosing, pres, a, elts); 
+      ret find_pre_post_state_exprs(fm, enclosing, pres, a, elts); 
     }
     case (expr_tup(?elts, ?a)) {
-      be find_pre_post_state_exprs(fm, enclosing, pres, a, elt_exprs(elts));
+      ret find_pre_post_state_exprs(fm, enclosing, pres, a, elt_exprs(elts));
     }
     case (expr_call(?operator, ?operands, ?a)) {
       /* do the prestate for the rator */
@@ -1267,15 +1543,56 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing,
                                     expr_poststate(*operator), a, operands)
           || changed);
     }
+    case (expr_spawn(_, _, ?operator, ?operands, ?a)) {
+        changed = find_pre_post_state_expr(fm, enclosing, pres, operator);
+        ret(find_pre_post_state_exprs(fm, enclosing,
+                 expr_poststate(*operator), a, operands)
+          || changed);
+    }
+    case (expr_bind(?operator, ?maybe_args, ?a)) {
+        changed = find_pre_post_state_expr(fm, enclosing, pres, operator)
+            || changed;
+        ret (find_pre_post_state_exprs(fm, enclosing,
+          expr_poststate(*operator), a, cat_options[@expr](maybe_args))
+            || changed);
+    }
     case (expr_path(_,_,?a)) {
       ret pure_exp(a, pres);
     }
     case (expr_log(_,?e,?a)) {
+        /* factor out the "one exp" pattern */
         changed = find_pre_post_state_expr(fm, enclosing, pres, e);
         changed = extend_prestate_ann(a, pres) || changed;
         changed = extend_poststate_ann(a, expr_poststate(*e)) || changed;
         ret changed;
     }
+    case (expr_chan(?e, ?a)) {
+        changed = find_pre_post_state_expr(fm, enclosing, pres, e);
+        changed = extend_prestate_ann(a, pres) || changed;
+        changed = extend_poststate_ann(a, expr_poststate(*e)) || changed;
+        ret changed;
+    }
+    case (expr_ext(_, _, _, ?expanded, ?a)) {
+        changed = find_pre_post_state_expr(fm, enclosing, pres, expanded);
+        changed = extend_prestate_ann(a, pres) || changed;
+        changed = extend_poststate_ann(a, expr_poststate(*expanded))
+           || changed;
+        ret changed;
+    }
+    case (expr_put(?maybe_e, ?a)) {
+        alt (maybe_e) {
+            case (some[@expr](?arg)) {
+                changed = find_pre_post_state_expr(fm, enclosing, pres, arg);
+                changed = extend_prestate_ann(a, pres) || changed;
+                changed = extend_poststate_ann(a, expr_poststate(*arg))
+                    || changed;
+                ret changed;
+            }
+            case (none[@expr]) {
+                ret pure_exp(a, pres);
+            }
+        }
+    }
     case (expr_lit(?l,?a)) {
         ret pure_exp(a, pres);
     }
@@ -1325,9 +1642,35 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing,
         }
         ret changed;
     }
+    case (expr_recv(?lhs, ?rhs, ?a)) {
+        extend_prestate_ann(a, pres);
+
+        alt (lhs.node) {
+            case (expr_path(?p, some[def](def_local(?d_id)), ?a_lhs)) {
+                // receive to local var
+                changed = pure_exp(a_lhs, pres) || changed;
+                changed = find_pre_post_state_expr(fm, enclosing, pres, rhs)
+                    || changed;
+                changed = extend_poststate_ann(a, expr_poststate(*rhs))
+                    || changed;
+                changed = gen_poststate(enclosing, a, d_id) || changed;
+            }
+            case (_) {
+                // receive to something that must already have been init'd
+                changed = find_pre_post_state_expr(fm, enclosing, pres, lhs)
+                    || changed;
+                changed = find_pre_post_state_expr(fm, enclosing,
+                     expr_poststate(*lhs), rhs) || changed;
+                changed = extend_poststate_ann(a, expr_poststate(*rhs))
+                    || changed;
+            }
+        }
+        ret changed;
+    }
+
     case (expr_ret(?maybe_ret_val, ?a)) {
         changed = extend_prestate_ann(a, pres) || changed;
-        set_poststate_ann(a, empty_poststate(num_local_vars));
+        set_poststate_ann(a, false_postcond(num_local_vars));
         alt(maybe_ret_val) {
             case (none[@expr]) { /* do nothing */ }
             case (some[@expr](?ret_val)) {
@@ -1337,6 +1680,12 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing,
         }
         ret changed;
     }
+    case (expr_be(?e, ?a)) {
+        changed = extend_prestate_ann(a, pres) || changed;
+        set_poststate_ann(a, false_postcond(num_local_vars));
+        changed = find_pre_post_state_expr(fm, enclosing, pres, e) || changed;
+        ret changed;
+    }
     case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) {
         changed = extend_prestate_ann(a, pres) || changed;
         changed = find_pre_post_state_expr(fm, enclosing, pres, antec)
@@ -1356,6 +1705,13 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing,
                 changed = extend_poststate_ann(a, poststate_res) || changed;
             }
         }
+        log("if:");
+        log_expr(*e);
+        log("new prestate:");
+        log_bitv(enclosing, pres);
+        log("new poststate:");
+        log_bitv(enclosing, expr_poststate(*e));
+
         ret changed;
     }
     case (expr_binary(?bop, ?l, ?r, ?a)) {
@@ -1368,6 +1724,25 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing,
         changed = extend_poststate_ann(a, expr_poststate(*r)) || changed;
         ret changed;
     }
+    case (expr_send(?l, ?r, ?a)) {
+        changed = extend_prestate_ann(a, pres) || changed;
+        changed = find_pre_post_state_expr(fm, enclosing, pres, l)
+                    || changed;
+        changed = find_pre_post_state_expr(fm,
+                    enclosing, expr_poststate(*l), r) || changed;
+        changed = extend_poststate_ann(a, expr_poststate(*r)) || changed;
+        ret changed;
+    }
+    case (expr_assign_op(?op, ?lhs, ?rhs, ?a)) {
+        /* quite similar to binary -- should abstract this */
+        changed = extend_prestate_ann(a, pres) || changed;
+        changed = find_pre_post_state_expr(fm, enclosing, pres, lhs)
+                    || changed;
+        changed = find_pre_post_state_expr(fm,
+                    enclosing, expr_poststate(*lhs), rhs) || changed;
+        changed = extend_poststate_ann(a, expr_poststate(*rhs)) || changed;
+        ret changed;
+    }
     case (expr_while(?test, ?body, ?a)) {
         changed = extend_prestate_ann(a, pres) || changed;
         /* to handle general predicates, we need to pass in
@@ -1387,6 +1762,33 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing,
                                         block_poststate(body)))) || changed;
         ret changed;
     }
+    case (expr_do_while(?body, ?test, ?a)) {
+        changed = extend_prestate_ann(a, pres) || changed;
+        changed = find_pre_post_state_block(fm, enclosing, pres, body)
+            || changed;
+        changed = find_pre_post_state_expr(fm, enclosing,
+                     block_poststate(body), test) || changed;
+
+        /* conservative approximination: if the body of the loop
+           could break or cont, we revert to the prestate
+           (TODO: could treat cont differently from break, since
+           if there's a cont, the test will execute) */
+        if (has_nonlocal_exits(body)) {
+            changed = set_poststate_ann(a, pres) || changed;
+        }
+        else {
+            changed = extend_poststate_ann(a, expr_poststate(*test))
+              || changed;
+        }
+
+        ret changed;
+    }
+    case (expr_for(?d, ?index, ?body, ?a)) {
+        ret find_pre_post_state_loop(fm, enclosing, pres, d, index, body, a);
+    }
+    case (expr_for_each(?d, ?index, ?body, ?a)) {
+        ret find_pre_post_state_loop(fm, enclosing, pres, d, index, body, a);
+    }
     case (expr_index(?e, ?sub, ?a)) {
         changed = extend_prestate_ann(a, pres) || changed; 
         changed = find_pre_post_state_expr(fm, enclosing, pres, e) || changed;
@@ -1399,13 +1801,21 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing,
         changed = extend_prestate_ann(a, pres) || changed; 
         changed = find_pre_post_state_expr(fm, enclosing, pres, e) || changed;
         auto e_post = expr_poststate(*e);
-        auto a_post = ann_to_poststate(a);
-        for (arm an_alt in alts) {
-            changed = find_pre_post_state_block(fm, enclosing, e_post,
-                        an_alt.block) || changed;
-            changed = intersect(a_post, block_poststate(an_alt.block))
-               || changed;
+        auto a_post;
+        if (_vec.len[arm](alts) > 0u) {
+            a_post = false_postcond(num_local_vars);
+            for (arm an_alt in alts) {
+                changed = find_pre_post_state_block(fm, enclosing, e_post,
+                                                    an_alt.block) || changed;
+                changed = intersect(a_post, block_poststate(an_alt.block))
+                    || changed; 
+            }
+        }
+        else {
+            // No alts; poststate is the poststate of the test
+            a_post = e_post;
         }
+        changed = extend_poststate_ann(a, a_post);
         ret changed;
     }
     case (expr_field(?e,_,?a)) {
@@ -1422,18 +1832,43 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing,
           || changed;
         ret changed;
     }
+    case (expr_cast(?operand, _, ?a)) {
+           changed = find_pre_post_state_expr(fm, enclosing, pres, operand)
+          || changed;
+        changed = extend_prestate_ann(a, pres) || changed;
+        changed = extend_poststate_ann(a, expr_poststate(*operand))
+          || changed;
+        ret changed;
+    }
     case (expr_fail(?a)) {
         changed = extend_prestate_ann(a, pres) || changed;
-        changed = set_poststate_ann(a, true_postcond(num_local_vars))
+        /* if execution continues after fail, then everything is true! woo! */
+        changed = set_poststate_ann(a, false_postcond(num_local_vars))
           || changed;
+        /*        log_err("fail: poststate = ");
+                  log_bitv(enclosing, expr_poststate(*e)); */
         ret changed;
     }
-    case (_) {
-      log("find_pre_post_state_expr: implement this case!");
-      fail;
+    case (expr_check_expr(?p, ?a)) {
+        changed = extend_prestate_ann(a, pres) || changed;
+        changed = find_pre_post_state_expr(fm, enclosing, pres, p) || changed;
+        /* p is pure, so the poststate must be the same as the prestate */
+        changed = extend_poststate_ann(a, pres) || changed;
+        ret changed;
+    }
+    case (expr_break(?a)) {
+        ret pure_exp(a, pres);
+    }
+    case (expr_cont(?a)) {
+        ret pure_exp(a, pres);
+    }
+    case (expr_port(?a)) {
+        ret pure_exp(a, pres);
+    }
+    case (expr_self_method(_, ?a)) {
+        ret pure_exp(a, pres);
     }
   }
-
 }
 
 fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing,
@@ -1442,7 +1877,6 @@ fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing,
   auto stmt_ann_ = stmt_to_ann(*s);
   check (!is_none[@ts_ann](stmt_ann_));
   auto stmt_ann = *(get[@ts_ann](stmt_ann_));
-  /*                  
               log("*At beginning: stmt = ");
               log_stmt(*s);
               log("*prestate = ");
@@ -1451,21 +1885,21 @@ fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing,
               log(bitv.to_str(stmt_ann.states.poststate));
               log("*changed =");
               log(changed);
-  */       
+  
   alt (s.node) {
     case (stmt_decl(?adecl, ?a)) {
       alt (adecl.node) {
         case (ast.decl_local(?alocal)) {
           alt (alocal.init) {
             case (some[ast.initializer](?an_init)) {
-              changed = find_pre_post_state_expr
-                (fm, enclosing, pres, an_init.expr) || changed;
-              changed = extend_poststate(stmt_ann.states.poststate,
-                                         expr_poststate(*an_init.expr))
-                  || changed;
-              changed = gen_poststate(enclosing, a, alocal.id) || changed;
-    
-              /*
+                changed = extend_prestate(stmt_ann.states.prestate, pres)
+                    || changed;
+                changed = find_pre_post_state_expr
+                    (fm, enclosing, pres, an_init.expr) || changed;
+                changed = extend_poststate(stmt_ann.states.poststate,
+                                           expr_poststate(*an_init.expr))
+                    || changed;
+                changed = gen_poststate(enclosing, a, alocal.id) || changed;
               log("Summary: stmt = ");
               log_stmt(*s);
               log("prestate = ");
@@ -1475,8 +1909,7 @@ fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing,
               log_bitv(enclosing, stmt_ann.states.poststate);
               log("changed =");
               log(changed);
-              */
-
+  
               ret changed;
             }
             case (none[ast.initializer]) {
@@ -1489,7 +1922,11 @@ fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing,
           }
         }
         case (ast.decl_item(?an_item)) {
-            be find_pre_post_state_item(fm, enclosing, an_item);
+            changed = extend_prestate(stmt_ann.states.prestate, pres)
+               || changed;
+            changed = extend_poststate(stmt_ann.states.poststate, pres)
+               || changed;
+            ret (find_pre_post_state_item(fm, enclosing, an_item) || changed);
         }
       }
     }
@@ -1500,12 +1937,13 @@ fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing,
       changed = extend_poststate(stmt_ann.states.poststate,
                                  expr_poststate(*e)) || changed;
       /*
-              log("Summary: stmt = ");
+                    log("Summary: stmt = ");
               log_stmt(*s);
               log("prestate = ");
               log(bitv.to_str(stmt_ann.states.prestate));
               log_bitv(enclosing, stmt_ann.states.prestate);
               log("poststate =");
+              log(bitv.to_str(stmt_ann.states.poststate));
               log_bitv(enclosing, stmt_ann.states.poststate);
               log("changed =");
               log(changed);
@@ -1519,9 +1957,9 @@ fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing,
 /* 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(&fn_info_map fm, &fn_info enclosing,
-                             &prestate pres0, block b)
+                             &prestate pres0, &block b)
   -> bool {
-
+    
   auto changed = false;
   auto num_local_vars = num_locals(enclosing);
 
@@ -1545,8 +1983,34 @@ fn find_pre_post_state_block(&fn_info_map fm, &fn_info enclosing,
       post = expr_poststate(*e);
     }
   }
-  set_prestate_ann(b.node.a, pres0);
+
+  /*
+  log_err("block:");
+  log_block_err(b);
+  log_err("has non-local exits?");
+  log_err(has_nonlocal_exits(b));
+  */
+
+  /* conservative approximation: if a block contains a break
+     or cont, we assume nothing about the poststate */
+  if (has_nonlocal_exits(b)) {
+      post = pres0;
+  }
+  
+  set_prestate_ann(@b.node.a, pres0);
   set_poststate_ann(b.node.a, post);
+
+
+  log("For block:");
+  log_block(b);
+  log("poststate = ");
+  log_states(block_states(b));
+  log("pres0:");
+  log_bitv(enclosing, pres0);
+  log("post:");
+  log_bitv(enclosing, post);
+
+
   ret changed;
 }
 
@@ -1579,12 +2043,12 @@ fn check_states_expr(fn_info enclosing, &expr e) -> () {
   let prestate pres   = expr_prestate(e);
 
   if (!implies(pres, prec)) {
-      log("check_states_expr: unsatisfied precondition for ");
-      log_expr(e);
-      log("Precondition: ");
-      log_bitv(enclosing, prec);
-      log("Prestate: ");
-      log_bitv(enclosing, pres);
+      log_err("check_states_expr: Unsatisfied precondition constraint for ");
+      log_expr_err(e);
+      log_err("Precondition: ");
+      log_bitv_err(enclosing, prec);
+      log_err("Prestate: ");
+      log_bitv_err(enclosing, pres);
       fail;
   }
 }
@@ -1608,12 +2072,13 @@ fn check_states_stmt(fn_info enclosing, &stmt s) -> () {
       */
 
       if (!implies(pres, prec)) {
-        log("check_states_stmt: unsatisfied precondition for ");
-        log_stmt(s);
-        log("Precondition: ");
-        log_bitv(enclosing, prec);
-        log("Prestate: ");
-        log_bitv(enclosing, pres);
+        log_err("check_states_stmt: "
+              + "Unsatisfied precondition constraint for ");
+        log_stmt_err(s);
+        log_err("Precondition: ");
+        log_bitv_err(enclosing, prec);
+        log_err("Prestate: ");
+        log_bitv_err(enclosing, pres);
         fail;
       }
     }
@@ -1638,12 +2103,12 @@ fn check_states_against_conditions(fn_info enclosing, &ast._fn f) -> () {
 fn check_fn_states(&fn_info_map f_info_map, &fn_info f_info, &ast._fn f)
     -> () {
   /* Compute the pre- and post-states for this function */
-  auto g = find_pre_post_state_fn;
-  fixed_point_states(f_info_map, f_info, g, f);
-
+    auto g = find_pre_post_state_fn;
+    fixed_point_states(f_info_map, f_info, g, f);
+    
   /* Now compare each expr's pre-state to its precondition
      and post-state to its postcondition */
-  check_states_against_conditions(f_info, f);
+    check_states_against_conditions(f_info, f);
 }
 
 fn check_item_fn_state(&fn_info_map f_info_map, &span sp, ident i,
@@ -1680,8 +2145,12 @@ fn check_obj_state(&fn_info_map f_info_map, vec[obj_field] fields,
 fn init_ann(&fn_info fi, ann a) -> ann {
     alt (a) {
         case (ann_none) {
-            log("init_ann: shouldn't see ann_none");
-            fail;
+            //            log("init_ann: shouldn't see ann_none");
+            // fail;
+            log("warning: init_ann: saw ann_none");
+            ret a; // Would be better to fail so we can catch bugs that
+            // result in an uninitialized ann -- but don't want to have to
+            // write code to handle native_mods properly
         }
         case (ann_type(?t,?ps,_)) {
             ret ann_type(t, ps, some[@ts_ann](@empty_ann(num_locals(fi))));
@@ -1692,8 +2161,10 @@ fn init_ann(&fn_info fi, ann a) -> ann {
 fn init_blank_ann(&() ignore, ann a) -> ann {
     alt (a) {
         case (ann_none) {
-            log("init_ann: shouldn't see ann_none");
-            fail;
+            //            log("init_blank_ann: shouldn't see ann_none");
+            //fail;
+            log("warning: init_blank_ann: saw ann_none");
+            ret a;
         }
         case (ann_type(?t,?ps,_)) {
             ret ann_type(t, ps, some[@ts_ann](@empty_ann(0u)));
@@ -1706,7 +2177,7 @@ fn init_block(&fn_info fi, &span sp, &block_ b) -> block {
     log_block(respan(sp, b));
     alt(b.a) {
         case (ann_none) {
-            log("init_ann: shouldn't see ann_none");
+            log("init_block: shouldn't see ann_none");
             fail;
         }
         case (ann_type(?t,?ps,_)) {
@@ -1730,7 +2201,6 @@ fn item_fn_anns(&fn_info_map fm, &span sp, ident i, &ast._fn f,
     auto fld0 = fold.new_identity_fold[fn_info]();
 
     fld0 = @rec(fold_ann = bind init_ann(_,_) 
-                //   fold_block = bind init_block(_,_,_)
                     with *fld0);
 
     ret fold.fold_item[fn_info]
@@ -1999,11 +2469,6 @@ fn annotate_mod(&fn_info_map fm, &ast._mod m) -> ast._mod {
     }
     ret rec(items=new_items, index=new_index with m);
 }
-fn annotate_native_mod(&fn_info_map fm, &ast.native_mod m)
-       -> ast.native_mod {
-    log("implement annotate_native_mod!");
-    fail;
-}
 fn annotate_method(&fn_info_map fm, &@method m) -> @method {
     auto f_info = get_fn_info(fm, m.node.id);
     auto fld0 = fold.new_identity_fold[fn_info]();
@@ -2044,9 +2509,7 @@ fn annotate_item_inner(&fn_info_map fm, &@ast.item item) -> @ast.item {
                        ast.item_mod(ident, annotate_mod(fm, mm), id));
         }
         case (ast.item_native_mod(?ident, ?mm, ?id)) {
-            ret @respan(item.span,
-                  ast.item_native_mod(ident, 
-                    annotate_native_mod(fm, mm), id));
+            ret item;
         }
         case (ast.item_ty(_,_,_,_,_)) {
             ret item;
@@ -2090,6 +2553,9 @@ fn annotate_item(&fn_info_map fm, &@ast.item item) -> @ast.item {
             auto outer = fold.fold_item[()]((), fld0, item);
             ret annotate_item_inner(fm, outer);
         }
+        case (ast.item_native_mod(?i, ?nm, ?id)) {
+            ret item;
+        }
         case (ast.item_ty(_,_,_,_,_)) {
             ret item;
         }
@@ -2130,13 +2596,8 @@ fn check_crate(@ast.crate crate) -> @ast.crate {
   auto fm = mk_f_to_fn_info(crate);
   
   /* Add a blank ts_ann to every statement (and expression) */
-  /*
-  auto fld0 = fold.new_identity_fold[fn_info_map]();
-  fld0 = @rec(fold_item_fn = bind item_fn_anns(_,_,_,_,_,_,_)
-              with *fld0);
-  */
   auto with_anns = annotate_crate(fm, crate);
-  
+
   /* Compute the pre and postcondition for every subexpression */
   auto fld = fold.new_identity_fold[fn_info_map]();
   fld = @rec(fold_item_fn = bind check_item_fn(_,_,_,_,_,_,_) with *fld);
diff --git a/src/comp/util/common.rs b/src/comp/util/common.rs
index a9e02c20e03ce..7484b4cf76f49 100644
--- a/src/comp/util/common.rs
+++ b/src/comp/util/common.rs
@@ -1,3 +1,5 @@
+import std.map;
+import std.map.hashmap;
 import std._uint;
 import std._int;
 import std._vec;
@@ -5,17 +7,22 @@ import std.option.none;
 import front.ast;
 import util.typestate_ann.ts_ann;
 
+import middle.fold;
+import middle.fold.respan;
+
 import std.io.stdout;
 import std.io.str_writer;
 import std.io.string_writer;
 import pretty.pprust.print_block;
 import pretty.pprust.print_expr;
 import pretty.pprust.print_decl;
+import pretty.pprust.print_fn;
 import pretty.pp.mkstate;
 
 type filename = str;
 type span = rec(uint lo, uint hi);
 type spanned[T] = rec(T node, span span);
+type flag = hashmap[str, ()];
 
 tag ty_mach {
     ty_i8;
@@ -98,9 +105,9 @@ fn uistr(uint i) -> str {
 
 fn elt_expr(&ast.elt e) -> @ast.expr { ret e.expr; }
 
-fn elt_exprs(vec[ast.elt] elts) -> vec[@ast.expr] {
+fn elt_exprs(&vec[ast.elt] elts) -> vec[@ast.expr] {
     auto f = elt_expr;
-    be _vec.map[ast.elt, @ast.expr](f, elts);
+    ret _vec.map[ast.elt, @ast.expr](f, elts);
 }
 
 fn field_expr(&ast.field f) -> @ast.expr { ret f.expr; }
@@ -115,18 +122,25 @@ fn plain_ann(middle.ty.ctxt tcx) -> ast.ann {
                    none[vec[middle.ty.t]], none[@ts_ann]);
 }
 
-fn log_expr(&ast.expr e) -> () {
+fn expr_to_str(&ast.expr e) -> str {
   let str_writer s = string_writer();
   auto out_ = mkstate(s.get_writer(), 80u);
   auto out = @rec(s=out_,
                   comments=none[vec[front.lexer.cmnt]],
                   mutable cur_cmnt=0u);
-
   print_expr(out, @e);
-  log(s.get_str());
+  ret s.get_str();
 }
 
-fn log_block(&ast.block b) -> () {
+fn log_expr(&ast.expr e) -> () {
+    log(expr_to_str(e));
+}
+
+fn log_expr_err(&ast.expr e) -> () {
+    log_err(expr_to_str(e));
+}
+
+fn block_to_str(&ast.block b) -> str {
   let str_writer s = string_writer();
   auto out_ = mkstate(s.get_writer(), 80u);
   auto out = @rec(s=out_,
@@ -134,7 +148,15 @@ fn log_block(&ast.block b) -> () {
                   mutable cur_cmnt=0u);
 
   print_block(out, b);
-  log(s.get_str());
+  ret s.get_str();
+}
+
+fn log_block(&ast.block b) -> () {
+    log(block_to_str(b));
+}
+
+fn log_block_err(&ast.block b) -> () {
+    log_err(block_to_str(b));
 }
 
 fn log_ann(&ast.ann a) -> () {
@@ -148,7 +170,26 @@ fn log_ann(&ast.ann a) -> () {
     }
 }
 
-fn log_stmt(ast.stmt st) -> () {
+fn fun_to_str(&ast._fn f, str name, vec[ast.ty_param] params) -> str {
+ let str_writer s = string_writer();
+  auto out_ = mkstate(s.get_writer(), 80u);
+  auto out = @rec(s=out_,
+                  comments=none[vec[front.lexer.cmnt]],
+                  mutable cur_cmnt=0u);
+
+  print_fn(out, f.decl, name, params);
+  ret s.get_str();
+}
+
+fn log_fn(&ast._fn f, str name, vec[ast.ty_param] params) -> () {
+    log(fun_to_str(f, name, params));
+}
+
+fn log_fn_err(&ast._fn f, str name, vec[ast.ty_param] params) -> () {
+    log_err(fun_to_str(f, name, params));
+}
+
+fn stmt_to_str(&ast.stmt st) -> str {
   let str_writer s = string_writer();
   auto out_ = mkstate(s.get_writer(), 80u);
   auto out = @rec(s=out_,
@@ -163,9 +204,76 @@ fn log_stmt(ast.stmt st) -> () {
     }
     case (_) { /* do nothing */ }
   }
-  log(s.get_str());
+  ret s.get_str();
+}
+
+fn log_stmt(&ast.stmt st) -> () {
+    log(stmt_to_str(st));
+}
+
+fn log_stmt_err(&ast.stmt st) -> () {
+    log_err(stmt_to_str(st));
+}
+
+fn decl_lhs(@ast.decl d) -> ast.def_id {
+    alt (d.node) {
+        case (ast.decl_local(?l)) {
+            ret l.id;
+        }
+        case (ast.decl_item(?an_item)) {
+            alt (an_item.node) {
+                case (ast.item_const(_,_,_,?d,_)) {
+                    ret d;
+                }
+                case (ast.item_fn(_,_,_,?d,_)) {
+                    ret d;
+                }
+                case (ast.item_mod(_,_,?d)) {
+                    ret d;
+                }
+                case (ast.item_native_mod(_,_,?d)) {
+                    ret d;
+                }
+                case (ast.item_ty(_,_,_,?d,_)) {
+                    ret d;
+                }
+                case (ast.item_tag(_,_,_,?d,_)) {
+                    ret d;
+                }
+                case (ast.item_obj(_,_,_,?d,_)) {
+                    ret d.ctor; /* This doesn't really make sense */
+                }
+            }
+        } 
+    }
 }
 
+fn has_nonlocal_exits(&ast.block b) -> bool {
+    /* overkill, but just passing around a mutable bool doesn't seem
+       to work in rustboot */
+    auto has_exits = new_str_hash[()]();
+ 
+   fn set_break(&flag f, &span sp, ast.ann a) -> @ast.expr {
+        f.insert("foo", ());
+        ret @respan(sp, ast.expr_break(a));
+    }
+    fn set_cont(&flag f, &span sp, ast.ann a) -> @ast.expr {
+        f.insert("foo", ());
+        ret @respan(sp, ast.expr_cont(a));
+    }
+    fn check_b(&flag f) -> bool {
+        ret (f.size() == 0u);
+    }
+
+    auto fld0 = fold.new_identity_fold[flag]();
+
+    fld0 = @rec(fold_expr_break = bind set_break(_,_,_),
+                fold_expr_cont  = bind set_cont(_,_,_),
+                keep_going      = bind check_b(_) with *fld0);
+    fold.fold_block[flag](has_exits, fld0, b);
+
+    ret (has_exits.size() > 0u);
+}
 //
 // Local Variables:
 // mode: rust
diff --git a/src/comp/util/typestate_ann.rs b/src/comp/util/typestate_ann.rs
index 9ad6e01e8dd27..b7fbc3cc25d58 100644
--- a/src/comp/util/typestate_ann.rs
+++ b/src/comp/util/typestate_ann.rs
@@ -44,6 +44,10 @@ fn empty_poststate(uint num_vars) -> poststate {
   be true_precond(num_vars);
 }
 
+fn false_postcond(uint num_vars) -> postcond {
+    be bitv.create(num_vars, true);
+}
+
 fn empty_pre_post(uint num_vars) -> pre_and_post {
   ret(rec(precondition=empty_prestate(num_vars),
           postcondition=empty_poststate(num_vars)));
@@ -119,7 +123,7 @@ fn set_postcondition(&ts_ann a, &postcond p) -> () {
 
 // Sets all the bits in a's prestate to equal the
 // corresponding bit in p's prestate.
-fn set_prestate(&ts_ann a, &prestate p) -> bool {
+fn set_prestate(@ts_ann a, &prestate p) -> bool {
   ret bitv.copy(a.states.prestate, p);
 }
 
@@ -139,6 +143,13 @@ fn extend_poststate(&poststate p, &poststate new) -> bool {
   ret bitv.union(p, new);
 }
 
+// Clears the given bit in p
+fn relax_prestate(uint i, &prestate p) -> bool {
+    auto was_set = bitv.get(p, i);
+    bitv.set(p, i, false);
+    ret was_set;
+}
+
 fn ann_precond(&ts_ann a) -> precond {
   ret a.conditions.precondition;
 }
@@ -148,8 +159,12 @@ fn ann_prestate(&ts_ann a) -> prestate {
 }
 
 fn pp_clone(&pre_and_post p) -> pre_and_post {
-  ret rec(precondition=bitv.clone(p.precondition),
-          postcondition=bitv.clone(p.postcondition));
+  ret rec(precondition=clone(p.precondition),
+          postcondition=clone(p.postcondition));
+}
+
+fn clone(prestate p) -> prestate {
+    ret bitv.clone(p);
 }
 
 // returns true if a implies b
diff --git a/src/lib/_vec.rs b/src/lib/_vec.rs
index cc8fabcaf1606..21a6cff560d94 100644
--- a/src/lib/_vec.rs
+++ b/src/lib/_vec.rs
@@ -280,6 +280,21 @@ fn plus_option[T](&vec[T] v, &option.t[T] o) -> () {
     }
 }
 
+fn cat_options[T](&vec[option.t[T]] v) -> vec[T] {
+    let vec[T] res = vec();
+
+    for (option.t[T] o in v) {
+        alt (o) {
+            case (none[T]) { }
+            case (some[T](?t)) {
+                res += vec(t);
+            }
+        }
+    }
+
+    ret res;
+}
+
 // TODO: Remove in favor of built-in "freeze" operation when it's implemented.
 fn freeze[T](vec[mutable T] v) -> vec[T] {
     let vec[T] result = vec();
diff --git a/src/rt/rust_crate_cache.cpp b/src/rt/rust_crate_cache.cpp
index 3fdb33b9896b2..3ab4a822e2ea8 100644
--- a/src/rt/rust_crate_cache.cpp
+++ b/src/rt/rust_crate_cache.cpp
@@ -49,7 +49,8 @@ rust_crate_cache::c_sym::c_sym(rust_dom *dom, lib *library, char const *name)
         DLOG(dom, cache, "resolved symbol '%s' to 0x%"  PRIxPTR,
                  name, val);
     } else {
-        DLOG_ERR(dom, cache, "unresolved symbol '%s', null lib handle", name);
+        DLOG_ERR(dom, cache, "unresolved symbol '%s', null lib handle\n"
+                             "(did you omit a -L flag?)", name);
     }
 }
 
diff --git a/src/test/compile-fail/break-uninit.rs b/src/test/compile-fail/break-uninit.rs
new file mode 100644
index 0000000000000..097312b2b6408
--- /dev/null
+++ b/src/test/compile-fail/break-uninit.rs
@@ -0,0 +1,21 @@
+// xfail-boot
+// error-pattern:Unsatisfied precondition
+
+fn foo() -> int {
+  let int x;
+  let int i;
+
+  do {
+    i = 0;
+    break;
+    x = 0;
+  } while ((x = 0) != 0);
+
+  log(x);
+
+  ret 17;
+}
+
+fn main() {
+  log(foo());
+}
diff --git a/src/test/compile-fail/break-uninit2.rs b/src/test/compile-fail/break-uninit2.rs
new file mode 100644
index 0000000000000..45d758f61943d
--- /dev/null
+++ b/src/test/compile-fail/break-uninit2.rs
@@ -0,0 +1,21 @@
+// xfail-boot
+// error-pattern:Unsatisfied precondition
+
+fn foo() -> int {
+  let int x;
+  let int i;
+
+  do {
+    i = 0;
+    break;
+    x = 0;
+  } while (1 != 2);
+
+  log(x);
+
+  ret 17;
+}
+
+fn main() {
+  log(foo());
+}
diff --git a/src/test/compile-fail/fru-typestate.rs b/src/test/compile-fail/fru-typestate.rs
index 74fcdb265205d..86c68e5b9056d 100644
--- a/src/test/compile-fail/fru-typestate.rs
+++ b/src/test/compile-fail/fru-typestate.rs
@@ -1,4 +1,3 @@
-// xfail-stage0
 // -*- rust -*-
 
 // error-pattern: precondition
diff --git a/src/test/compile-fail/return-uninit.rs b/src/test/compile-fail/return-uninit.rs
index 047db518fab43..3711716927a39 100644
--- a/src/test/compile-fail/return-uninit.rs
+++ b/src/test/compile-fail/return-uninit.rs
@@ -1,4 +1,3 @@
-// xfail-stage0
 // error-pattern: precondition constraint
 
 fn f() -> int {
diff --git a/src/test/compile-fail/use-uninit-2.rs b/src/test/compile-fail/use-uninit-2.rs
index c77676b80999f..79cebe2811f87 100644
--- a/src/test/compile-fail/use-uninit-2.rs
+++ b/src/test/compile-fail/use-uninit-2.rs
@@ -1,4 +1,3 @@
-// xfail-stage0
 // error-pattern:Unsatisfied precondition
 
 fn foo(int x) {
diff --git a/src/test/compile-fail/use-uninit-3.rs b/src/test/compile-fail/use-uninit-3.rs
index 5dd3926ba0dfc..e65454518a328 100644
--- a/src/test/compile-fail/use-uninit-3.rs
+++ b/src/test/compile-fail/use-uninit-3.rs
@@ -1,4 +1,3 @@
-// xfail-stage0
 // error-pattern:Unsatisfied precondition
 
 fn foo(int x) {
diff --git a/src/test/compile-fail/use-uninit-dtor.rs b/src/test/compile-fail/use-uninit-dtor.rs
index be2f1727a6ffc..fed90df61f696 100644
--- a/src/test/compile-fail/use-uninit-dtor.rs
+++ b/src/test/compile-fail/use-uninit-dtor.rs
@@ -1,4 +1,3 @@
-// xfail-stage0
 // error-pattern:Unsatisfied precondition
 
 fn main() {
diff --git a/src/test/compile-fail/use-uninit.rs b/src/test/compile-fail/use-uninit.rs
index bd2e9f416a2ee..03dafdcc00384 100644
--- a/src/test/compile-fail/use-uninit.rs
+++ b/src/test/compile-fail/use-uninit.rs
@@ -1,4 +1,3 @@
-// xfail-stage0
 // error-pattern:Unsatisfied precondition
 
 fn foo(int x) {
diff --git a/src/test/compile-fail/while-bypass.rs b/src/test/compile-fail/while-bypass.rs
index b49152b3e98cb..1de89e909dafb 100644
--- a/src/test/compile-fail/while-bypass.rs
+++ b/src/test/compile-fail/while-bypass.rs
@@ -1,4 +1,3 @@
-// xfail-stage0
 // error-pattern: precondition constraint
 
 fn f() -> int {
diff --git a/src/test/compile-fail/while-expr.rs b/src/test/compile-fail/while-expr.rs
index 295752f8e0299..9077c18fd62f4 100644
--- a/src/test/compile-fail/while-expr.rs
+++ b/src/test/compile-fail/while-expr.rs
@@ -1,4 +1,3 @@
-// xfail-stage0
 // error-pattern: precondition constraint
 
 fn main() {
diff --git a/src/test/compile-fail/writing-through-uninit-vec.rs b/src/test/compile-fail/writing-through-uninit-vec.rs
index 7757609df7839..55edbf8787515 100644
--- a/src/test/compile-fail/writing-through-uninit-vec.rs
+++ b/src/test/compile-fail/writing-through-uninit-vec.rs
@@ -1,4 +1,3 @@
-// xfail-stage0
 // error-pattern: Unsatisfied precondition constraint
 
 fn test() {
diff --git a/src/test/run-pass/alt-join.rs b/src/test/run-pass/alt-join.rs
new file mode 100644
index 0000000000000..152fac5d7bc17
--- /dev/null
+++ b/src/test/run-pass/alt-join.rs
@@ -0,0 +1,34 @@
+use std;
+import std.option;
+import std.option.t;
+import std.option.none;
+import std.option.some;
+
+fn foo[T](&option.t[T] y) {
+  let int x;
+  
+  let vec[int] res = vec();
+  
+  /* tests that x doesn't get put in the precondition for the 
+     entire if expression */
+  if (true) {
+  }
+  else {
+    alt (y) {
+      case (none[T]) {
+        x = 17;
+      }
+      case (_) {
+        x = 42;
+      }
+    }
+    res += vec(x);
+  }
+
+  ret;
+}
+
+fn main() {
+  log("hello");
+  foo[int](some[int](5));
+}
\ No newline at end of file
diff --git a/src/test/run-pass/nested-pattern.rs b/src/test/run-pass/nested-pattern.rs
new file mode 100644
index 0000000000000..e59c2dd5a4160
--- /dev/null
+++ b/src/test/run-pass/nested-pattern.rs
@@ -0,0 +1,29 @@
+// a bug was causing this to complain about leaked memory on exit
+
+use std;
+import std.option;
+import std.option.some;
+import std.option.none;
+
+tag t {
+  foo(int, uint);
+  bar(int, option.t[int]);
+}
+
+fn nested(t o) {
+
+  alt (o) {
+    case (bar(?i, some[int](_))) {
+      log_err "wrong pattern matched";
+      fail;
+    }
+    case (_) {
+      log_err "succeeded";
+    }
+  }
+
+}
+
+fn main() {
+  nested (bar (1, none[int]));
+}
\ No newline at end of file
diff --git a/src/test/run-pass/use-uninit-alt.rs b/src/test/run-pass/use-uninit-alt.rs
new file mode 100644
index 0000000000000..a7c77bba2eaac
--- /dev/null
+++ b/src/test/run-pass/use-uninit-alt.rs
@@ -0,0 +1,21 @@
+fn foo[T](&myoption[T] o) -> int {
+  let int x = 5;
+
+  alt (o) {
+    case (none[T]) { }
+    case (some[T](?t)) {
+      x += 1;
+    }
+  }
+  
+  ret x;
+}
+
+tag myoption[T] {
+  none;
+  some(T);
+}
+
+fn main() {
+  log(5);
+}
\ No newline at end of file
diff --git a/src/test/run-pass/use-uninit-alt2.rs b/src/test/run-pass/use-uninit-alt2.rs
new file mode 100644
index 0000000000000..36514d13ce139
--- /dev/null
+++ b/src/test/run-pass/use-uninit-alt2.rs
@@ -0,0 +1,21 @@
+fn foo[T](&myoption[T] o) -> int {
+  let int x;
+
+  alt (o) {
+    case (none[T]) { fail; }
+    case (some[T](?t)) {
+      x = 5;
+    }
+  }
+  
+  ret x;
+}
+
+tag myoption[T] {
+  none;
+  some(T);
+}
+
+fn main() {
+  log(5);
+}
\ No newline at end of file