Implemented computing prestates and poststates for a few expression forms.

The typestate checker (if it's uncommented) now correctly rejects a
trivial example program that has an uninitialized variable.

2 files changed, 25 insertions, 1 deletions

diff --git a/src/comp/util/common.rs b/src/comp/util/common.rs
index 5243e2f7..6dec6c00 100644
--- a/src/comp/util/common.rs
+++ b/src/comp/util/common.rs
@@ -1,5 +1,6 @@
 import std._uint;
 import std._int;
+import std._vec;
 import front.ast;
 
 
@@ -75,6 +76,17 @@ fn istr(int i) -> str {
     ret _int.to_str(i, 10u);
 }
 
+fn uistr(uint i) -> str {
+    ret _uint.to_str(i, 10u);
+}
+
+fn elt_expr(&ast.elt e) -> @ast.expr { ret e.expr; }
+
+fn elt_exprs(vec[ast.elt] elts) -> vec[@ast.expr] {
+    auto f = elt_expr;
+    be _vec.map[ast.elt, @ast.expr](f, elts);
+}
+
 //
 // Local Variables:
 // mode: rust
diff --git a/src/comp/util/typestate_ann.rs b/src/comp/util/typestate_ann.rs
index 53f9a71c..c8d23321 100644
--- a/src/comp/util/typestate_ann.rs
+++ b/src/comp/util/typestate_ann.rs
@@ -104,6 +104,18 @@ impure fn set_postcondition(&ts_ann a, &postcond p) -> () {
   bitv.copy(p, a.conditions.postcondition);
 }
 
+// Sets all the bits in a's prestate to equal the
+// corresponding bit in p's prestate.
+impure fn set_prestate(&ts_ann a, &prestate p) -> () {
+  bitv.copy(p, a.states.prestate);
+}
+
+// Sets all the bits in a's postcondition to equal the
+// corresponding bit in p's postcondition.
+impure fn set_poststate(&ts_ann a, &poststate p) -> () {
+  bitv.copy(p, a.states.poststate);
+}
+
 // Set all the bits in p that are set in new
 impure fn extend_prestate(&prestate p, &poststate new) -> () {
   bitv.union(p, new);
@@ -119,5 +131,5 @@ fn ann_prestate(&ts_ann a) -> prestate {
 
 impure fn implies(bitv.t a, bitv.t b) -> bool {
   bitv.difference(b, a);
-  be bitv.is_false(b);
+  ret bitv.is_false(b);
 }