diff --git a/src/boot/me/typestate.ml b/src/boot/me/typestate.ml index 72df6e38fe0..0f8588decda 100644 --- a/src/boot/me/typestate.ml +++ b/src/boot/me/typestate.ml @@ -391,6 +391,14 @@ let condition_assigning_visitor end in + let raise_dst_init_precond_if_writing_through sid lval = + match lval with + Ast.LVAL_base _ -> () + | Ast.LVAL_ext _ -> + let precond = slot_inits (lval_slots cx lval) in + raise_precondition sid precond; + in + let visit_stmt_pre s = begin match s.node with @@ -402,6 +410,7 @@ let condition_assigning_visitor let precond = slot_inits (lval_slots cx src) in let postcond = slot_inits (lval_slots cx dst) in raise_pre_post_cond s.id precond; + raise_dst_init_precond_if_writing_through s.id dst; raise_postcondition s.id postcond | Ast.STMT_send (dst, src) -> @@ -423,6 +432,7 @@ let condition_assigning_visitor (Array.append (rec_inputs_slots cx entries) base_slots) in let postcond = slot_inits (lval_slots cx dst) in + raise_dst_init_precond_if_writing_through s.id dst; raise_pre_post_cond s.id precond; raise_postcondition s.id postcond @@ -431,38 +441,45 @@ let condition_assigning_visitor (tup_inputs_slots cx modes_atoms) in let postcond = slot_inits (lval_slots cx dst) in + raise_dst_init_precond_if_writing_through s.id dst; raise_pre_post_cond s.id precond; raise_postcondition s.id postcond | Ast.STMT_new_vec (dst, _, atoms) -> let precond = slot_inits (atoms_slots cx atoms) in let postcond = slot_inits (lval_slots cx dst) in + raise_dst_init_precond_if_writing_through s.id dst; raise_pre_post_cond s.id precond; raise_postcondition s.id postcond | Ast.STMT_new_str (dst, _) -> let postcond = slot_inits (lval_slots cx dst) in + raise_dst_init_precond_if_writing_through s.id dst; raise_postcondition s.id postcond | Ast.STMT_new_port dst -> let postcond = slot_inits (lval_slots cx dst) in + raise_dst_init_precond_if_writing_through s.id dst; raise_postcondition s.id postcond | Ast.STMT_new_chan (dst, port) -> let precond = slot_inits (lval_option_slots cx port) in let postcond = slot_inits (lval_slots cx dst) in + raise_dst_init_precond_if_writing_through s.id dst; raise_pre_post_cond s.id precond; raise_postcondition s.id postcond | Ast.STMT_new_box (dst, _, src) -> let precond = slot_inits (atom_slots cx src) in let postcond = slot_inits (lval_slots cx dst) in + raise_dst_init_precond_if_writing_through s.id dst; raise_pre_post_cond 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 + raise_dst_init_precond_if_writing_through s.id dst; raise_pre_post_cond s.id precond; raise_postcondition s.id postcond @@ -474,11 +491,13 @@ let condition_assigning_visitor | Ast.STMT_spawn (dst, _, lv, args) | Ast.STMT_call (dst, lv, args) -> + raise_dst_init_precond_if_writing_through s.id dst; visit_callable_pre s.id (lval_slots cx dst) lv args | Ast.STMT_bind (dst, lv, args_opt) -> let args = arr_map_partial args_opt (fun a -> a) in - visit_callable_pre s.id (lval_slots cx dst) lv args + raise_dst_init_precond_if_writing_through s.id dst; + visit_callable_pre s.id (lval_slots cx dst) lv args | Ast.STMT_ret (Some at) -> let precond = slot_inits (atom_slots cx at) in diff --git a/src/test/compile-fail/writing-through-uninit-vec.rs b/src/test/compile-fail/writing-through-uninit-vec.rs new file mode 100644 index 00000000000..55edbf87875 --- /dev/null +++ b/src/test/compile-fail/writing-through-uninit-vec.rs @@ -0,0 +1,10 @@ +// error-pattern: Unsatisfied precondition constraint + +fn test() { + let vec[int] w; + w.(5) = 0; +} + +fn main() { + test(); +} \ No newline at end of file