From 9a24e4f78045bc32a9eec7c7486a9e0dc7b2b78f Mon Sep 17 00:00:00 2001
From: Tim Chevalier <chevalier@alum.wellesley.edu>
Date: Fri, 27 May 2011 17:01:37 -0700
Subject: [PATCH] Fix two typestate bugs

* Non-returning calls should set all predicates to be true, not
  just the "this function returns" predicate

* Fixed a bug in the expr_alt case in tstate.states that wasn't updating
  the changed flag properly, then fixed *another* bug that was updating
  it too enthusiastically, but was masked by the first bug.
---
 src/comp/middle/tstate/states.rs | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs
index 10dc882166a5..8c317490f37f 100644
--- a/src/comp/middle/tstate/states.rs
+++ b/src/comp/middle/tstate/states.rs
@@ -215,10 +215,10 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
   auto changed = false;
   auto num_local_vars = num_locals(fcx.enclosing);
 
-  /*
+  /*  
   log_err("states:");
   log_expr_err(*e);
-  log_err(middle::ty::expr_ann(e).id);
+  aux::log_bitv_err(fcx, expr_poststate(fcx.ccx, e));
   */
 
   /* FIXME could get rid of some of the copy/paste */
@@ -236,10 +236,12 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
       /* rands go left-to-right */
       changed = find_pre_post_state_exprs(fcx,
                   expr_poststate(fcx.ccx, operator), a, operands) || changed;
-      /* if this is a failing call, it sets the return value */
+      /* if this is a failing call, it sets everything as initialized */
        alt (controlflow_expr(fcx.ccx, operator)) {
           case (noreturn) {
-            changed = gen_poststate(fcx, a, fcx.id) || changed;
+              changed = set_poststate_ann(fcx.ccx, a,
+                                          false_postcond(num_local_vars))
+                  || changed;
           }
           case (_) { }
       }
@@ -525,16 +527,17 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
             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(fcx.ccx,
-                                            an_alt.block)) || changed; 
+                intersect(a_post, block_poststate(fcx.ccx, an_alt.block));
+                // We deliberately do *not* update changed here, because we'd
+                // go into an infinite loop that way, and the change gets made
+                // after the if expression.
             }
         }
         else {
             // No alts; poststate is the poststate of the test
             a_post = e_post;
         }
-        changed = extend_poststate_ann(fcx.ccx, a, a_post);
+        changed = extend_poststate_ann(fcx.ccx, a, a_post) || changed;
         ret changed;
     }
     case (expr_field(?e, _, ?a)) {