aboutsummaryrefslogtreecommitdiff
path: root/src/boot/me
diff options
context:
space:
mode:
authorGraydon Hoare <[email protected]>2010-07-01 10:14:38 -0700
committerGraydon Hoare <[email protected]>2010-07-01 10:14:38 -0700
commit8acb2cf47d4b4c55186d17e15560a8835ad21813 (patch)
tree024919816c2b6b5f4b1d7007925593c7bd1e9d4b /src/boot/me
parentSimplify types before analyzing call structure; 2 more tests compile. (diff)
downloadrust-8acb2cf47d4b4c55186d17e15560a8835ad21813.tar.xz
rust-8acb2cf47d4b4c55186d17e15560a8835ad21813.zip
Add STMT_init_box to typestate pass.
Diffstat (limited to 'src/boot/me')
-rw-r--r--src/boot/me/typestate.ml9
1 files changed, 8 insertions, 1 deletions
diff --git a/src/boot/me/typestate.ml b/src/boot/me/typestate.ml
index 79e47845..e0ebe4ee 100644
--- a/src/boot/me/typestate.ml
+++ b/src/boot/me/typestate.ml
@@ -439,6 +439,12 @@ let condition_assigning_visitor
raise_precondition s.id precond;
raise_postcondition s.id postcond
+ | Ast.STMT_init_box (dst, src) ->
+ let precond = slot_inits (atom_slots cx src) in
+ let postcond = slot_inits (lval_slots cx dst) in
+ raise_precondition s.id precond;
+ raise_postcondition s.id postcond
+
| Ast.STMT_copy (dst, src) ->
let precond = slot_inits (expr_slots cx src) in
let postcond = slot_inits (lval_slots cx dst) in
@@ -995,7 +1001,8 @@ let lifecycle_visitor
| Ast.STMT_init_vec (lv_dst, _)
| Ast.STMT_init_str (lv_dst, _)
| Ast.STMT_init_port lv_dst
- | Ast.STMT_init_chan (lv_dst, _) ->
+ | Ast.STMT_init_chan (lv_dst, _)
+ | Ast.STMT_init_box (lv_dst, _) ->
init_lval lv_dst
| Ast.STMT_for f ->