In pre/postcondition computation, failing calls should set the postcondition
A non-returning call should have a postcondition in which all predicates are true -- not just a poststate. Otherwise, alt expressions where one or more branches terminate in a non-returning call and others initialize a variable get rejected. Includes a test case.
Showing
src/test/run-pass/nested-alts.rs
0 → 100644
想要评论请 注册 或 登录