diff options
| author | Tim Chevalier <chevalier@alum.wellesley.edu> | 2011-05-27 20:41:48 -0700 |
|---|---|---|
| committer | Tim Chevalier <chevalier@alum.wellesley.edu> | 2011-05-27 20:43:51 -0700 |
| commit | 18883fea3a5c3c1a9af5c8a29464b83c0c81757b (patch) | |
| tree | 355d1b0e7abcc71db42767832f43edcbe3f833b2 /src/rt/rust_log.cpp | |
| parent | 95e1aa18c1290d087516bd417590a181300cfc6b (diff) | |
| download | rust-18883fea3a5c3c1a9af5c8a29464b83c0c81757b.tar.gz rust-18883fea3a5c3c1a9af5c8a29464b83c0c81757b.zip | |
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.
Diffstat (limited to 'src/rt/rust_log.cpp')
0 files changed, 0 insertions, 0 deletions