Rewrite tstate.annotate to use walk instead of fold

and various other tidying in typestate

8 files changed, 620 insertions, 883 deletions

diff --git a/src/comp/middle/tstate/ann.rs b/src/comp/middle/tstate/ann.rs
index 3e8c8e34a58..a62829f3a10 100644
--- a/src/comp/middle/tstate/ann.rs
+++ b/src/comp/middle/tstate/ann.rs
@@ -20,13 +20,13 @@ type poststate = bitv::t; /* 1 means "this variable is definitely initialized"
                             initialized" */
 
 /* named thus so as not to confuse with prestate and poststate */
-type pre_and_post = rec(precond precondition, postcond postcondition);
+type pre_and_post = @rec(precond precondition, postcond postcondition);
 /* FIXME: once it's implemented: */
 //  : ((*.precondition).nbits == (*.postcondition).nbits);
 
 type pre_and_post_state = rec(prestate prestate, poststate poststate);
 
-type ts_ann = rec(pre_and_post conditions, pre_and_post_state states);
+type ts_ann = @rec(pre_and_post conditions, pre_and_post_state states);
 
 fn true_precond(uint num_vars) -> precond {
   be bitv::create(num_vars, false);
@@ -49,18 +49,18 @@ fn false_postcond(uint num_vars) -> postcond {
 }
 
 fn empty_pre_post(uint num_vars) -> pre_and_post {
-  ret(rec(precondition=empty_prestate(num_vars),
-          postcondition=empty_poststate(num_vars)));
+  ret(@rec(precondition=empty_prestate(num_vars),
+           postcondition=empty_poststate(num_vars)));
 }
 
 fn empty_states(uint num_vars) -> pre_and_post_state {
   ret(rec(prestate=true_precond(num_vars),
-           poststate=true_postcond(num_vars)));
+          poststate=true_postcond(num_vars)));
 }
 
 fn empty_ann(uint num_vars) -> ts_ann {
-  ret(rec(conditions=empty_pre_post(num_vars),
-          states=empty_states(num_vars)));
+  ret(@rec(conditions=empty_pre_post(num_vars),
+           states=empty_states(num_vars)));
 }
 
 fn get_pre(&pre_and_post p) -> precond {
@@ -111,25 +111,25 @@ fn set_in_poststate(uint i, &pre_and_post_state s) -> bool {
 
 // Sets all the bits in a's precondition to equal the
 // corresponding bit in p's precondition.
-fn set_precondition(@ts_ann a, &precond p) -> () {
+fn set_precondition(ts_ann a, &precond p) -> () {
   bitv::copy(a.conditions.precondition, p);
 }
 
 // Sets all the bits in a's postcondition to equal the
 // corresponding bit in p's postcondition.
-fn set_postcondition(@ts_ann a, &postcond p) -> () {
+fn set_postcondition(ts_ann a, &postcond p) -> () {
   bitv::copy(a.conditions.postcondition, 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);
 }
 
 // Sets all the bits in a's postcondition to equal the
 // corresponding bit in p's postcondition.
-fn set_poststate(@ts_ann a, &poststate p) -> bool {
+fn set_poststate(ts_ann a, &poststate p) -> bool {
   ret bitv::copy(a.states.poststate, p);
 }
 
@@ -150,6 +150,16 @@ fn relax_prestate(uint i, &prestate p) -> bool {
     ret was_set;
 }
 
+// Clears all the bits in p
+fn clear(&precond p) -> () {
+    bitv::clear(p);
+}
+
+// Sets all the bits in p
+fn set(&precond p) -> () {
+    bitv::set_all(p);
+}
+
 fn ann_precond(&ts_ann a) -> precond {
   ret a.conditions.precondition;
 }
@@ -163,8 +173,8 @@ fn ann_poststate(&ts_ann a) -> poststate {
 }
 
 fn pp_clone(&pre_and_post p) -> pre_and_post {
-  ret rec(precondition=clone(p.precondition),
-          postcondition=clone(p.postcondition));
+  ret @rec(precondition=clone(p.precondition),
+           postcondition=clone(p.postcondition));
 }
 
 fn clone(prestate p) -> prestate {
diff --git a/src/comp/middle/tstate/annotate.rs b/src/comp/middle/tstate/annotate.rs
index 92e6accdbec..f1269303864 100644
--- a/src/comp/middle/tstate/annotate.rs
+++ b/src/comp/middle/tstate/annotate.rs
@@ -4,7 +4,6 @@ import std::option::some;
 import std::option::none;
 
 import front::ast;
-
 import front::ast::ident;
 import front::ast::def_id;
 import front::ast::ann;
@@ -76,417 +75,104 @@ import front::ast::method;
 
 import middle::fold;
 import middle::fold::respan;
-import middle::fold::new_identity_fold;
-import middle::fold::fold_crate;
-import middle::fold::fold_item;
-import middle::fold::fold_method;
+import middle::ty::expr_ann;
 
 import util::common::uistr;
 import util::common::span;
 import util::common::new_str_hash;
+import util::common::log_expr_err;
+import util::common::log_block_err;
+import util::common::log_item_err;
+import util::common::log_stmt_err;
+import util::common::log_expr;
+import util::common::log_block;
+import util::common::log_stmt;
 
 import middle::tstate::aux::fn_info;
 import middle::tstate::aux::fn_info_map;
 import middle::tstate::aux::num_locals;
-import middle::tstate::aux::init_ann;
-import middle::tstate::aux::init_blank_ann;
 import middle::tstate::aux::get_fn_info;
+import middle::tstate::aux::crate_ctxt;
+import middle::tstate::ann::empty_ann;
 
-fn item_fn_anns(&fn_info_map fm, &span sp, ident i, &_fn f,
-                vec[ty_param] ty_params, def_id id, ann a) -> @item {
-
-    assert (fm.contains_key(id));
-    auto f_info = fm.get(id);
-
-    log(i + " has " + uistr(num_locals(f_info)) + " local vars");
-
-    auto fld0 = new_identity_fold[fn_info]();
-
-    fld0 = @rec(fold_ann = bind init_ann(_,_) 
-                    with *fld0);
-
-    ret fold_item[fn_info]
-           (f_info, fld0, @respan(sp, item_fn(i, f, ty_params, id, a))); 
-}
-
-/* FIXME: rewrite this with walk instead of fold */
-
-/* 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 collect_ids_expr(&@expr e, @vec[uint] res) -> () {
+    vec::push(*res, (expr_ann(e)).id);
 }
-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 collect_ids_block(&block b, @vec[uint] res) -> () {
+    vec::push(*res, b.node.a.id);
 }
-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));
-    }
-    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, ?s_opt, ?e, ?a)) {
-            e1 = expr_ext(p, annotate_exprs(fm, es),
-                          s_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_assert(?e, ?a)) {
-            e1 = expr_assert(annotate_expr(fm, e), a);
-        }
-        case (expr_check(?e, ?a)) {
-            e1 = expr_check(annotate_expr(fm, e), a);
-        }
-        case (expr_port(_)) { /* no change */ }
-        case (expr_chan(?e, ?a)) {
-            e1 = expr_chan(annotate_expr(fm, e), a);
+fn collect_ids_stmt(&@stmt s, @vec[uint] res) -> () {
+    alt (s.node) {
+        case (stmt_decl(_,?a)) {
+            log("node_id " + uistr(a.id));
+            log_stmt(*s);
+  
+            vec::push(*res, a.id);
+        }
+        case (stmt_expr(_,?a)) {
+            log("node_id " + uistr(a.id));
+            log_stmt(*s);
+    
+            vec::push(*res, a.id);
         }
+        case (_) {}
     }
-    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 collect_ids_decl(&@decl d, @vec[uint] res) -> () {
+    alt (d.node) {
+        case (decl_local(?l)) {
+            vec::push(*res, l.ann.id);
         }
+        case (_) {}
     }
 }
-fn annotate_block(&fn_info_map fm, &block b) -> block {
-    let vec[@stmt] new_stmts = [];
-   
-    for (@stmt s in b.node.stmts) {
-        auto new_s = annotate_stmt(fm, s);
-        vec::push[@stmt](new_stmts, 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 with b.node));
-}
-fn annotate_fn(&fn_info_map fm, &_fn f) -> _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, &_mod m) -> _mod {
-    let vec[@item] new_items = [];
-   
-    for (@item i in m.items) {
-        auto new_i = annotate_item(fm, i);
-        vec::push[@item](new_items, new_i);
-    }
-    ret rec(items=new_items with m);
-}
-fn annotate_method(&fn_info_map fm, &@method m) -> @method {
-    auto f_info = get_fn_info(fm, m.node.id);
-    auto fld0 = new_identity_fold[fn_info]();
-    fld0 = @rec(fold_ann = bind init_ann(_,_) 
-                with *fld0);
-    auto outer = 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 node_ids_in_fn(&_fn f, &def_id d, @vec[uint] res) -> () {
+    auto collect_ids = walk::default_visitor();
+    collect_ids = rec(visit_expr_pre  = bind collect_ids_expr(_,res),
+                      visit_block_pre = bind collect_ids_block(_,res),
+                      visit_stmt_pre  = bind collect_ids_stmt(_,res),
+                      visit_decl_pre  = bind collect_ids_decl(_,res)
+                      with collect_ids);
+    walk::walk_fn(collect_ids, f, d);
 }
 
-fn annotate_obj(&fn_info_map fm, &_obj o) -> _obj {
-    fn one(fn_info_map fm, &@method m) -> @method {
-        ret annotate_method(fm, m);
+fn init_vecs(&crate_ctxt ccx, @vec[uint] node_ids, uint len) -> () {
+    for (uint i in *node_ids) {
+        log(uistr(i) + " |-> " + uistr(len));
+        ccx.node_anns.insert(i, empty_ann(len));
     }
-    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, &@item item) -> @item {
-    alt (item.node) {
-        /* FIXME can't skip this case -- exprs contain blocks contain stmts,
-         which contain decls */
-        case (item_const(_,_,_,_,_)) {
-            // this has already been annotated by annotate_item
-            ret item;
-        }
-        case (item_fn(?ident, ?ff, ?tps, ?id, ?ann)) {
-            ret @respan(item.span,
-                       item_fn(ident, annotate_fn(fm, ff), tps, id, ann));
-        }
-        case (item_mod(?ident, ?mm, ?id)) {
-            ret @respan(item.span,
-                       item_mod(ident, annotate_mod(fm, mm), id));
-        }
-        case (item_native_mod(?ident, ?mm, ?id)) {
-            ret item;
-        }
-        case (item_ty(_,_,_,_,_)) {
-            ret item;
-        }
-        case (item_tag(_,_,_,_,_)) {
-            ret item;
-        }
-        case (item_obj(?ident, ?ob, ?tps, ?odid, ?ann)) {
-            ret @respan(item.span,
-              item_obj(ident, annotate_obj(fm, ob), tps, odid, ann));
-        }
-    } 
+fn visit_fn(&crate_ctxt ccx, uint num_locals, &_fn f, &def_id d) -> () {
+     
+    let vec[uint] node_ids_ = [];
+    let @vec[uint] node_ids = @node_ids_;
+    node_ids_in_fn(f, d, node_ids);
+    init_vecs(ccx, node_ids, num_locals);
 }
 
-fn annotate_item(&fn_info_map fm, &@item item) -> @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 (item_const(_,_,_,_,_)) {
-            auto fld0 = new_identity_fold[()]();
-            fld0 = @rec(fold_ann = bind init_blank_ann(_,_) 
-                        with *fld0);
-            ret fold_item[()]((), fld0, item);
-        }
-        case (item_fn(?i,?ff,?tps,?id,?ann)) {
-            auto f_info = get_fn_info(fm, id);
-            auto fld0 = new_identity_fold[fn_info]();
-            fld0 = @rec(fold_ann = bind init_ann(_,_) 
-                        with *fld0);
-            auto outer = fold_item[fn_info](f_info, fld0, item);
-            // now recurse into any nested items
-            ret annotate_item_inner(fm, outer);
-         }
-        case (item_mod(?i, ?mm, ?id)) {
-            auto fld0 = new_identity_fold[()]();
-            fld0 = @rec(fold_ann = bind init_blank_ann(_,_) 
-                        with *fld0);
-            auto outer = fold_item[()]((), fld0, item);
-            ret annotate_item_inner(fm, outer);
-        }
-        case (item_native_mod(?i, ?nm, ?id)) {
-            ret item;
-        }
-        case (item_ty(_,_,_,_,_)) {
-            ret item;
-        }
-        case (item_tag(_,_,_,_,_)) {
-            ret item;
-        }
-        case (item_obj(?i,?ob,?tps,?odid,?ann)) {
-            auto fld0 = new_identity_fold[()]();
-            fld0 = @rec(fold_ann = bind init_blank_ann(_,_) 
-                        with *fld0);
-            auto outer = fold_item[()]((), fld0, item);
-            ret annotate_item_inner(fm, outer);
-        }
-    }
+fn annotate_in_fn(&crate_ctxt ccx, &_fn f, &def_id f_id) -> () {
+    auto f_info = get_fn_info(ccx, f_id);
+    visit_fn(ccx, num_locals(f_info), f, f_id);
 }
 
-fn annotate_module(&fn_info_map fm, &_mod module) -> _mod {
-    let vec[@item] new_items = [];
-   
-    for (@item i in module.items) {
-        auto new_item = annotate_item(fm, i);
-        vec::push[@item](new_items, new_item);
-    }
-
-    ret rec(items = new_items with module);
+fn annotate_crate(&crate_ctxt ccx, &crate crate) -> () {
+    auto do_ann = walk::default_visitor();
+    do_ann = rec(visit_fn_pre = bind annotate_in_fn(ccx, _, _)
+                 with do_ann);
+    walk::walk_crate(do_ann, crate);
 }
 
-fn annotate_crate(&fn_info_map fm, &@crate crate) -> @crate {
-    ret @respan(crate.span,
-               rec(module = annotate_module(fm, crate.node.module)
-                   with crate.node));
-}
+//
+// 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/middle/tstate/auxiliary.rs b/src/comp/middle/tstate/auxiliary.rs
index dbe411b0b66..2e656e45ceb 100644
--- a/src/comp/middle/tstate/auxiliary.rs
+++ b/src/comp/middle/tstate/auxiliary.rs
@@ -37,6 +37,7 @@ import util::common;
 import util::common::span;
 import util::common::log_block;
 import util::common::new_def_hash;
+import util::common::new_uint_hash;
 import util::common::log_expr_err;
 import util::common::uistr;
 
@@ -157,6 +158,10 @@ fn print_idents(vec[ident] idents) -> () {
 type var_info     = tup(uint, ident);
 type fn_info      = rec(@std::map::hashmap[def_id, var_info] vars,
                         controlflow cf);
+
+/* mapping from node ID to typestate annotation */
+type node_ann_table = @std::map::hashmap[uint, ts_ann];
+
 /* mapping from function name to fn_info map */
 type fn_info_map = @std::map::hashmap[def_id, fn_info];
 
@@ -167,176 +172,187 @@ type fn_ctxt    = rec(fn_info enclosing,
 
 type crate_ctxt = rec(ty::ctxt tcx,
                       ty::node_type_table node_types,
+                      node_ann_table node_anns,
                       fn_info_map fm);
 
-fn get_fn_info(fn_info_map fm, def_id did) -> fn_info {
-    assert (fm.contains_key(did));
-    ret fm.get(did);
+fn get_fn_info(&crate_ctxt ccx, def_id did) -> fn_info {
+    assert (ccx.fm.contains_key(did));
+    ret ccx.fm.get(did);
 }
 
 /********* utils ********/
 
-
-fn ann_to_ts_ann(ann a, uint nv) -> @ts_ann {
-    alt (ann_to_ts_ann_fail(a)) {
-        case (none[@ts_ann])         { ret @empty_ann(nv); }
-        case (some[@ts_ann](?t))     { ret t; }
-    }
-}
-
-
-fn ann_to_ts_ann_fail(ann a) -> option::t[@ts_ann] { ret a.ts; }
-
-fn ann_to_ts_ann_strict(ann a) -> @ts_ann {
-    alt (ann_to_ts_ann_fail(a)) {
-        case (none[@ts_ann]) {
-            log("ann_to_ts_ann_strict: didn't expect none here");
+fn ann_to_ts_ann(&crate_ctxt ccx, &ann a) -> ts_ann {
+    alt (ccx.node_anns.find(a.id)) {
+        case (none[ts_ann])         { 
+            log_err ("ann_to_ts_ann: no ts_ann for node_id "
+                     + uistr(a.id));
             fail;
         }
-        case (some[@ts_ann](?t)) { ret t; }
+        case (some[ts_ann](?t))     { ret t; }
     }
 }
 
-fn ann_to_poststate(ann a) -> poststate {
-    ret (ann_to_ts_ann_strict(a)).states.poststate;
+fn ann_to_poststate(&crate_ctxt ccx, ann a) -> poststate {
+    log "ann_to_poststate";
+    ret (ann_to_ts_ann(ccx, a)).states.poststate;
 }
 
-fn stmt_to_ann(&stmt s) -> option::t[@ts_ann] {
+fn stmt_to_ann(&crate_ctxt ccx, &stmt s) -> ts_ann {
+    log "stmt_to_ann";
   alt (s.node) {
     case (stmt_decl(_,?a)) {
-        ret ann_to_ts_ann_fail(a);
+        ret ann_to_ts_ann(ccx, a);
     }
     case (stmt_expr(_,?a)) {
-        ret ann_to_ts_ann_fail(a);
+        ret ann_to_ts_ann(ccx, a);
     }
     case (stmt_crate_directive(_)) {
-      ret none[@ts_ann];
+        log_err "expecting an annotated statement here";
+        fail;
     }
   }
 }
 
-fn stmt_to_ann_strict(&stmt s) -> @ts_ann {
-    alt (stmt_to_ann(s)) {
-        case (none[@ts_ann]) {
-            log_err("stmt_to_ann_strict: didn't expect none here");
-            fail;
-        }
-        case (some[@ts_ann](?a)) { ret a; }
-    }
-}
-
 /* fails if e has no annotation */
-fn expr_states(@expr e) -> pre_and_post_state {
-    ret (ann_to_ts_ann_strict(expr_ann(e)).states);
+fn expr_states(&crate_ctxt ccx, @expr e) -> pre_and_post_state {
+    log "expr_states";
+    ret (ann_to_ts_ann(ccx, expr_ann(e)).states);
 }
 
 /* fails if e has no annotation */
-fn expr_pp(@expr e) -> pre_and_post {
-    ret (ann_to_ts_ann_strict(expr_ann(e)).conditions);
+fn expr_pp(&crate_ctxt ccx, @expr e) -> pre_and_post {
+    log "expr_pp";
+    ret (ann_to_ts_ann(ccx, expr_ann(e)).conditions);
 }
 
-fn stmt_pp(&stmt s) -> pre_and_post {
-    ret (stmt_to_ann_strict(s).conditions);
+fn stmt_pp(&crate_ctxt ccx, &stmt s) -> pre_and_post {
+    ret (stmt_to_ann(ccx, s).conditions);
 }
 
 /* fails if b has no annotation */
-fn block_pp(&block b) -> pre_and_post {
-    ret (ann_to_ts_ann_strict(b.node.a).conditions);
+fn block_pp(&crate_ctxt ccx, &block b) -> pre_and_post {
+    log "block_pp";
+    ret (ann_to_ts_ann(ccx, b.node.a).conditions);
 }
 
-fn block_states(&block b) -> pre_and_post_state {
-    ret (ann_to_ts_ann_strict(b.node.a).states);
+fn clear_pp(pre_and_post pp) {
+    ann::clear(pp.precondition);
+    ann::clear(pp.postcondition);
 }
 
-fn stmt_states(&stmt s, uint nv) -> pre_and_post_state {
-  alt (stmt_to_ann(s)) {
-    case (none[@ts_ann]) {
-      ret empty_states(nv);
-    }
-    case (some[@ts_ann](?a)) {
-      ret a.states;
-    }
-  }
+fn clear_precond(&crate_ctxt ccx, &ann a) {
+    auto pp = ann_to_ts_ann(ccx, a);
+    ann::clear(pp.conditions.precondition);
+}
+
+fn block_states(&crate_ctxt ccx, &block b) -> pre_and_post_state {
+    log "block_states";
+    ret (ann_to_ts_ann(ccx, b.node.a).states);
 }
 
-fn expr_precond(@expr e) -> precond {
-  ret (expr_pp(e)).precondition;
+fn stmt_states(&crate_ctxt ccx, &stmt s) -> pre_and_post_state {
+    ret (stmt_to_ann(ccx, s)).states;
 }
 
-fn expr_postcond(@expr e) -> postcond {
-  ret (expr_pp(e)).postcondition;
+fn expr_precond(&crate_ctxt ccx, @expr e) -> precond {
+    ret (expr_pp(ccx, e)).precondition;
 }
 
-fn expr_prestate(@expr e) -> prestate {
-  ret (expr_states(e)).prestate;
+fn expr_postcond(&crate_ctxt ccx, @expr e) -> postcond {
+    ret (expr_pp(ccx, e)).postcondition;
 }
 
-fn expr_poststate(@expr e) -> poststate {
-  ret (expr_states(e)).poststate;
+fn expr_prestate(&crate_ctxt ccx, @expr e) -> prestate {
+    ret (expr_states(ccx, e)).prestate;
 }
 
-fn stmt_precond(&stmt s) -> precond {
-  ret (stmt_pp(s)).precondition;
+fn expr_poststate(&crate_ctxt ccx, @expr e) -> poststate {
+    ret (expr_states(ccx, e)).poststate;
 }
 
-fn stmt_postcond(&stmt s) -> postcond {
-  ret (stmt_pp(s)).postcondition;
+fn stmt_precond(&crate_ctxt ccx, &stmt s) -> precond {
+    ret (stmt_pp(ccx, s)).precondition;
+}
+
+fn stmt_postcond(&crate_ctxt ccx, &stmt s) -> postcond {
+    ret (stmt_pp(ccx, s)).postcondition;
 }
 
 fn states_to_poststate(&pre_and_post_state ss) -> poststate {
   ret ss.poststate;
 }
 
-fn stmt_prestate(&stmt s, uint nv) -> prestate {
-  ret (stmt_states(s, nv)).prestate;
+fn stmt_prestate(&crate_ctxt ccx, &stmt s) -> prestate {
+    ret (stmt_states(ccx, s)).prestate;
 }
 
-fn stmt_poststate(&stmt s, uint nv) -> poststate {
-  ret (stmt_states(s, nv)).poststate;
+fn stmt_poststate(&crate_ctxt ccx, &stmt s) -> poststate {
+    ret (stmt_states(ccx, s)).poststate;
 }
 
-fn block_postcond(&block b) -> postcond {
-    ret (block_pp(b)).postcondition;
+fn block_postcond(&crate_ctxt ccx, &block b) -> postcond {
+    ret (block_pp(ccx, b)).postcondition;
 }
 
-fn block_poststate(&block b) -> poststate {
-    ret (block_states(b)).poststate;
+fn block_poststate(&crate_ctxt ccx, &block b) -> poststate {
+    ret (block_states(ccx, b)).poststate;
 }
 
-/* returns a new annotation where the pre_and_post is p */
-fn with_pp(ann a, pre_and_post p) -> ann {
-    ret rec(id=a.id, ty=a.ty, tps=a.tps,
-            ts=some[@ts_ann](@rec(conditions=p,
-                                  states=empty_states(pps_len(p)))));
+/* sets the pre_and_post for an ann */
+fn with_pp(&crate_ctxt ccx, &ann a, pre_and_post p) {
+    ccx.node_anns.insert(a.id, @rec(conditions=p,
+                                    states=empty_states(pps_len(p))));
 }
 
-fn set_prestate_ann(&ann a, &prestate pre) -> bool {
-    ret set_prestate(ann_to_ts_ann_strict(a), pre);
+fn set_prestate_ann(&crate_ctxt ccx, &ann a, &prestate pre) -> bool {
+    log "set_prestate_ann";
+    ret set_prestate(ann_to_ts_ann(ccx, a), pre);
 }
 
 
-fn extend_prestate_ann(&ann a, &prestate pre) -> bool {
-    ret extend_prestate(ann_to_ts_ann_strict(a).states.prestate, pre);
+fn extend_prestate_ann(&crate_ctxt ccx, &ann a, &prestate pre) -> bool {
+    log "extend_prestate_ann";
+    ret extend_prestate(ann_to_ts_ann(ccx, a).states.prestate, pre);
 }
 
-fn set_poststate_ann(&ann a, &poststate post) -> bool {
-    ret set_poststate(ann_to_ts_ann_strict(a), post);
+fn set_poststate_ann(&crate_ctxt ccx, &ann a, &poststate post) -> bool {
+    log "set_poststate_ann";
+    ret set_poststate(ann_to_ts_ann(ccx, a), post);
 }
 
-fn extend_poststate_ann(&ann a, &poststate post) -> bool {
-    ret extend_poststate(ann_to_ts_ann_strict(a).states.poststate, post);
+fn extend_poststate_ann(&crate_ctxt ccx, &ann a, &poststate post) -> bool {
+    log "extend_poststate_ann";
+    ret extend_poststate(ann_to_ts_ann(ccx, a).states.poststate, post);
 }
 
-fn set_pre_and_post(&ann a, &pre_and_post pp) -> () {
-    auto t = ann_to_ts_ann_strict(a);
-    set_precondition(t, pp.precondition);
-    set_postcondition(t, pp.postcondition);
+fn set_pre_and_post(&crate_ctxt ccx, &ann a,
+                    &precond pre, &postcond post) -> () {
+    log "set_pre_and_post";
+    auto t = ann_to_ts_ann(ccx, a);
+    set_precondition(t, pre);
+    set_postcondition(t, post);
 }
 
-fn pure_exp(&ann a, &prestate p) -> bool {
+fn copy_pre_post(&crate_ctxt ccx, &ann a, &@expr sub) -> () {
+    log "set_pre_and_post";
+    auto p = expr_pp(ccx, sub);
+    auto t = ann_to_ts_ann(ccx, a);
+    set_precondition(t, p.precondition);
+    set_postcondition(t, p.postcondition);
+}
+
+
+/* sets all bits to *1* */
+fn set_postcond_false(&crate_ctxt ccx, &ann a) {
+    auto p = ann_to_ts_ann(ccx, a);
+    ann::set(p.conditions.postcondition);
+}
+
+fn pure_exp(&crate_ctxt ccx, &ann a, &prestate p) -> bool {
   auto changed = false;
-  changed = extend_prestate_ann(a, p) || changed;
-  changed = extend_poststate_ann(a, p) || changed;
+  changed = extend_prestate_ann(ccx, a, p) || changed;
+  changed = extend_poststate_ann(ccx, a, p) || changed;
   ret changed;
 }
 
@@ -354,31 +370,14 @@ fn fixed_point_states(&fn_ctxt fcx,
   }
 }
 
-fn init_ann(&fn_info fi, &ann a) -> ann {
-    ret rec(id=a.id, ty=a.ty, tps=a.tps,
-            ts=some[@ts_ann](@empty_ann(num_locals(fi))));
-}
-
-fn init_blank_ann(&() ignore, &ann a) -> ann {
-    ret rec(id=a.id, ty=a.ty, tps=a.tps, ts=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));
-
-    auto fld0 = new_identity_fold[fn_info]();
-
-    fld0 = @rec(fold_ann = bind init_ann(_,_) with *fld0);
-    ret fold_block[fn_info](fi, fld0, respan(sp, b)); 
-}
-
 fn num_locals(fn_info m) -> uint {
   ret m.vars.size();
 }
 
 fn new_crate_ctxt(ty::node_type_table nt, ty::ctxt cx) -> crate_ctxt {
-    ret rec(tcx=cx, node_types=nt, fm=@new_def_hash[fn_info]());
+    ret rec(tcx=cx, node_types=nt, 
+            node_anns=@new_uint_hash[ts_ann](),
+            fm=@new_def_hash[fn_info]());
 }
 
 fn controlflow_def_id(&crate_ctxt ccx, &def_id d) -> controlflow {
@@ -395,9 +394,15 @@ fn controlflow_def_id(&crate_ctxt ccx, &def_id d) -> controlflow {
 fn controlflow_expr(&crate_ctxt ccx, @expr e) -> controlflow {
     auto f = expr_ann(e).id;
     alt (ccx.tcx.def_map.find(f)) {
-        case (some[def](def_fn(?d)))        { ret controlflow_def_id(ccx, d); }
-        case (some[def](def_obj_field(?d))) { ret controlflow_def_id(ccx, d); }
-        case (_)                            { ret return; }
+        case (some[def](def_fn(?d))) { 
+            ret controlflow_def_id(ccx, d); 
+        }
+        case (some[def](def_obj_field(?d))) { 
+            ret controlflow_def_id(ccx, d);
+        }
+        case (_)                            {
+            ret return;
+        }
     }
 }
 
diff --git a/src/comp/middle/tstate/bitvectors.rs b/src/comp/middle/tstate/bitvectors.rs
index a0b9e5a3ece..aa379e072af 100644
--- a/src/comp/middle/tstate/bitvectors.rs
+++ b/src/comp/middle/tstate/bitvectors.rs
@@ -12,8 +12,8 @@ import aux::fn_ctxt;
 import aux::fn_info;
 import aux::log_bitv;
 import aux::num_locals;
-import aux::ann_to_ts_ann_strict;
 
+import tstate::aux::ann_to_ts_ann;
 import tstate::ann::pre_and_post;
 import tstate::ann::precond;
 import tstate::ann::postcond;
@@ -48,7 +48,7 @@ fn seq_preconds(fn_info enclosing, vec[pre_and_post] pps) -> precond {
   let uint num_vars = num_locals(enclosing);
 
   if (sz >= 1u) {
-    auto first   = pps.(0);
+    auto first = pps.(0);
     assert (pps_len(first) == num_vars);
     let precond rest = seq_preconds(enclosing,
                          slice[pre_and_post](pps, 1u, sz));
@@ -115,9 +115,10 @@ fn intersect_postconds(&vec[postcond] pcs) -> postcond {
 }
 
 fn gen(&fn_ctxt fcx, &ann a, def_id id) -> bool {
+  log "gen";
   assert (fcx.enclosing.vars.contains_key(id));
   let uint i = (fcx.enclosing.vars.get(id))._0;
-  ret set_in_postcond(i, (ann_to_ts_ann_strict(a)).conditions);
+  ret set_in_postcond(i, (ann_to_ts_ann(fcx.ccx, a)).conditions);
 }
 
 fn declare_var(&fn_info enclosing, def_id id, prestate pre)
@@ -130,8 +131,9 @@ fn declare_var(&fn_info enclosing, def_id id, prestate pre)
 }
 
 fn gen_poststate(&fn_ctxt fcx, &ann a, def_id id) -> bool {
+  log "gen_poststate";
   assert (fcx.enclosing.vars.contains_key(id));
   let uint i = (fcx.enclosing.vars.get(id))._0;
-  ret set_in_poststate(i, (ann_to_ts_ann_strict(a)).states);
+  ret set_in_poststate(i, (ann_to_ts_ann(fcx.ccx, a)).states);
 }
 
diff --git a/src/comp/middle/tstate/ck.rs b/src/comp/middle/tstate/ck.rs
index f9e8416a322..5de793d64b0 100644
--- a/src/comp/middle/tstate/ck.rs
+++ b/src/comp/middle/tstate/ck.rs
@@ -56,6 +56,8 @@ import aux::fixed_point_states;
 import aux::bitv_to_str;
 
 import util::common::ty_to_str;
+import util::common::log_stmt_err;
+import aux::log_bitv_err;
 import bitvectors::promises;
 
 import annotate::annotate_crate;
@@ -64,51 +66,45 @@ import pre_post_conditions::check_item_fn;
 import states::find_pre_post_state_fn;
 
 fn check_states_expr(&fn_ctxt fcx, @expr e) -> () {
-  let precond prec    = expr_precond(e);
-  let prestate pres   = expr_prestate(e);
-
-  if (!implies(pres, prec)) {
-      auto s = "";
-      s += ("Unsatisfied precondition constraint for expression:\n");
-      s += util::common::expr_to_str(e);
-      s += ("Precondition: ");
-      s += bitv_to_str(fcx.enclosing, prec);
-      s += ("Prestate: ");
-      s += bitv_to_str(fcx.enclosing, pres);
-      fcx.ccx.tcx.sess.span_err(e.span, s);
-  }
+    let precond prec  = expr_precond(fcx.ccx, e);
+    let prestate pres = expr_prestate(fcx.ccx, e);
+
+    if (!implies(pres, prec)) {
+        auto s = "";
+        s += ("Unsatisfied precondition constraint for expression:\n");
+        s += util::common::expr_to_str(e);
+        s += ("Precondition: ");
+        s += bitv_to_str(fcx.enclosing, prec);
+        s += ("Prestate: ");
+        s += bitv_to_str(fcx.enclosing, pres);
+        fcx.ccx.tcx.sess.span_err(e.span, s);
+    }
 }
 
 fn check_states_stmt(&fn_ctxt fcx, &stmt s) -> () {
-  alt (stmt_to_ann(s)) {
-    case (none[@ts_ann]) {
-      ret;
-    }
-    case (some[@ts_ann](?a)) {
-      let precond prec    = ann_precond(*a);
-      let prestate pres   = ann_prestate(*a);
-
-      /*
-      log("check_states_stmt:");
-      log_stmt(s);
-      log("prec = ");
-      log_bitv(enclosing, prec);
-      log("pres = ");
-      log_bitv(enclosing, pres);
-      */
-
-      if (!implies(pres, prec)) {
-          auto ss = "";
-          ss += ("Unsatisfied precondition constraint for statement:\n");
-          ss += util::common::stmt_to_str(s);
-          ss += ("Precondition: ");
-          ss += bitv_to_str(fcx.enclosing, prec);
-          ss += ("Prestate: ");
-          ss += bitv_to_str(fcx.enclosing, pres);
-          fcx.ccx.tcx.sess.span_err(s.span, ss);
-      }
+    auto a = stmt_to_ann(fcx.ccx, s);
+    let precond prec    = ann_precond(a);
+    let prestate pres   = ann_prestate(a);
+
+    /*    
+      log_err("check_states_stmt:");
+      log_stmt_err(s);
+      log_err("prec = ");
+      log_bitv_err(fcx.enclosing, prec);
+      log_err("pres = ");
+      log_bitv_err(fcx.enclosing, pres);
+    */
+
+    if (!implies(pres, prec)) {
+        auto ss = "";
+        ss += ("Unsatisfied precondition constraint for statement:\n");
+        ss += util::common::stmt_to_str(s);
+        ss += ("Precondition: ");
+        ss += bitv_to_str(fcx.enclosing, prec);
+        ss += ("Prestate: ");
+        ss += bitv_to_str(fcx.enclosing, pres);
+        fcx.ccx.tcx.sess.span_err(s.span, ss);
     }
-  }
 }
 
 fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) -> () {
@@ -116,33 +112,30 @@ fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) -> () {
     auto nv   = num_locals(enclosing);
     auto post = @empty_poststate(nv);
 
-    fn do_one_(fn_ctxt fcx, &@stmt s, @poststate post, uint nv) -> () {
+    fn do_one_(fn_ctxt fcx, &@stmt s, @poststate post) -> () {
         check_states_stmt(fcx, *s);
-        *post = stmt_poststate(*s, nv);
+        *post = stmt_poststate(fcx.ccx, *s);
     }
 
-    auto do_one = bind do_one_(fcx, _, post, nv);
+    auto do_one = bind do_one_(fcx, _, post);
  
-  vec::map[@stmt, ()](do_one, f.body.node.stmts);
-  fn do_inner_(fn_ctxt fcx, &@expr e, @poststate post) -> () {
-    check_states_expr(fcx, e);
-    *post = expr_poststate(e);
-  }
-  auto do_inner = bind do_inner_(fcx, _, post);
-  option::map[@expr, ()](do_inner, f.body.node.expr);
+    vec::map[@stmt, ()](do_one, f.body.node.stmts);
+    fn do_inner_(fn_ctxt fcx, &@expr e, @poststate post) -> () {
+        check_states_expr(fcx, e);
+        *post = expr_poststate(fcx.ccx, e);
+    }
+    auto do_inner = bind do_inner_(fcx, _, post);
+    option::map[@expr, ()](do_inner, f.body.node.expr);
   
-  /* Finally, check that the return value is initialized */
-  if (f.proto == ast::proto_fn
-      && ! promises(*post, fcx.id, enclosing)
-      && ! type_is_nil(fcx.ccx.tcx,
-                       ret_ty_of_fn(fcx.ccx.node_types, fcx.ccx.tcx, a)) ) {
-      /* FIXME: make this an error, not warning, once I finish implementing
-         ! annotations */
-        /* fcx.ccx.tcx.sess.span_err(f.body.span, "Function " +
-           fcx.name + " may not return. Its declared return type is "
-           + util.common.ty_to_str(*f.decl.output)); */
-        fcx.ccx.tcx.sess.span_warn(f.body.span, "not all control paths " +
-            "return a value");
+    /* Finally, check that the return value is initialized */
+    if (f.proto == ast::proto_fn
+        && ! promises(*post, fcx.id, enclosing)
+        && ! type_is_nil(fcx.ccx.tcx,
+                         ret_ty_of_fn(fcx.ccx.node_types, fcx.ccx.tcx, a)) ) {
+        /* FIXME: call span_err, not span_warn, once I finish implementing
+           ! annotations */
+        fcx.ccx.tcx.sess.span_warn(f.body.span, "In function " + fcx.name +
+          ", not all control paths return a value");
         fcx.ccx.tcx.sess.span_note(f.decl.output.span,
             "see declared return type of '" + ty_to_str(*f.decl.output) +
             "'");
@@ -202,15 +195,15 @@ fn check_crate(ty::node_type_table nt, ty::ctxt cx, @crate crate) -> @crate {
     /* Build the global map from function id to var-to-bit-num-map */
     mk_f_to_fn_info(ccx, crate);
   
-    /* Add a blank ts_ann to every statement (and expression) */
-    auto with_anns = annotate_crate(ccx.fm, crate);
+    /* Add a blank ts_ann for every statement (and expression) */
+    annotate_crate(ccx, *crate);
 
     /* Compute the pre and postcondition for every subexpression */
     
     auto fld = new_identity_fold[crate_ctxt]();
     fld = @rec(fold_item_fn = bind check_item_fn(_,_,_,_,_,_,_) with *fld);
     auto with_pre_postconditions =
-           fold_crate[crate_ctxt](ccx, fld, with_anns);
+           fold_crate[crate_ctxt](ccx, fld, crate);
     
     auto fld1 = new_identity_fold[crate_ctxt]();
 
diff --git a/src/comp/middle/tstate/collect_locals.rs b/src/comp/middle/tstate/collect_locals.rs
index 29f73a149c7..9f999860096 100644
--- a/src/comp/middle/tstate/collect_locals.rs
+++ b/src/comp/middle/tstate/collect_locals.rs
@@ -31,22 +31,28 @@ import aux::var_info;
 import aux::crate_ctxt;
 
 import util::common::new_def_hash;
+import util::common::uistr;
 
 fn var_is_local(def_id v, fn_info m) -> bool {
   ret (m.vars.contains_key(v));
 }
 
-fn collect_local(&@vec[tup(ident, def_id)] vars, &@local loc) -> () {
-    log("collect_local: pushing " + loc.ident);
-    _vec::push[tup(ident, def_id)](*vars, tup(loc.ident, loc.id));
+fn collect_local(&@vec[tup(ident, def_id)] vars, &@decl d) -> () {
+    alt (d.node) {
+      case (decl_local(?loc)) {
+        log("collect_local: pushing " + loc.ident);
+        vec::push[tup(ident, def_id)](*vars, tup(loc.ident, loc.id));
+      }
+      case (_) { ret; }
+    }
 }
 
-fn find_locals(_fn f) -> @vec[tup(ident,def_id)] {
+fn find_locals(_fn f, def_id d) -> @vec[tup(ident,def_id)] {
   auto res = @vec::alloc[tup(ident,def_id)](0u);
 
   auto visitor = walk::default_visitor();
   visitor = rec(visit_decl_pre=bind collect_local(res,_) with visitor);
-  walk_fn(visitor, f);
+  walk_fn(visitor, f, d);
 
   ret res;
 }
@@ -69,7 +75,7 @@ fn mk_fn_info(_fn f, def_id f_id, ident f_name) -> fn_info {
     /* ignore args, which we know are initialized;
        just collect locally declared vars */
 
-    let @vec[tup(ident,def_id)] locals = find_locals(f);
+    let @vec[tup(ident,def_id)] locals = find_locals(f, f_id);
     // 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);
@@ -78,6 +84,9 @@ fn mk_fn_info(_fn f, def_id f_id, ident f_name) -> fn_info {
        we can safely use the function's name itself for this purpose */
     add_var(f_id, f_name, next, res);
 
+    log(f_name + " has " + uistr(vec::len[tup(ident, def_id)](*locals))
+            + " locals");
+   
     ret res;
 }
 
@@ -91,7 +100,7 @@ fn mk_fn_info_item (&crate_ctxt ccx, &@item i) -> () {
       ccx.fm.insert(id, f_inf);
     }
     case (item_obj(?i,?o,?ty_params,?odid,?a)) {
-      auto all_methods = _vec::clone[@method](o.methods);
+      auto all_methods = vec::clone[@method](o.methods);
       plus_option[@method](all_methods, o.dtor);
       auto f_inf;
       for (@method m in all_methods) {
@@ -109,7 +118,7 @@ fn mk_fn_info_item (&crate_ctxt ccx, &@item i) -> () {
 fn mk_f_to_fn_info(&crate_ctxt ccx, @crate c) -> () {
   let ast_visitor vars_visitor = walk::default_visitor();
   vars_visitor = rec(visit_item_post=bind mk_fn_info_item(ccx,_)
-		     with vars_visitor);
+                     with vars_visitor);
 
   walk_crate(vars_visitor, *c);
 }
diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs
index adcfc496319..30437a4eeb5 100644
--- a/src/comp/middle/tstate/pre_post_conditions.rs
+++ b/src/comp/middle/tstate/pre_post_conditions.rs
@@ -9,13 +9,14 @@ import tstate::ann::get_post;
 import tstate::ann::postcond;
 import tstate::ann::true_precond;
 import tstate::ann::false_postcond;
-import tstate::ann::empty_pre_post;
 import tstate::ann::empty_poststate;
 import tstate::ann::require_and_preserve;
 import tstate::ann::union;
 import tstate::ann::intersect;
 import tstate::ann::pp_clone;
 import tstate::ann::empty_prestate;
+import tstate::ann::set_precondition;
+import tstate::ann::set_postcondition;
 import aux::var_info;
 import aux::crate_ctxt;
 import aux::fn_ctxt;
@@ -23,7 +24,10 @@ import aux::num_locals;
 import aux::expr_pp;
 import aux::stmt_pp;
 import aux::block_pp;
+import aux::clear_pp;
+import aux::clear_precond;
 import aux::set_pre_and_post;
+import aux::copy_pre_post;
 import aux::expr_precond;
 import aux::expr_postcond;
 import aux::expr_prestate;
@@ -33,6 +37,8 @@ import aux::fn_info;
 import aux::log_pp;
 import aux::ann_to_def;
 import aux::ann_to_def_strict;
+import aux::ann_to_ts_ann;
+import aux::set_postcond_false;
 
 import bitvectors::seq_preconds;
 import bitvectors::union_postconds;
@@ -145,6 +151,8 @@ import util::common::field_exprs;
 import util::common::has_nonlocal_exits;
 import util::common::log_stmt;
 import util::common::log_expr_err;
+import util::common::log_block_err;
+import util::common::log_block;
 
 fn find_pre_post_mod(&_mod m) -> _mod {
     log("implement find_pre_post_mod!");
@@ -209,6 +217,11 @@ fn find_pre_post_item(&crate_ctxt ccx, &item i) -> () {
    the preconditions for <args>, and the postcondition in a to 
    be the union of all postconditions for <args> */
 fn find_pre_post_exprs(&fn_ctxt fcx, &vec[@expr] args, ann a) {
+    if (vec::len[@expr](args) > 0u) {
+        log ("find_pre_post_exprs: oper =");
+        log_expr(*(args.(0)));
+    }
+
     auto enclosing = fcx.enclosing;
     auto fm        = fcx.ccx.fm;
     auto nv        = num_locals(enclosing);
@@ -220,37 +233,40 @@ fn find_pre_post_exprs(&fn_ctxt fcx, &vec[@expr] args, ann a) {
 
     vec::map[@expr, ()](f, args);
 
-    fn get_pp(&@expr e) -> pre_and_post {
-        ret expr_pp(e);
+    fn get_pp(crate_ctxt ccx, &@expr e) -> pre_and_post {
+        ret expr_pp(ccx, e);
     }
-    auto g = get_pp;
+
+    auto g = bind get_pp(fcx.ccx, _);
     auto pps = vec::map[@expr, pre_and_post](g, args);
     auto h = get_post;
 
-    set_pre_and_post(a,
-       rec(precondition=seq_preconds(enclosing, pps),
-           postcondition=union_postconds
-           (nv, (vec::map[pre_and_post, postcond](h, pps)))));
+    set_pre_and_post(fcx.ccx, a, seq_preconds(enclosing, pps),
+        union_postconds
+          (nv, (vec::map[pre_and_post, postcond](h, pps))));
 }
 
 fn find_pre_post_loop(&fn_ctxt fcx, &@decl d, &@expr index,
       &block body, &ann a) -> () {
     find_pre_post_expr(fcx, index);
     find_pre_post_block(fcx, body);
+    log("222");
     auto loop_precond = declare_var(fcx.enclosing, decl_lhs(d),
-           seq_preconds(fcx.enclosing, [expr_pp(index),
-                                       block_pp(body)]));
+      seq_preconds(fcx.enclosing, [expr_pp(fcx.ccx, index),
+                                   block_pp(fcx.ccx, body)]));
     auto loop_postcond = intersect_postconds
-        ([expr_postcond(index), block_postcond(body)]);
-    set_pre_and_post(a, rec(precondition=loop_precond,
-                            postcondition=loop_postcond));
+        ([expr_postcond(fcx.ccx, index), block_postcond(fcx.ccx, body)]);
+    set_pre_and_post(fcx.ccx, a, loop_precond, loop_postcond);
 }
 
-fn gen_if_local(&fn_ctxt fcx, @expr lhs, @expr rhs, &ann larger_ann, &ann new_var) -> () {
+fn gen_if_local(&fn_ctxt fcx, @expr lhs, @expr rhs,
+                &ann larger_ann, &ann new_var) -> () {
   alt (ann_to_def(fcx.ccx, new_var)) {
     case (some[def](def_local(?d_id))) {
       find_pre_post_expr(fcx, rhs);
-      set_pre_and_post(larger_ann, expr_pp(rhs));
+      auto p = expr_pp(fcx.ccx, rhs);
+      set_pre_and_post(fcx.ccx, larger_ann,
+                       p.precondition, p.postcondition);
       gen(fcx, larger_ann, d_id);
     }
     case (_) { find_pre_post_exprs(fcx, [lhs, rhs], larger_ann); }
@@ -265,15 +281,10 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
     fn do_rand_(fn_ctxt fcx, &@expr e) -> () {
         find_pre_post_expr(fcx, e);
     }
-    fn pp_one(&@expr e) -> pre_and_post {
-        ret expr_pp(e);
-    }
     
-    /*
-    log_err("find_pre_post_expr (num_locals =" +
+    log("find_pre_post_expr (num_locals =" +
         uistr(num_local_vars) + "):");
-    log_expr_err(*e);
-    */
+    log_expr(*e);
 
     alt (e.node) {
         case (expr_call(?operator, ?operands, ?a)) {
@@ -293,9 +304,10 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
             find_pre_post_exprs(fcx, elt_exprs(elts), a);
         }
         case (expr_path(?p, ?a)) {
-            auto res = empty_pre_post(num_local_vars);
-	    
-	    auto df = ann_to_def_strict(fcx.ccx, a);
+            auto res = expr_pp(fcx.ccx, e);
+            clear_pp(res);
+
+            auto df = ann_to_def_strict(fcx.ccx, a);
             alt (df) {
                 case (def_local(?d_id)) {
                     auto i = bit_num(d_id, enclosing);
@@ -303,37 +315,33 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
                 }
                 case (_) { /* nothing to check */ }
             }
-
-            // 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));
+            clear_pp(expr_pp(fcx.ccx, e));
         }
         case(expr_log(_, ?arg, ?a)) {
             find_pre_post_expr(fcx, arg);
-            set_pre_and_post(a, expr_pp(arg));
+            copy_pre_post(fcx.ccx, a, arg);
         }
         case (expr_chan(?arg, ?a)) {
             find_pre_post_expr(fcx, arg);
-            set_pre_and_post(a, expr_pp(arg));
+            copy_pre_post(fcx.ccx, a, arg);
         }
         case(expr_put(?opt, ?a)) {
             alt (opt) {
                 case (some[@expr](?arg)) {
                     find_pre_post_expr(fcx, arg);
-                    set_pre_and_post(a, expr_pp(arg));
+                    copy_pre_post(fcx.ccx, a, arg);
                 }
                 case (none[@expr]) {
-                    set_pre_and_post(a, empty_pre_post(num_local_vars));
+                    clear_pp(expr_pp(fcx.ccx, e));
                 }
             }
         }
         case (expr_block(?b, ?a)) {
             find_pre_post_block(fcx, b);
-            set_pre_and_post(a, block_pp(b));
+            auto p = block_pp(fcx.ccx, b);
+            set_pre_and_post(fcx.ccx, a, p.precondition, p.postcondition);
         }
         case (expr_rec(?fields,?maybe_base,?a)) {
             auto es = field_exprs(fields);
@@ -343,7 +351,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
         case (expr_assign(?lhs, ?rhs, ?a)) {
             alt (lhs.node) {
                 case (expr_path(?p, ?a_lhs)) {
-		  gen_if_local(fcx, lhs, rhs, a, a_lhs);
+                  gen_if_local(fcx, lhs, rhs, a, a_lhs);
                 }
                 case (_) {
                     find_pre_post_exprs(fcx, [lhs, rhs], a);
@@ -353,7 +361,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
         case (expr_recv(?lhs, ?rhs, ?a)) {
             alt (lhs.node) {
                 case (expr_path(?p, ?a_lhs)) {
-		  gen_if_local(fcx, lhs, rhs, a, a_lhs);
+                  gen_if_local(fcx, lhs, rhs, a, a_lhs);
                 }
                 case (_) {
                     // doesn't check that lhs is an lval, but
@@ -368,63 +376,65 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
             find_pre_post_exprs(fcx, [lhs, rhs], a);
         }
         case (expr_lit(_,?a)) {
-            set_pre_and_post(a, empty_pre_post(num_local_vars));
+            clear_pp(expr_pp(fcx.ccx, e));
         }
         case (expr_ret(?maybe_val, ?a)) {
             alt (maybe_val) {
                 case (none[@expr]) {
-                    set_pre_and_post(a,
-                      rec(precondition=true_precond(num_local_vars),
-                          postcondition=false_postcond(num_local_vars)));
+                    clear_precond(fcx.ccx, a);
+                    set_postcond_false(fcx.ccx, a);
                 }
                 case (some[@expr](?ret_val)) {
                     find_pre_post_expr(fcx, ret_val);
-                    let pre_and_post pp =
-                        rec(precondition=expr_precond(ret_val),
-                            postcondition=false_postcond(num_local_vars));
-                    set_pre_and_post(a, pp);
+                    set_precondition(ann_to_ts_ann(fcx.ccx, a),
+                                     expr_precond(fcx.ccx, ret_val));
+                    set_postcond_false(fcx.ccx, a);
                 }
             }
         }
         case (expr_be(?e, ?a)) {
             find_pre_post_expr(fcx, e);
-            set_pre_and_post(a,
-               rec(precondition=expr_prestate(e),
-                   postcondition=false_postcond(num_local_vars)));
+            set_pre_and_post(fcx.ccx, a,
+               expr_prestate(fcx.ccx, e),
+               false_postcond(num_local_vars));
         }
         case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) {
             find_pre_post_expr(fcx, antec);
             find_pre_post_block(fcx, conseq);
             alt (maybe_alt) {
                 case (none[@expr]) {
+                    log "333";
                     auto precond_res = seq_preconds(enclosing,
-                                                    [expr_pp(antec),
-                                                        block_pp(conseq)]);
-                    set_pre_and_post(a, rec(precondition=precond_res,
-                                            postcondition=
-                                            expr_poststate(antec)));
+                                         [expr_pp(fcx.ccx, antec),
+                                          block_pp(fcx.ccx, conseq)]);
+                    set_pre_and_post(fcx.ccx, a, precond_res,
+                                     expr_poststate(fcx.ccx, antec));
                 }
                 case (some[@expr](?altern)) {
                     find_pre_post_expr(fcx, altern);
+                    log "444";
                     auto precond_true_case =
                         seq_preconds(enclosing,
-                                     [expr_pp(antec), block_pp(conseq)]);
+                                     [expr_pp(fcx.ccx, antec),
+                                      block_pp(fcx.ccx, conseq)]);
                     auto postcond_true_case = union_postconds
                         (num_local_vars,
-                         [expr_postcond(antec), block_postcond(conseq)]);
+                         [expr_postcond(fcx.ccx, antec),
+                          block_postcond(fcx.ccx, conseq)]);
+                    log "555";
                     auto precond_false_case = seq_preconds
                         (enclosing,
-                         [expr_pp(antec), expr_pp(altern)]);
+                         [expr_pp(fcx.ccx, antec), expr_pp(fcx.ccx, altern)]);
                     auto postcond_false_case = union_postconds
                         (num_local_vars,
-                         [expr_postcond(antec), expr_postcond(altern)]);
+                         [expr_postcond(fcx.ccx, antec),
+                          expr_postcond(fcx.ccx, altern)]);
                     auto precond_res = union_postconds
                         (num_local_vars,
                          [precond_true_case, precond_false_case]);
                     auto postcond_res = intersect_postconds
                         ([postcond_true_case, postcond_false_case]);
-                    set_pre_and_post(a, rec(precondition=precond_res,
-                                            postcondition=postcond_res));
+                    set_pre_and_post(fcx.ccx, a, precond_res, postcond_res);
                 }
             }
         }
@@ -438,41 +448,42 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
         }
         case (expr_unary(_,?operand,?a)) {
             find_pre_post_expr(fcx, operand);
-            set_pre_and_post(a, expr_pp(operand));
+            copy_pre_post(fcx.ccx, a, operand);
         }
         case (expr_cast(?operand, _, ?a)) {
             find_pre_post_expr(fcx, operand);
-            set_pre_and_post(a, expr_pp(operand));
+            copy_pre_post(fcx.ccx, a, operand);
         }
         case (expr_while(?test, ?body, ?a)) {
             find_pre_post_expr(fcx, test);
             find_pre_post_block(fcx, body);
-            set_pre_and_post(a,
-              rec(precondition=
+            log "666";
+            set_pre_and_post(fcx.ccx, a,
                     seq_preconds(enclosing,
-                               [expr_pp(test), 
-                                   block_pp(body)]),
-                  postcondition=
-                    intersect_postconds([expr_postcond(test),
-                                            block_postcond(body)])));
+                               [expr_pp(fcx.ccx, test), 
+                                   block_pp(fcx.ccx, body)]),
+                    intersect_postconds([expr_postcond(fcx.ccx, test),
+                                         block_postcond(fcx.ccx, body)]));
         }
         case (expr_do_while(?body, ?test, ?a)) {
             find_pre_post_block(fcx, body);
             find_pre_post_expr(fcx, test);
    
             auto loop_postcond = union_postconds(num_local_vars,
-                   [block_postcond(body), expr_postcond(test)]);
+                   [block_postcond(fcx.ccx, body),
+                    expr_postcond(fcx.ccx, 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,
-                                            [block_pp(body),
-                                                expr_pp(test)]),
-                  postcondition=loop_postcond));
+            log "777";
+            set_pre_and_post(fcx.ccx, a, 
+              seq_preconds(enclosing,
+                           [block_pp(fcx.ccx, body),
+                            expr_pp(fcx.ccx, test)]),
+              loop_postcond);
         }
         case (expr_for(?d, ?index, ?body, ?a)) {
             find_pre_post_loop(fcx, d, index, body, a);
@@ -487,47 +498,49 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
             find_pre_post_expr(fcx, e);
             fn do_an_alt(&fn_ctxt fcx, &arm an_alt) -> pre_and_post {
                 find_pre_post_block(fcx, an_alt.block);
-                ret block_pp(an_alt.block);
+                ret block_pp(fcx.ccx, an_alt.block);
             }
             auto f = bind do_an_alt(fcx, _);
             auto alt_pps = vec::map[arm, pre_and_post](f, alts);
             fn combine_pp(pre_and_post antec, 
                           fn_info enclosing, &pre_and_post pp,
                           &pre_and_post next) -> pre_and_post {
+                log "777";
                 union(pp.precondition, seq_preconds(enclosing,
                                                     [antec, next]));
                 intersect(pp.postcondition, next.postcondition);
                 ret pp;
             }
-            auto antec_pp = pp_clone(expr_pp(e)); 
-            auto e_pp  = rec(precondition=empty_prestate(num_local_vars),
+            auto antec_pp = pp_clone(expr_pp(fcx.ccx, e)); 
+            auto e_pp  = @rec(precondition=empty_prestate(num_local_vars),
                              postcondition=false_postcond(num_local_vars));
             auto g = bind combine_pp(antec_pp, fcx.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);
+            set_pre_and_post(fcx.ccx, a, alts_overall_pp.precondition,
+                             alts_overall_pp.postcondition);
         }
         case (expr_field(?operator, _, ?a)) {
             find_pre_post_expr(fcx, operator);
-            set_pre_and_post(a, expr_pp(operator));
+            copy_pre_post(fcx.ccx, a, operator);
         }
         case (expr_fail(?a)) {
-            set_pre_and_post(a,
+            set_pre_and_post(fcx.ccx, a,
                              /* if execution continues after fail,
                                 then everything is true! */
-               rec(precondition=empty_prestate(num_local_vars),
-                   postcondition=false_postcond(num_local_vars)));
+               empty_prestate(num_local_vars),
+               false_postcond(num_local_vars));
         }
         case (expr_assert(?p, ?a)) {
             find_pre_post_expr(fcx, p);
-            set_pre_and_post(a, expr_pp(p));
+            copy_pre_post(fcx.ccx, a, p);
         }
         case (expr_check(?p, ?a)) {
             /* will need to change when we support arbitrary predicates... */
             find_pre_post_expr(fcx, p);
-            set_pre_and_post(a, expr_pp(p));
+            copy_pre_post(fcx.ccx, a, p);
         }
         case(expr_bind(?operator, ?maybe_args, ?a)) {
             auto args = vec::cat_options[@expr](maybe_args);
@@ -535,17 +548,17 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
             find_pre_post_exprs(fcx, args, a);
         }
         case (expr_break(?a)) {
-            set_pre_and_post(a, empty_pre_post(num_local_vars));
+            clear_pp(expr_pp(fcx.ccx, e));
         }
         case (expr_cont(?a)) {
-            set_pre_and_post(a, empty_pre_post(num_local_vars));
+            clear_pp(expr_pp(fcx.ccx, e));
         }
         case (expr_port(?a)) {
-            set_pre_and_post(a, empty_pre_post(num_local_vars));
+            clear_pp(expr_pp(fcx.ccx, e));
         }
         case (expr_ext(_, _, _, ?expanded, ?a)) {
             find_pre_post_expr(fcx, expanded);
-            set_pre_and_post(a, expr_pp(expanded));
+            copy_pre_post(fcx.ccx, a, expanded);
         }
     }
 }
@@ -565,12 +578,11 @@ fn find_pre_post_stmt(&fn_ctxt fcx, &stmt s)
                     alt(alocal.init) {
                         case(some[initializer](?an_init)) {
                             find_pre_post_expr(fcx, an_init.expr);
-                            auto rhs_pp = expr_pp(an_init.expr);
-                            set_pre_and_post(alocal.ann, rhs_pp);
+                            copy_pre_post(fcx.ccx, alocal.ann, an_init.expr);
 
                             /* Inherit ann from initializer, and add var being
                                initialized to the postcondition */
-                            set_pre_and_post(a, rhs_pp);
+                            copy_pre_post(fcx.ccx, a, an_init.expr);
                             /*  log("gen (decl):");
                                 log_stmt(s); */
                             gen(fcx, a, alocal.id); 
@@ -580,22 +592,21 @@ fn find_pre_post_stmt(&fn_ctxt fcx, &stmt s)
                                                    log_pp(stmt_pp(s)); */
                         }
                         case(none[initializer]) {
-                            auto pp = empty_pre_post(num_local_vars);
-                            set_pre_and_post(alocal.ann, pp);
-                            set_pre_and_post(a, pp);
+                            clear_pp(ann_to_ts_ann(fcx.ccx,
+                                                   alocal.ann).conditions);
+                            clear_pp(ann_to_ts_ann(fcx.ccx, a).conditions);
                         }
                     }
                 }
                 case(decl_item(?anitem)) {
-                    auto pp = empty_pre_post(num_local_vars);
-                    set_pre_and_post(a, pp);
+                    clear_pp(ann_to_ts_ann(fcx.ccx, a).conditions);
                     find_pre_post_item(fcx.ccx, *anitem);
                 }
             }
         }
         case(stmt_expr(?e,?a)) {
             find_pre_post_expr(fcx, e);
-            set_pre_and_post(a, expr_pp(e));
+            copy_pre_post(fcx.ccx, a, e);
         }    
     }
 }
@@ -624,7 +635,7 @@ fn find_pre_post_block(&fn_ctxt fcx, block b) -> () {
         log("pre_post for stmt:");
         log_stmt(*s);
         log("is:");
-        log_pp(stmt_pp(*s));
+        log_pp(stmt_pp(fcx.ccx, *s));
     }
     auto do_one = bind do_one_(fcx, _);
     
@@ -637,15 +648,15 @@ fn find_pre_post_block(&fn_ctxt fcx, block b) -> () {
 
     let vec[pre_and_post] pps = [];
 
-    fn get_pp_stmt(&@stmt s) -> pre_and_post {
-        ret stmt_pp(*s);
+    fn get_pp_stmt(crate_ctxt ccx, &@stmt s) -> pre_and_post {
+        ret stmt_pp(ccx, *s);
     }
-    auto f = get_pp_stmt;
+    auto f = bind get_pp_stmt(fcx.ccx,_);
     pps += vec::map[@stmt, pre_and_post](f, b.node.stmts);
-    fn get_pp_expr(&@expr e) -> pre_and_post {
-        ret expr_pp(e);
+    fn get_pp_expr(crate_ctxt ccx, &@expr e) -> pre_and_post {
+        ret expr_pp(ccx, e);
     }
-    auto g = get_pp_expr;
+    auto g = bind get_pp_expr(fcx.ccx, _);
     plus_option[pre_and_post](pps,
        option::map[@expr, pre_and_post](g, b.node.expr));
 
@@ -661,8 +672,7 @@ fn find_pre_post_block(&fn_ctxt fcx, block b) -> () {
         block_postcond = union_postconds(nv, postconds);
     }
 
-    set_pre_and_post(b.node.a, rec(precondition=block_precond,
-                                   postcondition=block_postcond));
+    set_pre_and_post(fcx.ccx, b.node.a, block_precond, block_postcond);
 }
 
 fn find_pre_post_fn(&fn_ctxt fcx, &_fn f) -> () {
diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs
index 9352541ae78..9c0ca53410e 100644
--- a/src/comp/middle/tstate/states.rs
+++ b/src/comp/middle/tstate/states.rs
@@ -17,7 +17,6 @@ import tstate::ann::empty_poststate;
 import tstate::ann::require_and_preserve;
 import tstate::ann::union;
 import tstate::ann::intersect;
-import tstate::ann::pp_clone;
 import tstate::ann::empty_prestate;
 import tstate::ann::prestate;
 import tstate::ann::poststate;
@@ -181,7 +180,7 @@ fn seq_states(&fn_ctxt fcx, prestate pres, vec[@expr] exprs)
 
   for (@expr e in exprs) {
     changed = find_pre_post_state_expr(fcx, post, e) || changed;
-    post = expr_poststate(e);
+    post = expr_poststate(fcx.ccx, e);
   }
 
   ret tup(changed, post);
@@ -191,8 +190,8 @@ fn find_pre_post_state_exprs(&fn_ctxt fcx, &prestate pres,
                              &ann a, &vec[@expr] es) -> bool {
     auto res = seq_states(fcx, pres, es);
     auto changed = res._0;
-    changed = extend_prestate_ann(a, pres) || changed;
-    changed = extend_poststate_ann(a, res._1) || changed;
+    changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
+    changed = extend_poststate_ann(fcx.ccx, a, res._1) || changed;
     ret changed;
 }
 
@@ -201,16 +200,16 @@ fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@decl d,
     auto changed = false;
 
     /* same issues as while */
-    changed = extend_prestate_ann(a, pres) || changed;
+    changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
     changed = find_pre_post_state_expr(fcx, pres, index) || changed;
     /* in general, would need the intersection of
        (poststate of index, poststate of body) */
-    changed = find_pre_post_state_block(fcx, expr_poststate(index), body)
-                || changed;
-    auto res_p = intersect_postconds([expr_poststate(index),
-                                         block_poststate(body)]);
+    changed = find_pre_post_state_block(fcx,
+                expr_poststate(fcx.ccx, index), body) || changed;
+    auto res_p = intersect_postconds([expr_poststate(fcx.ccx, index),
+                                         block_poststate(fcx.ccx, body)]);
   
-    changed = extend_poststate_ann(a, res_p) || changed;
+    changed = extend_poststate_ann(fcx.ccx, a, res_p) || changed;
     ret changed;
 }
 
@@ -245,83 +244,85 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
         || changed;
       /* rands go left-to-right */
       changed = find_pre_post_state_exprs(fcx,
-                                    expr_poststate(operator), a, operands)
-          || changed;
+                  expr_poststate(fcx.ccx, operator), a, operands) || changed;
       /* if this is a failing call, it sets the return value */
        alt (controlflow_expr(fcx.ccx, operator)) {
           case (noreturn) {
-	    /*
-	    log_err("Call that might fail! to");
-	    log_expr_err(*operator);
-	    */
-	    changed = gen_poststate(fcx, a, fcx.id) || changed;
+            /*
+            log_err("Call that might fail! to");
+            log_expr_err(*operator);
+            */
+            changed = gen_poststate(fcx, a, fcx.id) || changed;
           }
           case (_) { 
-	    /*	    log_err("non-failing call, to:");
-	    log_expr_err(*operator);
-	    */
-	  }
+            /*      log_err("non-failing call, to:");
+            log_expr_err(*operator);
+            */
+          }
       }
       ret changed;
     }
     case (expr_spawn(_, _, ?operator, ?operands, ?a)) {
         changed = find_pre_post_state_expr(fcx, pres, operator);
         ret(find_pre_post_state_exprs(fcx,
-                 expr_poststate(operator), a, operands)
+                 expr_poststate(fcx.ccx, operator), a, operands)
           || changed);
     }
     case (expr_bind(?operator, ?maybe_args, ?a)) {
         changed = find_pre_post_state_expr(fcx, pres, operator)
             || changed;
         ret (find_pre_post_state_exprs(fcx,
-          expr_poststate(operator), a, cat_options[@expr](maybe_args))
-            || changed);
+          expr_poststate(fcx.ccx, operator), a,
+             cat_options[@expr](maybe_args)) || changed);
     }
     case (expr_path(_,?a)) {
-      ret pure_exp(a, pres);
+      ret pure_exp(fcx.ccx, a, pres);
     }
     case (expr_log(_,?e,?a)) {
         /* factor out the "one exp" pattern */
         changed = find_pre_post_state_expr(fcx, pres, e);
-        changed = extend_prestate_ann(a, pres) || changed;
-        changed = extend_poststate_ann(a, expr_poststate(e)) || changed;
+        changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
+        changed = extend_poststate_ann(fcx.ccx, a,
+                    expr_poststate(fcx.ccx, e)) || changed;
         ret changed;
     }
     case (expr_chan(?e, ?a)) {
         changed = find_pre_post_state_expr(fcx, pres, e);
-        changed = extend_prestate_ann(a, pres) || changed;
-        changed = extend_poststate_ann(a, expr_poststate(e)) || changed;
+        changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
+        changed = extend_poststate_ann(fcx.ccx, a,
+                    expr_poststate(fcx.ccx, e)) || changed;
         ret changed;
     }
     case (expr_ext(_, _, _, ?expanded, ?a)) {
         changed = find_pre_post_state_expr(fcx, pres, expanded);
-        changed = extend_prestate_ann(a, pres) || changed;
-        changed = extend_poststate_ann(a, expr_poststate(expanded))
-           || changed;
+        changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
+        changed = extend_poststate_ann(fcx.ccx, a,
+                    expr_poststate(fcx.ccx, expanded)) || changed;
         ret changed;
     }
     case (expr_put(?maybe_e, ?a)) {
         alt (maybe_e) {
             case (some[@expr](?arg)) {
                 changed = find_pre_post_state_expr(fcx, pres, arg);
-                changed = extend_prestate_ann(a, pres) || changed;
-                changed = extend_poststate_ann(a, expr_poststate(arg))
-                    || changed;
+                changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
+                changed = extend_poststate_ann(fcx.ccx, a,
+                            expr_poststate(fcx.ccx, arg)) || changed;
                 ret changed;
             }
             case (none[@expr]) {
-                ret pure_exp(a, pres);
+                ret pure_exp(fcx.ccx, a, pres);
             }
         }
     }
     case (expr_lit(?l,?a)) {
-        ret pure_exp(a, pres);
+        ret pure_exp(fcx.ccx, a, pres);
     }
     case (expr_block(?b,?a)) {
         changed = find_pre_post_state_block(fcx, pres, b)
            || changed;
-        changed = extend_prestate_ann(a, pres) || changed;
-        changed = extend_poststate_ann(a, block_poststate(b)) || changed;
+        changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
+        changed = extend_poststate_ann(fcx.ccx, a,
+                    block_poststate(fcx.ccx, b)) || changed;
         ret changed;
     }
     case (expr_rec(?fields,?maybe_base,?a)) {
@@ -332,23 +333,23 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
             case (some[@expr](?base)) {
                 changed = find_pre_post_state_expr(fcx, pres, base)
                     || changed;
-                changed = extend_poststate_ann(a, expr_poststate(base))
-                    || changed;
+                changed = extend_poststate_ann(fcx.ccx, a,
+                            expr_poststate(fcx.ccx, base)) || changed;
             }
         }
         ret changed;
     }
     case (expr_assign(?lhs, ?rhs, ?a)) {
-        extend_prestate_ann(a, pres);
+        extend_prestate_ann(fcx.ccx, a, pres);
 
         alt (lhs.node) {
             case (expr_path(?p, ?a_lhs)) {
                 // assignment to local var
-                changed = pure_exp(a_lhs, pres) || changed;
+                changed = pure_exp(fcx.ccx, a_lhs, pres) || changed;
                 changed = find_pre_post_state_expr(fcx, pres, rhs)
                     || changed;
-                changed = extend_poststate_ann(a, expr_poststate(rhs))
-                    || changed;
+                changed = extend_poststate_ann(fcx.ccx, a,
+                            expr_poststate(fcx.ccx, rhs)) || changed;
                 changed = gen_if_local(fcx, a_lhs, a)|| changed;
             }
             case (_) {
@@ -356,24 +357,24 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
                 changed = find_pre_post_state_expr(fcx, pres, lhs)
                     || changed;
                 changed = find_pre_post_state_expr(fcx,
-                     expr_poststate(lhs), rhs) || changed;
-                changed = extend_poststate_ann(a, expr_poststate(rhs))
-                    || changed;
+                     expr_poststate(fcx.ccx, lhs), rhs) || changed;
+                changed = extend_poststate_ann(fcx.ccx, a,
+                            expr_poststate(fcx.ccx, rhs)) || changed;
             }
         }
         ret changed;
     }
     case (expr_recv(?lhs, ?rhs, ?a)) {
-        extend_prestate_ann(a, pres);
+        extend_prestate_ann(fcx.ccx, a, pres);
 
         alt (lhs.node) {
             case (expr_path(?p, ?a_lhs)) {
                 // receive to local var
-                changed = pure_exp(a_lhs, pres) || changed;
+                changed = pure_exp(fcx.ccx, a_lhs, pres) || changed;
                 changed = find_pre_post_state_expr(fcx, pres, rhs)
                     || changed;
-                changed = extend_poststate_ann(a, expr_poststate(rhs))
-                    || changed;
+                changed = extend_poststate_ann(fcx.ccx, a,
+                            expr_poststate(fcx.ccx, rhs)) || changed;
                 changed = gen_if_local(fcx, a_lhs, a) || changed;
             }
             case (_) {
@@ -381,17 +382,17 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
                 changed = find_pre_post_state_expr(fcx, pres, lhs)
                     || changed;
                 changed = find_pre_post_state_expr(fcx,
-                     expr_poststate(lhs), rhs) || changed;
-                changed = extend_poststate_ann(a, expr_poststate(rhs))
-                    || changed;
+                     expr_poststate(fcx.ccx, lhs), rhs) || changed;
+                changed = extend_poststate_ann(fcx.ccx, a,
+                            expr_poststate(fcx.ccx, rhs)) || changed;
             }
         }
         ret changed;
     }
 
     case (expr_ret(?maybe_ret_val, ?a)) {
-        changed = extend_prestate_ann(a, pres) || changed;
-        set_poststate_ann(a, false_postcond(num_local_vars));
+        changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
+        set_poststate_ann(fcx.ccx, a, false_postcond(num_local_vars));
         alt(maybe_ret_val) {
             case (none[@expr]) { /* do nothing */ }
             case (some[@expr](?ret_val)) {
@@ -402,28 +403,30 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
         ret changed;
     }
     case (expr_be(?e, ?a)) {
-        changed = extend_prestate_ann(a, pres) || changed;
-        set_poststate_ann(a, false_postcond(num_local_vars));
+        changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
+        set_poststate_ann(fcx.ccx, a, false_postcond(num_local_vars));
         changed = find_pre_post_state_expr(fcx, pres, e) || changed;
         ret changed;
     }
     case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) {
-        changed = extend_prestate_ann(a, pres) || changed;
+        changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
         changed = find_pre_post_state_expr(fcx, pres, antec)
             || changed;
         changed = find_pre_post_state_block(fcx,
-          expr_poststate(antec), conseq) || changed;
+          expr_poststate(fcx.ccx, antec), conseq) || changed;
         alt (maybe_alt) {
             case (none[@expr]) {
-                changed = extend_poststate_ann(a, expr_poststate(antec))
-                    || changed;
+                changed = extend_poststate_ann(fcx.ccx, a,
+                            expr_poststate(fcx.ccx, antec)) || changed;
             }
             case (some[@expr](?altern)) {
                 changed = find_pre_post_state_expr(fcx,
-                   expr_poststate(antec), altern) || changed;
+                   expr_poststate(fcx.ccx, antec), altern) || changed;
                 auto poststate_res = intersect_postconds
-                    ([block_poststate(conseq), expr_poststate(altern)]);
-                changed = extend_poststate_ann(a, poststate_res) || changed;
+                    ([block_poststate(fcx.ccx, conseq),
+                      expr_poststate(fcx.ccx, altern)]);
+                changed = extend_poststate_ann(fcx.ccx, a, poststate_res)
+                            || changed;
             }
         }
         log("if:");
@@ -431,41 +434,44 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
         log("new prestate:");
         log_bitv(fcx.enclosing, pres);
         log("new poststate:");
-        log_bitv(fcx.enclosing, expr_poststate(e));
+        log_bitv(fcx.enclosing, expr_poststate(fcx.ccx, e));
 
         ret changed;
     }
     case (expr_binary(?bop, ?l, ?r, ?a)) {
         /* FIXME: what if bop is lazy? */
-        changed = extend_prestate_ann(a, pres) || changed;
+        changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
         changed = find_pre_post_state_expr(fcx, pres, l)
                     || changed;
-        changed = find_pre_post_state_expr(fcx, expr_poststate(l), r)
+        changed = find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, l), r)
                     || changed;
-        changed = extend_poststate_ann(a, expr_poststate(r)) || changed;
+        changed = extend_poststate_ann(fcx.ccx, a,
+                    expr_poststate(fcx.ccx, r)) || changed;
         ret changed;
     }
     case (expr_send(?l, ?r, ?a)) {
-        changed = extend_prestate_ann(a, pres) || changed;
+        changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
         changed = find_pre_post_state_expr(fcx, pres, l)
                     || changed;
-        changed = find_pre_post_state_expr(fcx, expr_poststate(l), r)
+        changed = find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, l), r)
                     || changed;
-        changed = extend_poststate_ann(a, expr_poststate(r)) || changed;
+        changed = extend_poststate_ann(fcx.ccx, a,
+                    expr_poststate(fcx.ccx, 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 = extend_prestate_ann(fcx.ccx, a, pres) || changed;
         changed = find_pre_post_state_expr(fcx, pres, lhs)
                     || changed;
-        changed = find_pre_post_state_expr(fcx, expr_poststate(lhs), rhs)
-                    || changed;
-        changed = extend_poststate_ann(a, expr_poststate(rhs)) || changed;
+        changed = find_pre_post_state_expr(fcx,
+                    expr_poststate(fcx.ccx, lhs), rhs) || changed;
+        changed = extend_poststate_ann(fcx.ccx, a,
+                    expr_poststate(fcx.ccx, rhs)) || changed;
         ret changed;
     }
     case (expr_while(?test, ?body, ?a)) {
-        changed = extend_prestate_ann(a, pres) || changed;
+        changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
         /* to handle general predicates, we need to pass in
             pres `intersect` (poststate(a)) 
          like: auto test_pres = intersect_postconds(pres, expr_postcond(a));
@@ -476,30 +482,30 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
         */
         changed = find_pre_post_state_expr(fcx, pres, test)
             || changed;
-        changed = find_pre_post_state_block(fcx, expr_poststate(test), body)
-                    || changed; 
-        changed = extend_poststate_ann(a,
-                    intersect_postconds([expr_poststate(test),
-                                        block_poststate(body)])) || changed;
+        changed = find_pre_post_state_block(fcx,
+                    expr_poststate(fcx.ccx, test), body) || changed; 
+        changed = extend_poststate_ann(fcx.ccx, a,
+                    intersect_postconds([expr_poststate(fcx.ccx, test),
+                      block_poststate(fcx.ccx, body)])) || changed;
         ret changed;
     }
     case (expr_do_while(?body, ?test, ?a)) {
-        changed = extend_prestate_ann(a, pres) || changed;
+        changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
         changed = find_pre_post_state_block(fcx, pres, body)
             || changed;
         changed = find_pre_post_state_expr(fcx,
-                     block_poststate(body), test) || changed;
+                     block_poststate(fcx.ccx, 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;
+            changed = set_poststate_ann(fcx.ccx, a, pres) || changed;
         }
         else {
-            changed = extend_poststate_ann(a, expr_poststate(test))
-              || changed;
+            changed = extend_poststate_ann(fcx.ccx, a,
+                        expr_poststate(fcx.ccx, test)) || changed;
         }
 
         ret changed;
@@ -511,155 +517,160 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
         ret find_pre_post_state_loop(fcx, pres, d, index, body, a);
     }
     case (expr_index(?e, ?sub, ?a)) {
-        changed = extend_prestate_ann(a, pres) || changed; 
+        changed = extend_prestate_ann(fcx.ccx, a, pres) || changed; 
         changed = find_pre_post_state_expr(fcx, pres, e) || changed;
         changed = find_pre_post_state_expr(fcx,
-                     expr_poststate(e), sub) || changed;
-        changed = extend_poststate_ann(a, expr_poststate(sub));
+                     expr_poststate(fcx.ccx, e), sub) || changed;
+        changed = extend_poststate_ann(fcx.ccx, a,
+                                       expr_poststate(fcx.ccx, sub));
         ret changed;
     }
     case (expr_alt(?e, ?alts, ?a)) {
-        changed = extend_prestate_ann(a, pres) || changed; 
+        changed = extend_prestate_ann(fcx.ccx, a, pres) || changed; 
         changed = find_pre_post_state_expr(fcx, pres, e) || changed;
-        auto e_post = expr_poststate(e);
+        auto e_post = expr_poststate(fcx.ccx, e);
         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(fcx, e_post,
                                                     an_alt.block) || changed;
-                changed = intersect(a_post, block_poststate(an_alt.block))
-                    || changed; 
+                changed = intersect(a_post,
+                            block_poststate(fcx.ccx,
+                                            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);
+        changed = extend_poststate_ann(fcx.ccx, a, a_post);
         ret changed;
     }
     case (expr_field(?e, _, ?a)) {
         changed = find_pre_post_state_expr(fcx, pres, e);
-        changed = extend_prestate_ann(a, pres) || changed;
-        changed = extend_poststate_ann(a, expr_poststate(e)) || changed;
+        changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
+        changed = extend_poststate_ann(fcx.ccx, a,
+                    expr_poststate(fcx.ccx, e)) || changed;
         ret changed;
     }
     case (expr_unary(_,?operand,?a)) {
         changed = find_pre_post_state_expr(fcx, pres, operand)
           || changed;
-        changed = extend_prestate_ann(a, pres) || changed;
-        changed = extend_poststate_ann(a, expr_poststate(operand))
-          || changed;
+        changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
+        changed = extend_poststate_ann(fcx.ccx, a,
+                    expr_poststate(fcx.ccx, operand)) || changed;
         ret changed;
     }
     case (expr_cast(?operand, _, ?a)) {
            changed = find_pre_post_state_expr(fcx, pres, operand)
           || changed;
-        changed = extend_prestate_ann(a, pres) || changed;
-        changed = extend_poststate_ann(a, expr_poststate(operand))
-          || changed;
+        changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
+        changed = extend_poststate_ann(fcx.ccx, a,
+                    expr_poststate(fcx.ccx, operand)) || changed;
         ret changed;
     }
     case (expr_fail(?a)) {
-        changed = extend_prestate_ann(a, pres) || changed;
+        changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
         /* if execution continues after fail, then everything is true! woo! */
-        changed = set_poststate_ann(a, false_postcond(num_local_vars))
-          || changed;
+        changed = set_poststate_ann(fcx.ccx, a,
+                    false_postcond(num_local_vars)) || changed;
         ret changed;
     }
     case (expr_assert(?p, ?a)) {
-        ret pure_exp(a, pres);
+        ret pure_exp(fcx.ccx, a, pres);
     }
     case (expr_check(?p, ?a)) {
-        changed = extend_prestate_ann(a, pres) || changed;
+        changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
         changed = find_pre_post_state_expr(fcx, pres, p) || changed;
         /* FIXME: update the postcondition to reflect that p holds */
-        changed = extend_poststate_ann(a, pres) || changed;
+        changed = extend_poststate_ann(fcx.ccx, a, pres) || changed;
         ret changed;
     }
     case (expr_break(?a)) {
-        ret pure_exp(a, pres);
+        ret pure_exp(fcx.ccx, a, pres);
     }
     case (expr_cont(?a)) {
-        ret pure_exp(a, pres);
+        ret pure_exp(fcx.ccx, a, pres);
     }
     case (expr_port(?a)) {
-        ret pure_exp(a, pres);
+        ret pure_exp(fcx.ccx, a, pres);
     }
     case (expr_self_method(_, ?a)) {
-        ret pure_exp(a, pres);
+        ret pure_exp(fcx.ccx, a, pres);
     }
   }
 }
 
 fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool {
-  auto changed = false;
-  auto stmt_ann_ = stmt_to_ann(*s);
-  assert (!is_none[@ts_ann](stmt_ann_));
-  auto stmt_ann = *(get[@ts_ann](stmt_ann_));
-              log("*At beginning: stmt = ");
-              log_stmt(*s);
-              log("*prestate = ");
-              log(bitv::to_str(stmt_ann.states.prestate));
-              log("*poststate =");
-              log(bitv::to_str(stmt_ann.states.poststate));
-              log("*changed =");
-              log(changed);
+    auto changed = false;
+    auto stmt_ann = stmt_to_ann(fcx.ccx, *s);
+ 
+    log("*At beginning: stmt = ");
+    log_stmt(*s);
+    log("*prestate = ");
+    log(bitv::to_str(stmt_ann.states.prestate));
+    log("*poststate =");
+    log(bitv::to_str(stmt_ann.states.poststate));
+    log("*changed =");
+    log(changed);
   
-  alt (s.node) {
-    case (stmt_decl(?adecl, ?a)) {
-      alt (adecl.node) {
-        case (decl_local(?alocal)) {
-          alt (alocal.init) {
-            case (some[initializer](?an_init)) {
-                changed = extend_prestate(stmt_ann.states.prestate, pres)
-                    || changed;
-                changed = find_pre_post_state_expr
-                    (fcx, pres, an_init.expr) || changed;
-                changed = extend_poststate(stmt_ann.states.poststate,
-                                           expr_poststate(an_init.expr))
-                    || changed;
-                changed = gen_poststate(fcx, a, alocal.id)
-                            || changed;
-              log("Summary: stmt = ");
-              log_stmt(*s);
-              log("prestate = ");
-              log(bitv::to_str(stmt_ann.states.prestate));
-              log_bitv(fcx.enclosing, stmt_ann.states.prestate);
-              log("poststate =");
-              log_bitv(fcx.enclosing, stmt_ann.states.poststate);
-              log("changed =");
-              log(changed);
+    alt (s.node) {
+        case (stmt_decl(?adecl, ?a)) {
+            alt (adecl.node) {
+                case (decl_local(?alocal)) {
+                    alt (alocal.init) {
+                        case (some[initializer](?an_init)) {
+                            changed = extend_prestate
+                                (stmt_ann.states.prestate, pres) || changed;
+                            changed = find_pre_post_state_expr
+                                (fcx, pres, an_init.expr) || changed;
+                            changed = extend_poststate
+                                (stmt_ann.states.poststate,
+                                 expr_poststate(fcx.ccx, an_init.expr))
+                                || changed;
+                            changed = gen_poststate(fcx, a, alocal.id)
+                                || changed;
+                            log("Summary: stmt = ");
+                            log_stmt(*s);
+                            log("prestate = ");
+                            log(bitv::to_str(stmt_ann.states.prestate));
+                            log_bitv(fcx.enclosing, stmt_ann.states.prestate);
+                            log("poststate =");
+                            log_bitv(fcx.enclosing,
+                                     stmt_ann.states.poststate);
+                            log("changed =");
+                            log(changed);
   
-              ret changed;
-            }
-            case (none[initializer]) {
-              changed = extend_prestate(stmt_ann.states.prestate, pres)
-                  || changed;
-              changed = extend_poststate(stmt_ann.states.poststate, pres)
-                  || changed;
-              ret changed;
+                            ret changed;
+                        }
+                        case (none[initializer]) {
+                            changed = extend_prestate
+                                (stmt_ann.states.prestate, pres) || changed;
+                            changed = extend_poststate
+                                (stmt_ann.states.poststate, pres) || changed;
+                            ret changed;
+                        }
+                    }
+                }
+                case (decl_item(?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(fcx, an_item) || changed);
+                }
             }
-          }
         }
-        case (decl_item(?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(fcx, an_item) || changed);
-        }
-      }
-    }
-    case (stmt_expr(?e, _)) {
-      changed = find_pre_post_state_expr(fcx, pres, e) || changed;
-      changed = extend_prestate(stmt_ann.states.prestate, expr_prestate(e))
-          || changed;
-      changed = extend_poststate(stmt_ann.states.poststate,
-                                 expr_poststate(e)) || changed;
-      /*
-                    log("Summary: stmt = ");
+        case (stmt_expr(?e, _)) {
+            changed = find_pre_post_state_expr(fcx, pres, e) || changed;
+            changed = extend_prestate(stmt_ann.states.prestate,
+                                      expr_prestate(fcx.ccx, e))
+                || changed;
+            changed = extend_poststate(stmt_ann.states.poststate,
+                                       expr_poststate(fcx.ccx, e)) || changed;
+            /*
+              log("Summary: stmt = ");
               log_stmt(*s);
               log("prestate = ");
               log(bitv::to_str(stmt_ann.states.prestate));
@@ -669,11 +680,11 @@ fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool {
               log_bitv(enclosing, stmt_ann.states.poststate);
               log("changed =");
               log(changed);
-      */
-      ret changed;
+            */
+            ret changed;
+        }
+        case (_) { ret false; }
     }
-    case (_) { ret false; }
-  }
 }
 
 /* Updates the pre- and post-states of statements in the block,
@@ -692,7 +703,7 @@ fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b)
   Then <pres> becomes the new poststate. */ 
   for (@stmt s in b.node.stmts) {
     changed = find_pre_post_state_stmt(fcx, pres, s) || changed;
-    pres = stmt_poststate(*s, num_local_vars);
+    pres = stmt_poststate(fcx.ccx, *s);
   }
 
   auto post = pres;
@@ -701,7 +712,7 @@ fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b)
     case (none[@expr]) {}
     case (some[@expr](?e)) {
       changed = find_pre_post_state_expr(fcx, pres, e) || changed;
-      post = expr_poststate(e);
+      post = expr_poststate(fcx.ccx, e);
     }
   }
 
@@ -718,13 +729,13 @@ fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b)
       post = pres0;
   }
   
-  set_prestate_ann(b.node.a, pres0);
-  set_poststate_ann(b.node.a, post);
+  set_prestate_ann(fcx.ccx, b.node.a, pres0);
+  set_poststate_ann(fcx.ccx, b.node.a, post);
 
   log("For block:");
   log_block(b);
   log("poststate = ");
-  log_states(block_states(b));
+  log_states(block_states(fcx.ccx, b));
   log("pres0:");
   log_bitv(fcx.enclosing, pres0);
   log("post:");
@@ -785,3 +796,14 @@ fn find_pre_post_state_item(&fn_ctxt fcx, @item i) -> bool {
         }
     }
 }
+//
+// 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:
+//
+