diff --git a/src/comp/middle/trans.rs b/src/comp/middle/trans.rs
index cf16d31728332..997e41e0cb963 100644
--- a/src/comp/middle/trans.rs
+++ b/src/comp/middle/trans.rs
@@ -1953,6 +1953,13 @@ fn make_drop_glue(@block_ctxt cx, ValueRef v0, ty.t t) {
                        ty.type_is_nil(cx.fcx.lcx.ccx.tystore, t)) {
                 rslt = res(cx, C_nil());
             }
+            else {
+                // task, native_fn, var, local, param, bound_param
+                cx.fcx.lcx.ccx.sess.bug
+                    ("unexpected type in trans.make_drop_glue: " +
+                     ty.ty_to_str(cx.fcx.lcx.ccx.tystore, t));
+                fail;
+            }
         }
     }
 
diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs
index f86e2c4f95c53..0ae626e8d91a2 100644
--- a/src/comp/middle/typeck.rs
+++ b/src/comp/middle/typeck.rs
@@ -102,7 +102,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)) {
@@ -153,7 +153,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;
         }
 
@@ -205,23 +205,28 @@ fn instantiate_path(@fn_ctxt fcx, &ast.path pth, &ty_param_count_and_ty tpt,
 // Parses the programmer's textual representation of a type into our internal
 // notion of a type. `getter` is a function that returns the type
 // corresponding to a definition ID.
-fn ast_ty_to_ty(@ty.type_store tystore,
+fn ast_ty_to_ty(session.session sess,
+                @ty.type_store tystore,
                 ty_getter getter,
                 &@ast.ty ast_ty) -> ty.t {
-    fn ast_arg_to_arg(@ty.type_store tystore,
+    fn ast_arg_to_arg(session.session sess,
+                      @ty.type_store tystore,
                       ty_getter getter,
                       &rec(ast.mode mode, @ast.ty ty) arg)
             -> rec(ast.mode mode, ty.t ty) {
-        ret rec(mode=arg.mode, ty=ast_ty_to_ty(tystore, getter, arg.ty));
+        ret rec(mode=arg.mode, ty=ast_ty_to_ty(sess, tystore,
+                  getter, arg.ty));
     }
 
-    fn ast_mt_to_mt(@ty.type_store tystore,
+    fn ast_mt_to_mt(session.session sess,
+                    @ty.type_store tystore,
                     ty_getter getter,
                     &ast.mt mt) -> ty.mt {
-        ret rec(ty=ast_ty_to_ty(tystore, getter, mt.ty), mut=mt.mut);
+        ret rec(ty=ast_ty_to_ty(sess, tystore, getter, mt.ty), mut=mt.mut);
     }
 
-    fn instantiate(@ty.type_store tystore,
+    fn instantiate(session.session sess,
+                   @ty.type_store tystore,
                    ty_getter getter,
                    ast.def_id id,
                    vec[@ast.ty] args) -> ty.t {
@@ -240,7 +245,8 @@ fn ast_ty_to_ty(@ty.type_store tystore,
         auto bound_ty = bind_params_in_type(tystore, params_opt_and_ty._1);
         let vec[ty.t] param_bindings = vec();
         for (@ast.ty ast_ty in args) {
-            param_bindings += vec(ast_ty_to_ty(tystore, getter, ast_ty));
+            param_bindings += vec(ast_ty_to_ty(sess, tystore,
+                                    getter, ast_ty));
         }
         ret ty.substitute_type_params(tystore, param_bindings, bound_ty);
     }
@@ -258,40 +264,41 @@ fn ast_ty_to_ty(@ty.type_store tystore,
         case (ast.ty_char)         { typ = ty.mk_char(tystore); }
         case (ast.ty_str)          { typ = ty.mk_str(tystore); }
         case (ast.ty_box(?mt)) {
-            typ = ty.mk_box(tystore, ast_mt_to_mt(tystore, getter, mt));
+            typ = ty.mk_box(tystore, ast_mt_to_mt(sess, tystore, getter, mt));
         }
         case (ast.ty_vec(?mt)) {
-            typ = ty.mk_vec(tystore, ast_mt_to_mt(tystore, getter, mt));
+            typ = ty.mk_vec(tystore, ast_mt_to_mt(sess, tystore, getter, mt));
         }
 
         case (ast.ty_port(?t)) {
-            typ = ty.mk_port(tystore, ast_ty_to_ty(tystore, getter, t));
+            typ = ty.mk_port(tystore, ast_ty_to_ty(sess, tystore, getter, t));
         }
 
         case (ast.ty_chan(?t)) {
-            typ = ty.mk_chan(tystore, ast_ty_to_ty(tystore, getter, t));
+            typ = ty.mk_chan(tystore, ast_ty_to_ty(sess, tystore, getter, t));
         }
 
         case (ast.ty_tup(?fields)) {
             let vec[ty.mt] flds = vec();
             for (ast.mt field in fields) {
-                _vec.push[ty.mt](flds, ast_mt_to_mt(tystore, getter, field));
+                _vec.push[ty.mt](flds, ast_mt_to_mt(sess, tystore,
+                                          getter, field));
             }
             typ = ty.mk_tup(tystore, flds);
         }
         case (ast.ty_rec(?fields)) {
             let vec[field] flds = vec();
             for (ast.ty_field f in fields) {
-                auto tm = ast_mt_to_mt(tystore, getter, f.mt);
+                auto tm = ast_mt_to_mt(sess, tystore, getter, f.mt);
                 _vec.push[field](flds, rec(ident=f.ident, mt=tm));
             }
             typ = ty.mk_rec(tystore, flds);
         }
 
         case (ast.ty_fn(?proto, ?inputs, ?output)) {
-            auto f = bind ast_arg_to_arg(tystore, getter, _);
+            auto f = bind ast_arg_to_arg(sess, tystore, getter, _);
             auto i = _vec.map[ast.ty_arg, arg](f, inputs);
-            auto out_ty = ast_ty_to_ty(tystore, getter, output);
+            auto out_ty = ast_ty_to_ty(sess, tystore, getter, output);
             typ = ty.mk_fn(tystore, proto, i, out_ty);
         }
 
@@ -299,14 +306,20 @@ fn ast_ty_to_ty(@ty.type_store tystore,
             check (def != none[ast.def]);
             alt (option.get[ast.def](def)) {
                 case (ast.def_ty(?id)) {
-                    typ = instantiate(tystore, getter, id, path.node.types);
+                    typ = instantiate(sess, tystore, getter,
+                            id, path.node.types);
                 }
                 case (ast.def_native_ty(?id)) { typ = getter(id)._1; }
                 case (ast.def_obj(?id)) {
-                    typ = instantiate(tystore, getter, id, path.node.types);
+                    typ = instantiate(sess, tystore, getter,
+                            id, path.node.types);
                 }
                 case (ast.def_ty_arg(?id)) { typ = ty.mk_param(tystore, id); }
-                case (_)                   { fail; }
+                case (_)                   { 
+                    sess.span_err(ast_ty.span,
+                       "found type name used as a variable");
+                    fail;
+                }
             }
 
             cname = some(path_to_str(path));
@@ -314,10 +327,10 @@ fn ast_ty_to_ty(@ty.type_store tystore,
 
         case (ast.ty_obj(?meths)) {
             let vec[ty.method] tmeths = vec();
-            auto f = bind ast_arg_to_arg(tystore, getter, _);
+            auto f = bind ast_arg_to_arg(sess, tystore, getter, _);
             for (ast.ty_method m in meths) {
                 auto ins = _vec.map[ast.ty_arg, arg](f, m.inputs);
-                auto out = ast_ty_to_ty(tystore, getter, m.output);
+                auto out = ast_ty_to_ty(sess, tystore, getter, m.output);
                 _vec.push[ty.method](tmeths,
                                   rec(proto=m.proto,
                                       ident=m.ident,
@@ -345,7 +358,7 @@ fn ast_ty_to_ty_crate(@crate_ctxt ccx, &@ast.ty ast_ty) -> ty.t {
         ret ty.lookup_item_type(ccx.sess, ccx.tystore, ccx.type_cache, id);
     }
     auto f = bind getter(ccx, _);
-    ret ast_ty_to_ty(ccx.tystore, f, ast_ty);
+    ret ast_ty_to_ty(ccx.sess, ccx.tystore, f, ast_ty);
 }
 
 
@@ -422,12 +435,12 @@ mod Collect {
 
     fn ty_of_arg(@ctxt cx, &ast.arg a) -> arg {
         auto f = bind getter(cx, _);
-        ret rec(mode=a.mode, ty=ast_ty_to_ty(cx.tystore, f, a.ty));
+        ret rec(mode=a.mode, ty=ast_ty_to_ty(cx.sess, cx.tystore, f, a.ty));
     }
 
     fn ty_of_method(@ctxt cx, &@ast.method m) -> method {
         auto get = bind getter(cx, _);
-        auto convert = bind ast_ty_to_ty(cx.tystore, get, _);
+        auto convert = bind ast_ty_to_ty(cx.sess, cx.tystore, get, _);
         auto f = bind ty_of_arg(cx, _);
         auto inputs = _vec.map[ast.arg,arg](f, m.node.meth.decl.inputs);
         auto output = convert(m.node.meth.decl.output);
@@ -458,7 +471,7 @@ mod Collect {
         let vec[arg] t_inputs = vec();
         for (ast.obj_field f in obj_info.fields) {
             auto g = bind getter(cx, _);
-            auto t_field = ast_ty_to_ty(cx.tystore, g, f.ty);
+            auto t_field = ast_ty_to_ty(cx.sess, cx.tystore, g, f.ty);
             _vec.push[arg](t_inputs, rec(mode=ast.alias, ty=t_field));
         }
 
@@ -471,7 +484,7 @@ mod Collect {
     fn ty_of_item(@ctxt cx, @ast.item it) -> ty.ty_param_count_and_ty {
 
         auto get = bind getter(cx, _);
-        auto convert = bind ast_ty_to_ty(cx.tystore, get, _);
+        auto convert = bind ast_ty_to_ty(cx.sess, cx.tystore, get, _);
 
         alt (it.node) {
 
@@ -537,7 +550,7 @@ mod Collect {
             case (ast.native_item_fn(?ident, ?lname, ?fn_decl,
                                      ?params, ?def_id, _)) {
                 auto get = bind getter(cx, _);
-                auto convert = bind ast_ty_to_ty(cx.tystore, get, _);
+                auto convert = bind ast_ty_to_ty(cx.sess, cx.tystore, get, _);
                 auto f = bind ty_of_arg(cx, _);
                 ret ty_of_native_fn_decl(cx, convert, f, fn_decl, abi, params,
                                          def_id);
@@ -585,7 +598,7 @@ mod Collect {
 
                 let vec[arg] args = vec();
                 for (ast.variant_arg va in variant.node.args) {
-                    auto arg_ty = ast_ty_to_ty(cx.tystore, f, va.ty);
+                    auto arg_ty = ast_ty_to_ty(cx.sess, cx.tystore, f, va.ty);
                     args += vec(rec(mode=ast.alias, ty=arg_ty));
                 }
                 auto tag_t = ty.mk_tag(cx.tystore, tag_id, ty_param_tys);
@@ -735,7 +748,7 @@ mod Collect {
         }
         auto g = bind getter(e.cx, _);
         for (ast.obj_field fld in ob.fields) {
-            let ty.t fty = ast_ty_to_ty(e.cx.tystore, g, fld.ty);
+            let ty.t fty = ast_ty_to_ty(e.cx.sess, e.cx.tystore, g, fld.ty);
             let ast.obj_field f = rec(ann=triv_ann(fty)
                 with fld
             );
@@ -1827,7 +1840,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);
@@ -2620,15 +2633,17 @@ 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.tystore)));
                 }
 
                 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.tystore)));
                 }
             }
 
-            ret stmt;
+            //         ret stmt;
         }
 
         case (ast.stmt_expr(?expr,?a)) {
@@ -2636,7 +2651,8 @@ fn check_stmt(&@fn_ctxt fcx, &@ast.stmt stmt) -> @ast.stmt {
             expr_t = Pushdown.pushdown_expr(fcx,
                                             expr_ty(fcx.ccx.tystore, 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.tystore)));
         }
     }
 
diff --git a/src/comp/middle/typestate_check.rs b/src/comp/middle/typestate_check.rs
index 8a6e840a4284e..2bbcc3e722520 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);
   }
 
@@ -435,6 +489,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 +733,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 +775,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 +881,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 +899,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 +925,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 +970,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 +1008,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 +1019,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 +1079,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 +1105,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 +1165,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 +1188,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 +1222,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 +1243,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 +1260,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 +1291,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 +1338,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 +1362,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 +1400,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 +1467,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 +1504,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 +1545,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 +1644,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 +1682,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 +1707,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 +1726,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 +1764,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 +1803,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 +1834,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 +1879,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 +1887,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 +1911,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 +1924,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);
         }
       }
     }
@@ -1499,17 +1938,18 @@ fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing,
           || changed;
       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);
-      */
+      
       ret changed;
     }
     case (_) { ret false; }
@@ -1519,9 +1959,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 +1985,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 +2045,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 +2074,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;
       }
     }
@@ -1680,8 +2147,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 +2163,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 +2179,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 +2203,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 +2471,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 +2511,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 +2555,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;
         }
diff --git a/src/comp/util/common.rs b/src/comp/util/common.rs
index 0d0ca05da4bad..e78e969ba1311 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.type_store tystore) -> 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/test/compile-fail/break-uninit.rs b/src/test/compile-fail/break-uninit.rs
new file mode 100644
index 0000000000000..e9085dd25e823
--- /dev/null
+++ b/src/test/compile-fail/break-uninit.rs
@@ -0,0 +1,22 @@
+// xfail-boot
+// xfail-stage0
+// 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..8ef83f08cf5ec
--- /dev/null
+++ b/src/test/compile-fail/break-uninit2.rs
@@ -0,0 +1,22 @@
+// xfail-boot
+// xfail-stage0
+// 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/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/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