diff --git a/src/comp/middle/fold.rs b/src/comp/middle/fold.rs
index ef592fc8ab3..25617640734 100644
--- a/src/comp/middle/fold.rs
+++ b/src/comp/middle/fold.rs
@@ -291,8 +291,6 @@ type ast_fold[ENV] =
      (fn(&ENV e, ann a) -> ann)                   fold_ann,
 
      // Additional nodes.
-     (fn(&ENV e, &span sp,
-         &ast.block_) -> block)                   fold_block,
 
      (fn(&ENV e, &fn_decl decl,
          ast.proto proto,
@@ -1716,7 +1714,6 @@ fn new_identity_fold[ENV]() -> ast_fold[ENV] {
 
          fold_ann = bind identity_fold_ann[ENV](_,_),
 
-         fold_block = bind identity_fold_block[ENV](_,_,_),
          fold_fn = bind identity_fold_fn[ENV](_,_,_,_),
          fold_fn_decl = bind identity_fold_fn_decl[ENV](_,_,_),
          fold_mod = bind identity_fold_mod[ENV](_,_),
diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs
index 87c11a7b90a..95ed4c2fd3a 100644
--- a/src/comp/middle/typeck.rs
+++ b/src/comp/middle/typeck.rs
@@ -1469,7 +1469,8 @@ mod Pushdown {
             }
             case (none[@ast.expr]) {
                 Demand.simple(fcx, bloc.span, expected, plain_ty(ty.ty_nil));
-                ret bloc;
+                ret fold.respan[ast.block_](bloc.span,
+                      rec(a = boring_ann() with bloc.node));
             }
         }
     }
diff --git a/src/comp/middle/typestate_check.rs b/src/comp/middle/typestate_check.rs
index 7d7108ff82a..3e67cf2e109 100644
--- a/src/comp/middle/typestate_check.rs
+++ b/src/comp/middle/typestate_check.rs
@@ -1,12 +1,16 @@
 import front.ast;
 import front.ast.ann;
+import front.ast.method;
 import front.ast.ty;
 import front.ast.mutability;
 import front.ast.item;
 import front.ast.block;
 import front.ast.block_;
 import front.ast.block_index_entry;
+import front.ast.mod_index_entry;
+import front.ast.obj_field;
 import front.ast.decl;
+import front.ast.arm;
 import front.ast.stmt;
 import front.ast.stmt_;
 import front.ast.stmt_decl;
@@ -17,6 +21,7 @@ import front.ast.decl_item;
 import front.ast.ident;
 import front.ast.def_id;
 import front.ast.ann;
+import front.ast.field;
 import front.ast.expr;
 import front.ast.expr_call;
 import front.ast.expr_vec;
@@ -29,11 +34,33 @@ import front.ast.expr_block;
 import front.ast.expr_rec;
 import front.ast.expr_if;
 import front.ast.expr_binary;
+import front.ast.expr_unary;
 import front.ast.expr_assign;
+import front.ast.expr_assign_op;
 import front.ast.expr_while;
+import front.ast.expr_do_while;
+import front.ast.expr_alt;
 import front.ast.expr_lit;
 import front.ast.expr_ret;
+import front.ast.expr_self_method;
+import front.ast.expr_bind;
+import front.ast.expr_spawn;
+import front.ast.expr_ext;
+import front.ast.expr_fail;
+import front.ast.expr_break;
+import front.ast.expr_cont;
+import front.ast.expr_send;
+import front.ast.expr_recv;
+import front.ast.expr_put;
+import front.ast.expr_port;
+import front.ast.expr_chan;
+import front.ast.expr_be;
+import front.ast.expr_check_expr;
+import front.ast.expr_cast;
+import front.ast.expr_for;
+import front.ast.expr_for_each;
 import front.ast.path;
+import front.ast.elt;
 import front.ast.crate_directive;
 import front.ast.fn_decl;
 import front.ast._obj;
@@ -59,6 +86,7 @@ import front.ast.crate;
 import front.ast.mod_index_entry;
 import front.ast.mie_item;
 import front.ast.item_fn;
+import front.ast.item_obj;
 import front.ast.def_local;
 
 import middle.fold;
@@ -73,6 +101,8 @@ import util.common.uistr;
 import util.common.elt_exprs;
 import util.common.field_exprs;
 import util.common.log_expr;
+import util.common.log_stmt;
+import util.common.log_block;
 import util.typestate_ann;
 import util.typestate_ann.ts_ann;
 import util.typestate_ann.empty_pre_post;
@@ -102,6 +132,7 @@ import util.typestate_ann.empty_ann;
 import util.typestate_ann.extend_prestate;
 import util.typestate_ann.extend_poststate;
 import util.typestate_ann.intersect;
+import util.typestate_ann.pp_clone;
 
 import middle.ty;
 import middle.ty.ann_to_type;
@@ -124,11 +155,13 @@ import std._vec.pop;
 import std._vec.push;
 import std._vec.slice;
 import std._vec.unzip;
+import std._vec.plus_option;
 import std.option;
 import std.option.t;
 import std.option.some;
 import std.option.none;
 import std.option.from_maybe;
+import std.option.maybe;
 import std.option.is_none;
 import std.option.get;
 import std.map.hashmap;
@@ -151,24 +184,6 @@ import util.typestate_ann.require_and_preserve;
 
 /**** debugging junk  ****/
 
-fn log_stmt(stmt st) -> () {
-  let str_writer s = string_writer();
-  auto out_ = mkstate(s.get_writer(), 80u);
-  auto out = @rec(s=out_,
-                  comments=option.none[vec[front.lexer.cmnt]],
-                  mutable cur_cmnt=0u);
-  alt (st.node) {
-    case (ast.stmt_decl(?decl,_)) {
-      print_decl(out, decl);
-    }
-    case (ast.stmt_expr(?ex,_)) {
-      print_expr(out, ex);
-    }
-    case (_) { /* do nothing */ }
-  }
-  log(s.get_str());
-}
-
 fn log_bitv(fn_info enclosing, bitv.t v) {
   auto s = "";
 
@@ -222,12 +237,16 @@ fn print_idents(vec[ident] idents) -> () {
 type var_info     = tup(uint, ident);
 type fn_info      = std.map.hashmap[def_id, var_info];
 /* mapping from function name to fn_info map */
-type _fn_info_map = std.map.hashmap[def_id, fn_info];
+type fn_info_map = std.map.hashmap[def_id, fn_info];
  
 fn bit_num(def_id v, fn_info m) -> uint {
   check (m.contains_key(v));
   ret m.get(v)._0;
 }
+fn get_fn_info(fn_info_map fm, def_id did) -> fn_info {
+    check (fm.contains_key(did));
+    ret fm.get(did);
+}
 
 fn var_is_local(def_id v, fn_info m) -> bool {
   ret (m.contains_key(v));
@@ -254,6 +273,7 @@ fn find_locals(_fn f) -> vec[tup(ident,def_id)] {
 }
 
 fn add_var(def_id v, ident nm, uint next, fn_info tbl) -> uint {
+    log(nm + " |-> " + util.common.uistr(next));
   tbl.insert(v, tup(next,nm));
   ret (next + 1u);
 }
@@ -277,23 +297,42 @@ fn mk_fn_info(_fn f) -> fn_info {
   ret res;
 }
 
-/* extends mk_fn_info to an item, side-effecting the map fi from
+/* extends mk_fn_info to a function item, side-effecting the map fi from 
    function IDs to fn_info maps */
-fn mk_fn_info_item_fn(&_fn_info_map fi, &span sp, ident i, &ast._fn f,
+fn mk_fn_info_item_fn(&fn_info_map fi, &span sp, ident i, &ast._fn f,
                  vec[ast.ty_param] ty_params, def_id id, ann a) -> @item {
   fi.insert(id, mk_fn_info(f));
+  log(i + " has " + uistr(num_locals(mk_fn_info(f))) + " local vars");
   ret @respan(sp, item_fn(i, f, ty_params, id, a));
 }
 
+/* extends mk_fn_info to an obj item, side-effecting the map fi from 
+   function IDs to fn_info maps */
+fn mk_fn_info_item_obj(&fn_info_map fi, &span sp, ident i, &ast._obj o,
+     vec[ast.ty_param] ty_params, ast.obj_def_ids odid, ann a) -> @item {
+    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");
+    }
+    ret @respan(sp, item_obj(i, o, ty_params, odid, a));
+}
+
 /* initializes the global fn_info_map (mapping each function ID, including
    nested locally defined functions, onto a mapping from local variable name
    to bit number) */
-fn mk_f_to_fn_info(@ast.crate c) -> _fn_info_map {
+fn mk_f_to_fn_info(@ast.crate c) -> fn_info_map {
   auto res = new_def_hash[fn_info]();
 
-  auto fld = fold.new_identity_fold[_fn_info_map]();
-  fld = @rec(fold_item_fn = bind mk_fn_info_item_fn(_,_,_,_,_,_,_) with *fld);
-  fold.fold_crate[_fn_info_map](res, fld, c);
+  auto fld = fold.new_identity_fold[fn_info_map]();
+  fld = @rec(fold_item_fn  = bind mk_fn_info_item_fn(_,_,_,_,_,_,_),
+             fold_item_obj = bind mk_fn_info_item_obj(_,_,_,_,_,_,_)
+               with *fld);
+  fold.fold_crate[fn_info_map](res, fld, c);
 
   ret res;
 }
@@ -438,6 +477,10 @@ fn ann_to_ts_ann_fail_more(ann a) -> @ts_ann {
   }
 }
 
+fn ann_to_poststate(ann a) -> poststate {
+    ret (ann_to_ts_ann_fail_more(a)).states.poststate;
+}
+
 fn stmt_to_ann(&stmt s) -> option.t[@ts_ann] {
   alt (s.node) {
     case (stmt_decl(_,?a)) {
@@ -452,13 +495,6 @@ fn stmt_to_ann(&stmt s) -> option.t[@ts_ann] {
   }
 }
 
-/*
-/* fails if no annotation */
-fn stmt_pp(&stmt s) -> pre_and_post {
-  ret (stmt_ann(s)).conditions;
-}
-*/
-
 /* fails if e has no annotation */
 fn expr_states(&expr e) -> pre_and_post_state {
   alt (expr_ann(e)) {
@@ -501,6 +537,18 @@ fn expr_pp(&expr e) -> pre_and_post {
   }
 }
 
+fn stmt_pp(&stmt s) -> pre_and_post {
+    alt (stmt_to_ann(s)) {
+        case (none[@ts_ann]) {
+            log "stmt_pp: the impossible happened (no annotation)";
+            fail;
+        }
+        case (some[@ts_ann](?p)) {
+            ret p.conditions;
+        }
+    }
+}
+
 /* fails if b has no annotation */
 /* FIXME: factor out code in the following two functions (block_ts_ann) */
 fn block_pp(&block b) -> pre_and_post {
@@ -624,18 +672,19 @@ fn with_pp(ann a, pre_and_post p) -> ann {
 // precondition shouldn't include x.
 fn seq_preconds(uint num_vars, vec[pre_and_post] pps) -> precond {
   let uint sz = len[pre_and_post](pps);
-  check(sz >= 1u);
-  auto first   = pps.(0);
-
-  if (sz > 1u) {
+ 
+  if (sz >= 1u) {
+    auto first   = pps.(0);
     check (pps_len(first) == num_vars);
     let precond rest = seq_preconds(num_vars,
                          slice[pre_and_post](pps, 1u, sz));
     difference(rest, first.postcondition);
     union(first.precondition, rest);
+    ret first.precondition;
+  }
+  else {
+      ret true_precond(num_vars);
   }
-
-  ret (first.precondition);
 }
 
 /* works on either postconds or preconds
@@ -681,18 +730,48 @@ fn intersect_postconds(&vec[postcond] pcs) -> postcond {
 /******* AST-traversing code ********/
 
 fn find_pre_post_mod(&_mod m) -> _mod {
-  ret m; /* FIXME */
+    log("implement find_pre_post_mod!");
+    fail;
+}
+
+fn find_pre_post_state_mod(&_mod m) -> bool {
+    log("implement find_pre_post_state_mod!");
+    fail;
 }
 
 fn find_pre_post_native_mod(&native_mod m) -> native_mod {
-  ret m; /* FIXME */
-}
- 
-fn find_pre_post_obj(_obj o) -> _obj {
-  ret o; /* FIXME */
+    log("implement find_pre_post_native_mod");
+    fail;
 }
 
-fn find_pre_post_item(_fn_info_map fm, fn_info enclosing, &item i) -> () {
+fn find_pre_post_state_native_mod(&native_mod m) -> bool {
+    log("implement find_pre_post_state_native_mod!");
+    fail;
+}
+ 
+fn find_pre_post_obj(&fn_info_map fm, _obj o) -> () {
+    fn do_a_method(fn_info_map fm, &@method m) -> () {
+        check(fm.contains_key(m.node.id));
+        find_pre_post_fn(fm, fm.get(m.node.id), m.node.meth);
+    }
+    auto f = bind do_a_method(fm,_);
+    _vec.map[@method, ()](f, o.methods);
+    option.map[@method, ()](f, o.dtor);
+}
+
+fn find_pre_post_state_obj(fn_info_map fm, _obj o) -> bool {
+    fn do_a_method(fn_info_map fm, &@method m) -> bool {
+        check(fm.contains_key(m.node.id));
+        ret find_pre_post_state_fn(fm, fm.get(m.node.id), m.node.meth);
+    }
+    auto f = bind do_a_method(fm,_);
+    auto flags = _vec.map[@method, bool](f, o.methods);
+    auto changed = _vec.or(flags);
+    changed = changed || maybe[@method, bool](false, f, o.dtor);
+    ret changed;
+}
+
+fn find_pre_post_item(fn_info_map fm, fn_info enclosing, &item i) -> () {
   alt (i.node) {
     case (ast.item_const(?id, ?t, ?e, ?di, ?a)) {
         find_pre_post_expr(fm, enclosing, *e);
@@ -714,7 +793,7 @@ fn find_pre_post_item(_fn_info_map fm, fn_info enclosing, &item i) -> () {
       ret;
     }
     case (ast.item_obj(?id, ?o, ?ps, ?di, ?a)) {
-      find_pre_post_obj(o);
+        find_pre_post_obj(fm, o);
     }
   }
 }
@@ -723,9 +802,9 @@ fn find_pre_post_item(_fn_info_map fm, fn_info enclosing, &item i) -> () {
    sets the precondition in a to be the result of combining
    the preconditions for <args>, and the postcondition in a to 
    be the union of all postconditions for <args> */
-fn find_pre_post_exprs(&_fn_info_map fm, &fn_info enclosing,
+fn find_pre_post_exprs(&fn_info_map fm, &fn_info enclosing,
                        &vec[@expr] args, ann a) {
-    fn do_one(_fn_info_map fm, fn_info enclosing,
+    fn do_one(fn_info_map fm, fn_info enclosing,
               &@expr e) -> () {
         find_pre_post_expr(fm, enclosing, *e);
     }
@@ -747,16 +826,21 @@ fn find_pre_post_exprs(&_fn_info_map fm, &fn_info enclosing,
 }
 
 /* Fills in annotations as a side effect. Does not rebuild the expr */
-fn find_pre_post_expr(&_fn_info_map fm, &fn_info enclosing, &expr e) -> () {
+fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () {
     auto num_local_vars = num_locals(enclosing);
 
-    fn do_rand_(_fn_info_map fm, fn_info enclosing, &@expr e) -> () {
+    fn do_rand_(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);
     }
 
+    /*    log("find_pre_post_expr (num_locals =" +
+             uistr(num_local_vars) + "):");
+          log_expr(e);
+    */
+
     alt(e.node) {
         case(expr_call(?operator, ?operands, ?a)) {
             auto args = _vec.clone[@expr](operands);
@@ -866,6 +950,10 @@ 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_unary(_,?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);
@@ -881,8 +969,41 @@ fn find_pre_post_expr(&_fn_info_map fm, &fn_info enclosing, &expr e) -> () {
         case (expr_index(?e, ?sub, ?a)) {
             find_pre_post_exprs(fm, enclosing, vec(e, sub), a);
         }
+        case (expr_alt(?e, ?alts, ?a)) {
+            find_pre_post_expr(fm, enclosing, *e);
+            fn do_an_alt(fn_info_map fm, fn_info enc, &arm an_alt)
+                -> pre_and_post {
+                find_pre_post_block(fm, enc, an_alt.block);
+                ret block_pp(an_alt.block);
+            }
+            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,
+                          &pre_and_post next) -> pre_and_post {
+                union(pp.precondition, seq_preconds(num_local_vars,
+                                         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));
+        }
+        case (expr_field(?operator, _, ?a)) {
+            find_pre_post_expr(fm, enclosing, *operator);
+            set_pre_and_post(a, expr_pp(*operator));
+        }
+        case (expr_fail(?a)) {
+            set_pre_and_post(a,
+               rec(precondition=empty_prestate(num_local_vars),
+                   postcondition=true_postcond(num_local_vars)));
+        }
         case(_) {
             log("this sort of expr isn't implemented!");
+            log_expr(e);
             fail;
         }
     }
@@ -902,7 +1023,7 @@ fn gen_poststate(&fn_info enclosing, &ann a, def_id id) -> bool {
   ret set_in_poststate(i, (ann_to_ts_ann_fail_more(a)).states);
 }
 
-fn find_pre_post_stmt(_fn_info_map fm, &fn_info enclosing, &ast.stmt s)
+fn find_pre_post_stmt(fn_info_map fm, &fn_info enclosing, &ast.stmt s)
     -> () {
   auto num_local_vars = num_locals(enclosing);
   alt(s.node) {
@@ -941,27 +1062,49 @@ 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)
+fn find_pre_post_block(&fn_info_map fm, &fn_info enclosing, block b)
     -> () {
-    fn do_one_(_fn_info_map fm, fn_info i, &@stmt s) -> () {
+    fn do_one_(fn_info_map fm, fn_info i, &@stmt s) -> () {
         find_pre_post_stmt(fm, i, *s);
     }
     auto do_one = bind do_one_(fm, enclosing, _);
     
     _vec.map[@stmt, ()](do_one, b.node.stmts);
-    fn do_inner_(_fn_info_map fm, fn_info i, &@expr e) -> () {
+    fn do_inner_(fn_info_map fm, fn_info i, &@expr e) -> () {
         find_pre_post_expr(fm, i, *e);
     }
     auto do_inner = bind do_inner_(fm, enclosing, _);
     option.map[@expr, ()](do_inner, b.node.expr);
-    /* FIXME needs to set up the ann for b!!!!!!!!!!! */
+
+    let vec[pre_and_post] pps = vec();
+
+    fn get_pp_stmt(&@stmt s) -> pre_and_post {
+        ret stmt_pp(*s);
+    }
+    auto f = get_pp_stmt;
+    pps += _vec.map[@stmt, pre_and_post](f, b.node.stmts);
+    fn get_pp_expr(&@expr e) -> pre_and_post {
+        ret expr_pp(*e);
+    }
+    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 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);
+    set_pre_and_post(b.node.a, rec(precondition=block_precond,
+                                   postcondition=block_postcond));
 }
 
-fn find_pre_post_fn(&_fn_info_map fm, &fn_info fi, &_fn f) -> () {
+fn find_pre_post_fn(&fn_info_map fm, &fn_info fi, &_fn f) -> () {
     find_pre_post_block(fm, fi, f.body);
 }
 
-fn check_item_fn(&_fn_info_map fm, &span sp, ident i, &ast._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 {
 
   check (fm.contains_key(id));
@@ -970,10 +1113,33 @@ fn check_item_fn(&_fn_info_map fm, &span sp, ident i, &ast._fn f,
   ret @respan(sp, ast.item_fn(i, f, ty_params, id, a));
 }
 
-/* FIXME */
-fn find_pre_post_state_item(_fn_info_map fm, @item i) -> bool {
-  log("Implement find_pre_post_item!");
-  fail;
+fn find_pre_post_state_item(fn_info_map fm, fn_info enclosing, @item i)
+   -> bool {
+ alt (i.node) {
+    case (ast.item_const(?id, ?t, ?e, ?di, ?a)) {
+        ret find_pre_post_state_expr(fm, enclosing,
+              empty_prestate(num_locals(enclosing)), e);
+    }
+    case (ast.item_fn(?id, ?f, ?ps, ?di, ?a)) {
+      check (fm.contains_key(di));
+      ret find_pre_post_state_fn(fm, fm.get(di), f);
+    }
+    case (ast.item_mod(?id, ?m, ?di)) {
+      ret find_pre_post_state_mod(m);
+    }
+    case (ast.item_native_mod(?id, ?nm, ?di)) {
+      ret find_pre_post_state_native_mod(nm);
+    }
+    case (ast.item_ty(_,_,_,_,_)) {
+      ret false;
+    }
+    case (ast.item_tag(_,_,_,_,_)) {
+      ret false;
+    }
+    case (ast.item_obj(?id, ?o, ?ps, ?di, ?a)) {
+        ret find_pre_post_state_obj(fm, o);
+    }
+  }
 }
 
 fn set_prestate_ann(ann a, prestate pre) -> bool {
@@ -1034,6 +1200,11 @@ fn set_pre_and_post(&ann a, pre_and_post pp) -> () {
         case (ann_type(_,_,?ts_a)) {
             check (! is_none[@ts_ann](ts_a));
             auto t = *get[@ts_ann](ts_a);
+            /*  log("set_pre_and_post, old =");
+            log_pp(t.conditions);
+            log("new =");
+            log_pp(pp);
+            */
             set_precondition(t, pp.precondition);
             set_postcondition(t, pp.postcondition);
         }
@@ -1044,7 +1215,7 @@ fn set_pre_and_post(&ann a, pre_and_post pp) -> () {
     }
 }
 
-fn seq_states(&_fn_info_map fm, &fn_info enclosing,
+fn seq_states(&fn_info_map fm, &fn_info enclosing,
     prestate pres, vec[@expr] exprs) -> tup(bool, poststate) {
   auto changed = false;
   auto post = pres;
@@ -1057,7 +1228,7 @@ fn seq_states(&_fn_info_map fm, &fn_info enclosing,
   ret tup(changed, post);
 }
 
-fn find_pre_post_state_exprs(&_fn_info_map fm,
+fn find_pre_post_state_exprs(&fn_info_map fm,
                              &fn_info enclosing,
                              &prestate pres,
                              &ann a, &vec[@expr] es) -> bool {
@@ -1075,7 +1246,7 @@ fn pure_exp(&ann a, &prestate p) -> bool {
   ret changed;
 }
 
-fn find_pre_post_state_expr(&_fn_info_map fm, &fn_info enclosing,
+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);
@@ -1224,6 +1395,39 @@ fn find_pre_post_state_expr(&_fn_info_map fm, &fn_info enclosing,
         changed = extend_poststate_ann(a, expr_poststate(*sub));
         ret changed;
     }
+    case (expr_alt(?e, ?alts, ?a)) {
+        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;
+        }
+        ret changed;
+    }
+    case (expr_field(?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_unary(_,?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))
+          || changed;
+        ret changed;
+    }
     case (_) {
       log("find_pre_post_state_expr: implement this case!");
       fail;
@@ -1232,7 +1436,7 @@ fn find_pre_post_state_expr(&_fn_info_map fm, &fn_info enclosing,
 
 }
 
-fn find_pre_post_state_stmt(&_fn_info_map fm, &fn_info enclosing,
+fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing,
                             &prestate pres, @stmt s) -> bool {
   auto changed = false;
   auto stmt_ann_ = stmt_to_ann(*s);
@@ -1285,7 +1489,7 @@ 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, an_item);
+            be find_pre_post_state_item(fm, enclosing, an_item);
         }
       }
     }
@@ -1314,7 +1518,7 @@ 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,
+fn find_pre_post_state_block(&fn_info_map fm, &fn_info enclosing,
                              &prestate pres0, block b)
   -> bool {
 
@@ -1332,24 +1536,31 @@ fn find_pre_post_state_block(&_fn_info_map fm, &fn_info enclosing,
     pres = stmt_poststate(*s, num_local_vars);
   }
 
+  auto post = pres;
+
   alt (b.node.expr) {
     case (none[@expr]) {}
     case (some[@expr](?e)) {
       changed = find_pre_post_state_expr(fm, enclosing, pres, e) || changed;
+      post = expr_poststate(*e);
     }
   }
+  set_prestate_ann(b.node.a, pres0);
+  set_poststate_ann(b.node.a, post);
   ret changed;
 }
 
-fn find_pre_post_state_fn(&_fn_info_map f_info, &fn_info fi, &ast._fn f)
+fn find_pre_post_state_fn(&fn_info_map f_info, &fn_info fi, &ast._fn f)
   -> bool {
+    /* FIXME: where do we set args as being initialized?
+       What about for methods? */
     auto num_local_vars = num_locals(fi);
     ret find_pre_post_state_block(f_info, fi,
                                   empty_prestate(num_local_vars), f.body);
 }
 
-fn fixed_point_states(_fn_info_map fm, fn_info f_info,
-                      fn (&_fn_info_map, &fn_info, &ast._fn) -> bool f,
+fn fixed_point_states(fn_info_map fm, fn_info f_info,
+                      fn (&fn_info_map, &fn_info, &ast._fn) -> bool f,
                       &ast._fn start) -> () {
 
   auto changed = f(fm, f_info, start);
@@ -1368,7 +1579,7 @@ fn check_states_expr(fn_info enclosing, &expr e) -> () {
   let prestate pres   = expr_prestate(e);
 
   if (!implies(pres, prec)) {
-      log("check_states_stmt: unsatisfied precondition for ");
+      log("check_states_expr: unsatisfied precondition for ");
       log_expr(e);
       log("Precondition: ");
       log_bitv(enclosing, prec);
@@ -1424,14 +1635,8 @@ fn check_states_against_conditions(fn_info enclosing, &ast._fn f) -> () {
   
 }
 
-fn check_item_fn_state(&_fn_info_map f_info_map, &span sp, ident i,
-                       &ast._fn f, vec[ast.ty_param] ty_params, def_id id,
-                       ann a) -> @item {
-
-  /* Look up the var-to-bit-num map for this function */
-  check(f_info_map.contains_key(id));
-  auto f_info = f_info_map.get(id);
-
+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);
@@ -1439,11 +1644,39 @@ fn check_item_fn_state(&_fn_info_map f_info_map, &span sp, ident i,
   /* Now compare each expr's pre-state to its precondition
      and post-state to its postcondition */
   check_states_against_conditions(f_info, f);
+}
+
+fn check_item_fn_state(&fn_info_map f_info_map, &span sp, ident i,
+                       &ast._fn f, vec[ast.ty_param] ty_params, def_id id,
+                       ann a) -> @item {
+
+  /* Look up the var-to-bit-num map for this function */
+  check(f_info_map.contains_key(id));
+  auto f_info = f_info_map.get(id);
+
+  check_fn_states(f_info_map, f_info, f);
 
   /* Rebuild the same function */
   ret @respan(sp, ast.item_fn(i, f, ty_params, id, a));
 }
 
+fn check_method_states(&fn_info_map f_info_map, @method m) -> () {
+    check (f_info_map.contains_key(m.node.id));
+    auto f_info = f_info_map.get(m.node.id);
+    check_fn_states(f_info_map, f_info, m.node.meth);
+}
+
+fn check_obj_state(&fn_info_map f_info_map, vec[obj_field] fields,
+                  vec[@method] methods, option.t[@method] dtor) -> ast._obj {
+    fn one(fn_info_map fm, &@method m) -> () {
+        ret check_method_states(fm, m);
+    }
+    auto f = bind one(f_info_map,_);
+    _vec.map[@method, ()](f, methods);
+    option.map[@method, ()](f, dtor);
+    ret rec(fields=fields, methods=methods, dtor=dtor);
+}
+
 fn init_ann(&fn_info fi, ann a) -> ann {
     alt (a) {
         case (ann_none) {
@@ -1456,42 +1689,467 @@ fn init_ann(&fn_info fi, ann a) -> ann {
     }
 }
 
-fn item_fn_anns(&_fn_info_map fm, &span sp, ident i, &ast._fn f,
+fn init_blank_ann(&() ignore, ann a) -> ann {
+    alt (a) {
+        case (ann_none) {
+            log("init_ann: shouldn't see ann_none");
+            fail;
+        }
+        case (ann_type(?t,?ps,_)) {
+            ret ann_type(t, ps, some[@ts_ann](@empty_ann(0u)));
+        }
+    }
+}
+
+fn init_block(&fn_info fi, &span sp, &block_ b) -> block {
+    log("init_block:");
+    log_block(respan(sp, b));
+    alt(b.a) {
+        case (ann_none) {
+            log("init_ann: shouldn't see ann_none");
+            fail;
+        }
+        case (ann_type(?t,?ps,_)) {
+            auto fld0 = fold.new_identity_fold[fn_info]();
+
+            fld0 = @rec(fold_ann = bind init_ann(_,_) with *fld0);
+            ret fold.fold_block[fn_info](fi, fld0, respan(sp, b)); 
+        }
+    }
+    
+}
+
+fn item_fn_anns(&fn_info_map fm, &span sp, ident i, &ast._fn f,
                 vec[ast.ty_param] ty_params, def_id id, ann a) -> @item {
 
     check(fm.contains_key(id));
     auto f_info = fm.get(id);
 
+    log(i + " has " + uistr(num_locals(f_info)) + " local vars");
+
     auto fld0 = fold.new_identity_fold[fn_info]();
 
-    fld0 = @rec(fold_ann = bind init_ann(_,_) with *fld0);
+    fld0 = @rec(fold_ann = bind init_ann(_,_) 
+                //   fold_block = bind init_block(_,_,_)
+                    with *fld0);
 
     ret fold.fold_item[fn_info]
            (f_info, fld0, @respan(sp, item_fn(i, f, ty_params, id, a))); 
 }
 
-fn check_crate(@ast.crate crate) -> @ast.crate {
+/* This is painstakingly written as an explicit recursion b/c the
+   standard ast.fold doesn't traverse in the correct order:
+   consider
+   fn foo() {
+      fn bar() {
+        auto x = 5;
+        log(x);
+      }
+   }
+   With fold, first bar() would be processed and its subexps would
+   correctly be annotated with length-1 bit vectors.
+   But then, the process would be repeated with (fn bar()...) as
+   a subexp of foo, which has 0 local variables -- so then
+   the body of bar() would be incorrectly annotated with length-0 bit
+   vectors. */
+fn annotate_exprs(&fn_info_map fm, &vec[@expr] es) -> vec[@expr] {
+    fn one(fn_info_map fm, &@expr e) -> @expr {
+        ret annotate_expr(fm, e);
+    }
+    auto f = bind one(fm,_);
+    ret _vec.map[@expr, @expr](f, es);
+}
+fn annotate_elts(&fn_info_map fm, &vec[elt] es) -> vec[elt] {
+    fn one(fn_info_map fm, &elt e) -> elt {
+        ret rec(mut=e.mut,
+                expr=annotate_expr(fm, e.expr));
+    }
+    auto f = bind one(fm,_);
+    ret _vec.map[elt, elt](f, es);
+}
+fn annotate_fields(&fn_info_map fm, &vec[field] fs) -> vec[field] {
+    fn one(fn_info_map fm, &field f) -> field {
+        ret rec(mut=f.mut,
+                 ident=f.ident,
+                 expr=annotate_expr(fm, f.expr));
+    }
+    auto f = bind one(fm,_);
+    ret _vec.map[field, field](f, fs);
+}
+fn annotate_option_exp(&fn_info_map fm, &option.t[@expr] o)
+  -> option.t[@expr] {
+    fn one(fn_info_map fm, &@expr e) -> @expr {
+        ret annotate_expr(fm, e);
+    }
+    auto f = bind one(fm,_);
+    ret option.map[@expr, @expr](f, o);
+}
+fn annotate_option_exprs(&fn_info_map fm, &vec[option.t[@expr]] es)
+  -> vec[option.t[@expr]] {
+    fn one(fn_info_map fm, &option.t[@expr] o) -> option.t[@expr] {
+        ret annotate_option_exp(fm, o);
+    }
+    auto f = bind one(fm,_);
+    ret _vec.map[option.t[@expr], option.t[@expr]](f, es);
+}
+fn annotate_decl(&fn_info_map fm, &@decl d) -> @decl {
+    auto d1 = d.node;
+    alt (d.node) {
+        case (decl_local(?l)) {
+            alt(l.init) {
+                case (some[initializer](?init)) {
+                    let option.t[initializer] an_i =
+                        some[initializer]
+                          (rec(expr=annotate_expr(fm, init.expr)
+                                 with init));
+                    let @local new_l = @rec(init=an_i with *l);
+                    d1 = decl_local(new_l);
+                }
+                case (_) { /* do nothing */ }
+            }
+        }
+        case (decl_item(?item)) {
+            d1 = decl_item(annotate_item(fm, item));
+        }
+    }
+    ret @respan(d.span, d1);
+}
+fn annotate_alts(&fn_info_map fm, &vec[arm] alts) -> vec[arm] {
+    fn one(fn_info_map fm, &arm a) -> arm {
+        ret rec(pat=a.pat,
+                 block=annotate_block(fm, a.block),
+                 index=a.index);
+    }
+    auto f = bind one(fm,_);
+    ret _vec.map[arm, arm](f, alts);
 
+}
+fn annotate_expr(&fn_info_map fm, &@expr e) -> @expr {
+    auto e1 = e.node;
+    alt (e.node) {
+        case (expr_vec(?es, ?m, ?a)) {
+            e1 = expr_vec(annotate_exprs(fm, es), m, a);
+        }
+        case (expr_tup(?es, ?a)) {
+            e1 = expr_tup(annotate_elts(fm, es), a);
+        }
+        case (expr_rec(?fs, ?maybe_e, ?a)) {
+            e1 = expr_rec(annotate_fields(fm, fs),
+                          annotate_option_exp(fm, maybe_e), a);
+        }
+        case (expr_call(?e, ?es, ?a)) {
+            e1 = expr_call(annotate_expr(fm, e),
+                          annotate_exprs(fm, es), a);
+        }
+        case (expr_self_method(_,_)) {
+            // no change
+        }
+        case (expr_bind(?e, ?maybe_es, ?a)) {
+            e1 = expr_bind(annotate_expr(fm, e),
+                           annotate_option_exprs(fm, maybe_es),
+                           a);
+        }
+        case (expr_spawn(?s, ?maybe_s, ?e, ?es, ?a)) {
+            e1 = expr_spawn(s, maybe_s, annotate_expr(fm, e),
+                            annotate_exprs(fm, es), a);
+        }
+        case (expr_binary(?bop, ?w, ?x, ?a)) {
+            e1 = expr_binary(bop, annotate_expr(fm, w),
+                             annotate_expr(fm, x), a);
+        }
+        case (expr_unary(?uop, ?w, ?a)) {
+            e1 = expr_unary(uop, annotate_expr(fm, w), a);
+        }
+        case (expr_lit(_,_)) {
+            /* no change */
+        }
+        case (expr_cast(?e,?t,?a)) {
+            e1 = expr_cast(annotate_expr(fm, e), t, a);
+        }
+        case (expr_if(?e, ?b, ?maybe_e, ?a)) {
+            e1 = expr_if(annotate_expr(fm, e),
+                         annotate_block(fm, b),
+                         annotate_option_exp(fm, maybe_e), a);
+        }
+        case (expr_while(?e, ?b, ?a)) {
+            e1 = expr_while(annotate_expr(fm, e),
+                            annotate_block(fm, b), a);
+        }
+        case (expr_for(?d, ?e, ?b, ?a)) {
+            e1 = expr_for(annotate_decl(fm, d),
+                          annotate_expr(fm, e),
+                          annotate_block(fm, b), a);
+        }
+        case (expr_for_each(?d, ?e, ?b, ?a)) {
+            e1 = expr_for_each(annotate_decl(fm, d),
+                          annotate_expr(fm, e),
+                          annotate_block(fm, b), a);
+        }
+        case (expr_do_while(?b, ?e, ?a)) {
+            e1 = expr_do_while(annotate_block(fm, b),
+                               annotate_expr(fm, e), a);
+        }
+        case (expr_alt(?e, ?alts, ?a)) {
+            e1 = expr_alt(annotate_expr(fm, e),
+                          annotate_alts(fm, alts), a);
+        }
+        case (expr_block(?b, ?a)) {
+            e1 = expr_block(annotate_block(fm, b), a);
+        }
+        case (expr_assign(?l, ?r, ?a)) {
+            e1 = expr_assign(annotate_expr(fm, l), annotate_expr(fm, r), a);
+        }
+        case (expr_assign_op(?bop, ?l, ?r, ?a)) {
+            e1 = expr_assign_op(bop,
+               annotate_expr(fm, l), annotate_expr(fm, r), a);
+        }
+        case (expr_send(?l, ?r, ?a)) {
+            e1 = expr_send(annotate_expr(fm, l),
+                           annotate_expr(fm, r), a);
+        }
+        case (expr_recv(?l, ?r, ?a)) {
+           e1 = expr_recv(annotate_expr(fm, l),
+                           annotate_expr(fm, r), a);
+        }
+        case (expr_field(?e, ?i, ?a)) {
+            e1 = expr_field(annotate_expr(fm, e),
+                            i, a);
+        }
+        case (expr_index(?e, ?sub, ?a)) {
+            e1 = expr_index(annotate_expr(fm, e),
+                            annotate_expr(fm, sub), a);
+        }
+        case (expr_path(_,_,_)) {
+            /* no change */
+        }
+        case (expr_ext(?p, ?es, ?e_opt, ?e, ?a)) {
+            e1 = expr_ext(p, annotate_exprs(fm, es),
+                          annotate_option_exp(fm, e_opt),
+                          annotate_expr(fm, e), a);
+        }
+        /* no change, next 3 cases */
+        case (expr_fail(_)) { }
+        case (expr_break(_)) { }
+        case (expr_cont(_)) { }
+        case (expr_ret(?maybe_e, ?a)) {
+            e1 = expr_ret(annotate_option_exp(fm, maybe_e), a);
+        }
+        case (expr_put(?maybe_e, ?a)) {
+            e1 = expr_put(annotate_option_exp(fm, maybe_e), a);
+        }
+        case (expr_be(?e, ?a)) {
+            e1 = expr_be(annotate_expr(fm, e), a);
+        }
+        case (expr_log(?n, ?e, ?a)) {
+            e1 = expr_log(n, annotate_expr(fm, e), a);
+        }
+        case (expr_check_expr(?e, ?a)) {
+            e1 = expr_check_expr(annotate_expr(fm, e), a);
+        }
+        case (expr_port(_)) { /* no change */ }
+        case (expr_chan(?e, ?a)) {
+            e1 = expr_chan(annotate_expr(fm, e), a);
+        }
+    }
+    ret @respan(e.span, e1);
+}
+
+fn annotate_stmt(&fn_info_map fm, &@stmt s) -> @stmt {
+    alt (s.node) {
+        case (stmt_decl(?d, ?a)) {
+            ret @respan(s.span, stmt_decl(annotate_decl(fm, d), a));
+        }
+        case (stmt_expr(?e, ?a)) {
+            ret @respan(s.span, stmt_expr(annotate_expr(fm, e), a));
+        }
+    }
+}
+fn annotate_block(&fn_info_map fm, &block b) -> block {
+    let vec[@stmt] new_stmts = vec();
+    auto new_index = new_str_hash[block_index_entry]();
+
+    for (@stmt s in b.node.stmts) {
+        auto new_s = annotate_stmt(fm, s);
+        _vec.push[@stmt](new_stmts, new_s);
+        ast.index_stmt(new_index, new_s);
+    }
+    fn ann_e(fn_info_map fm, &@expr e) -> @expr {
+        ret annotate_expr(fm, e);
+    }
+    auto f = bind ann_e(fm,_);
+
+    auto new_e = option.map[@expr, @expr](f, b.node.expr);
+
+    ret respan(b.span,
+          rec(stmts=new_stmts, expr=new_e, index=new_index with b.node));
+}
+fn annotate_fn(&fn_info_map fm, &ast._fn f) -> ast._fn {
+    // subexps have *already* been annotated based on
+    // f's number-of-locals
+    ret rec(body=annotate_block(fm, f.body) with f);
+}
+fn annotate_mod(&fn_info_map fm, &ast._mod m) -> ast._mod {
+    let vec[@item] new_items = vec();
+    auto new_index = new_str_hash[mod_index_entry]();
+
+    for (@item i in m.items) {
+        auto new_i = annotate_item(fm, i);
+        _vec.push[@item](new_items, new_i);
+        ast.index_item(new_index, new_i);
+    }
+    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]();
+    fld0 = @rec(fold_ann = bind init_ann(_,_) 
+                with *fld0);
+    auto outer = fold.fold_method[fn_info](f_info, fld0, m);
+    auto new_fn = annotate_fn(fm, outer.node.meth);
+    ret @respan(m.span,
+                rec(meth=new_fn with m.node));
+}
+
+fn annotate_obj(&fn_info_map fm, &ast._obj o) -> ast._obj {
+    fn one(fn_info_map fm, &@method m) -> @method {
+        ret annotate_method(fm, m);
+    }
+    auto f = bind one(fm,_);
+    auto new_methods = _vec.map[@method, @method](f, o.methods);
+    auto new_dtor    = option.map[@method, @method](f, o.dtor);
+    ret rec(methods=new_methods, dtor=new_dtor with o);
+}
+
+ 
+// Only annotates the components of the item recursively.
+fn annotate_item_inner(&fn_info_map fm, &@ast.item item) -> @ast.item {
+    alt (item.node) {
+        /* FIXME can't skip this case -- exprs contain blocks contain stmts,
+         which contain decls */
+        case (ast.item_const(_,_,_,_,_)) {
+            // this has already been annotated by annotate_item
+            ret item;
+        }
+        case (ast.item_fn(?ident, ?ff, ?tps, ?id, ?ann)) {
+            ret @respan(item.span,
+                       ast.item_fn(ident, annotate_fn(fm, ff), tps, id, ann));
+        }
+        case (ast.item_mod(?ident, ?mm, ?id)) {
+            ret @respan(item.span,
+                       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));
+        }
+        case (ast.item_ty(_,_,_,_,_)) {
+            ret item;
+        }
+        case (ast.item_tag(_,_,_,_,_)) {
+            ret item;
+        }
+        case (ast.item_obj(?ident, ?ob, ?tps, ?odid, ?ann)) {
+            ret @respan(item.span,
+              ast.item_obj(ident, annotate_obj(fm, ob), tps, odid, ann));
+        }
+    } 
+}
+
+fn annotate_item(&fn_info_map fm, &@ast.item item) -> @ast.item {
+    // Using a fold, recursively set all anns in this item
+    // to be blank.
+    // *Then*, call annotate_item recursively to do the right
+    // thing for any nested items inside this one.
+    
+    alt (item.node) {
+        case (ast.item_const(_,_,_,_,_)) {
+            auto fld0 = fold.new_identity_fold[()]();
+            fld0 = @rec(fold_ann = bind init_blank_ann(_,_) 
+                        with *fld0);
+            ret fold.fold_item[()]((), fld0, item);
+        }
+        case (ast.item_fn(?i,?ff,?tps,?id,?ann)) {
+            auto f_info = get_fn_info(fm, id);
+            auto fld0 = fold.new_identity_fold[fn_info]();
+            fld0 = @rec(fold_ann = bind init_ann(_,_) 
+                        with *fld0);
+            auto outer = fold.fold_item[fn_info](f_info, fld0, item);
+            // now recurse into any nested items
+            ret annotate_item_inner(fm, outer);
+         }
+        case (ast.item_mod(?i, ?mm, ?id)) {
+            auto fld0 = fold.new_identity_fold[()]();
+            fld0 = @rec(fold_ann = bind init_blank_ann(_,_) 
+                        with *fld0);
+            auto outer = fold.fold_item[()]((), fld0, item);
+            ret annotate_item_inner(fm, outer);
+        }
+        case (ast.item_ty(_,_,_,_,_)) {
+            ret item;
+        }
+        case (ast.item_tag(_,_,_,_,_)) {
+            ret item;
+        }
+        case (ast.item_obj(?i,?ob,?tps,?odid,?ann)) {
+            auto fld0 = fold.new_identity_fold[()]();
+            fld0 = @rec(fold_ann = bind init_blank_ann(_,_) 
+                        with *fld0);
+            auto outer = fold.fold_item[()]((), fld0, item);
+            ret annotate_item_inner(fm, outer);
+        }
+    }
+}
+
+fn annotate_module(&fn_info_map fm, &ast._mod module) -> ast._mod {
+    let vec[@item] new_items = vec();
+    auto new_index = new_str_hash[ast.mod_index_entry]();
+
+    for (@item i in module.items) {
+        auto new_item = annotate_item(fm, i);
+        _vec.push[@item](new_items, new_item);
+        ast.index_item(new_index, new_item);
+    }
+
+    ret rec(items = new_items, index = new_index with module);
+}
+
+fn annotate_crate(&fn_info_map fm, &@ast.crate crate) -> @ast.crate {
+    ret @respan(crate.span,
+               rec(module = annotate_module(fm, crate.node.module)
+                   with crate.node));
+}
+
+fn check_crate(@ast.crate crate) -> @ast.crate {
   /* Build the global map from function id to var-to-bit-num-map */
-  auto fn_info_map = mk_f_to_fn_info(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 = fold.fold_crate[_fn_info_map](fn_info_map, fld0, crate);
+  /*
+  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]();
+  auto fld = fold.new_identity_fold[fn_info_map]();
   fld = @rec(fold_item_fn = bind check_item_fn(_,_,_,_,_,_,_) with *fld);
-  auto with_pre_postconditions = fold.fold_crate[_fn_info_map]
-    (fn_info_map, fld, with_anns);
+  auto with_pre_postconditions = fold.fold_crate[fn_info_map]
+    (fm, fld, with_anns);
 
-  auto fld1 = fold.new_identity_fold[_fn_info_map]();
+  auto fld1 = fold.new_identity_fold[fn_info_map]();
 
-  fld1 = @rec(fold_item_fn = bind check_item_fn_state(_,_,_,_,_,_,_)
+  fld1 = @rec(fold_item_fn = bind check_item_fn_state(_,_,_,_,_,_,_),
+              fold_obj     = bind check_obj_state(_,_,_,_)
               with *fld1);
 
-  ret fold.fold_crate[_fn_info_map](fn_info_map, fld1,
+  ret fold.fold_crate[fn_info_map](fm, fld1,
                                     with_pre_postconditions);
 }
 
diff --git a/src/comp/pretty/pprust.rs b/src/comp/pretty/pprust.rs
index cf606d9e6f1..e49ed34e948 100644
--- a/src/comp/pretty/pprust.rs
+++ b/src/comp/pretty/pprust.rs
@@ -475,6 +475,13 @@ fn print_expr(ps s, &@ast.expr expr) {
             commasep[option.t[@ast.expr]](s, args, f);
             pclose(s);
         }
+    case (ast.expr_spawn(_,_,?e,?es,_)) {
+          wrd1(s, "spawn");
+          print_expr(s, e);
+          popen(s);
+          commasep_exprs(s, es);
+          pclose(s);
+        }
         case (ast.expr_binary(?op,?lhs,?rhs,_)) {
             auto prec = operator_prec(op);
             print_maybe_parens(s, lhs, prec);
@@ -1018,3 +1025,13 @@ fn print_comment(ps s, lexer.cmnt_ cmnt) {
         }
     }
 }
+//
+// Local Variables:
+// mode: rust
+// fill-column: 78;
+// indent-tabs-mode: nil
+// c-basic-offset: 4
+// buffer-file-coding-system: utf-8-unix
+// compile-command: "make -k -C $RBUILD 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
+// End:
+//
diff --git a/src/comp/util/common.rs b/src/comp/util/common.rs
index 006bccb0683..af000cb6d0a 100644
--- a/src/comp/util/common.rs
+++ b/src/comp/util/common.rs
@@ -137,6 +137,35 @@ fn log_block(&ast.block b) -> () {
   log(s.get_str());
 }
 
+fn log_ann(&ast.ann a) -> () {
+    alt (a) {
+        case (ast.ann_none) {
+            log("ann_none");
+        }
+        case (ast.ann_type(_,_,_)) {
+            log("ann_type");
+        }
+    }
+}
+
+fn log_stmt(ast.stmt st) -> () {
+  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);
+  alt (st.node) {
+    case (ast.stmt_decl(?decl,_)) {
+      print_decl(out, decl);
+    }
+    case (ast.stmt_expr(?ex,_)) {
+      print_expr(out, ex);
+    }
+    case (_) { /* do nothing */ }
+  }
+  log(s.get_str());
+}
+
 //
 // Local Variables:
 // mode: rust
diff --git a/src/comp/util/typestate_ann.rs b/src/comp/util/typestate_ann.rs
index b1f12ffbc87..9ad6e01e8dd 100644
--- a/src/comp/util/typestate_ann.rs
+++ b/src/comp/util/typestate_ann.rs
@@ -147,6 +147,11 @@ fn ann_prestate(&ts_ann a) -> prestate {
   ret a.states.prestate;
 }
 
+fn pp_clone(&pre_and_post p) -> pre_and_post {
+  ret rec(precondition=bitv.clone(p.precondition),
+          postcondition=bitv.clone(p.postcondition));
+}
+
 // returns true if a implies b
 // that is, returns true except if for some bits c and d,
 // c = 1 and d = 0
@@ -155,3 +160,14 @@ fn implies(bitv.t a, bitv.t b) -> bool {
   bitv.difference(tmp, a);
   ret bitv.is_false(tmp);
 }
+
+//
+// Local Variables:
+// mode: rust
+// fill-column: 78;
+// indent-tabs-mode: nil
+// c-basic-offset: 4
+// buffer-file-coding-system: utf-8-unix
+// compile-command: "make -k -C $RBUILD 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
+// End:
+//
diff --git a/src/lib/_vec.rs b/src/lib/_vec.rs
index 6fc1d700886..cc8fabcaf16 100644
--- a/src/lib/_vec.rs
+++ b/src/lib/_vec.rs
@@ -266,7 +266,7 @@ fn unzip[T, U](&vec[tup(T, U)] v) -> tup(vec[T], vec[U]) {
 
 fn or(&vec[bool] v) -> bool {
     auto f = orb;
-    be _vec.foldl[bool, bool](f, false, v);
+    ret _vec.foldl[bool, bool](f, false, v);
 }
 
 fn clone[T](&vec[T] v) -> vec[T] {
diff --git a/src/lib/option.rs b/src/lib/option.rs
index 66a41bcac68..e214c77487f 100644
--- a/src/lib/option.rs
+++ b/src/lib/option.rs
@@ -39,12 +39,16 @@ fn is_none[T](&t[T] opt) -> bool {
 }
 
 fn from_maybe[T](&T def, &t[T] opt) -> T {
-    alt(opt) {
-        case (none[T])     { ret def; }
-        case (some[T](?t)) { ret t; }
-    }
+    auto f = bind util.id[T](_);
+    ret maybe[T, T](def, f, opt);
 }
 
+fn maybe[T, U](&U def, fn(&T) -> U f, &t[T] opt) -> U {
+    alt (opt) {
+        case (none[T]) { ret def; }
+        case (some[T](?t)) { ret f(t); }
+    }
+}
 // Local Variables:
 // mode: rust;
 // fill-column: 78;
diff --git a/src/test/compile-fail/use-uninit-dtor.rs b/src/test/compile-fail/use-uninit-dtor.rs
new file mode 100644
index 00000000000..be2f1727a6f
--- /dev/null
+++ b/src/test/compile-fail/use-uninit-dtor.rs
@@ -0,0 +1,12 @@
+// xfail-stage0
+// error-pattern:Unsatisfied precondition
+
+fn main() {
+ state obj foo(int x) {
+        drop {
+          let int baz;
+          log(baz);
+        }
+ }
+ fail;
+}