@@ -39,6 +39,7 @@ import aux::ann_to_def;
39
39
import aux:: ann_to_def_strict;
40
40
import aux:: ann_to_ts_ann;
41
41
import aux:: set_postcond_false;
42
+ import aux:: controlflow_expr;
42
43
43
44
import bitvectors:: seq_preconds;
44
45
import bitvectors:: union_postconds;
@@ -78,6 +79,7 @@ import front::ast::def;
78
79
import front:: ast:: lit;
79
80
import front:: ast:: init_op;
80
81
import front:: ast:: controlflow;
82
+ import front:: ast:: noreturn;
81
83
import front:: ast:: return;
82
84
import front:: ast:: _fn;
83
85
import front:: ast:: _obj;
@@ -294,6 +296,13 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
294
296
auto args = vec:: clone[ @expr] ( operands) ;
295
297
vec:: push[ @expr] ( args, operator) ;
296
298
find_pre_post_exprs ( fcx, args, a) ;
299
+ /* if this is a failing call, its postcondition sets everything */
300
+ alt ( controlflow_expr ( fcx. ccx , operator) ) {
301
+ case ( noreturn) {
302
+ set_postcond_false ( fcx. ccx , a) ;
303
+ }
304
+ case ( _) { }
305
+ }
297
306
}
298
307
case ( expr_spawn ( _, _, ?operator, ?operands, ?a) ) {
299
308
auto args = vec:: clone[ @expr] ( operands) ;
@@ -495,8 +504,8 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
495
504
case ( expr_index ( ?e, ?sub, ?a) ) {
496
505
find_pre_post_exprs ( fcx, [ e, sub] , a) ;
497
506
}
498
- case ( expr_alt ( ?e , ?alts, ?a) ) {
499
- find_pre_post_expr ( fcx, e ) ;
507
+ case ( expr_alt ( ?ex , ?alts, ?a) ) {
508
+ find_pre_post_expr ( fcx, ex ) ;
500
509
fn do_an_alt ( & fn_ctxt fcx, & arm an_alt ) -> pre_and_post {
501
510
find_pre_post_block ( fcx, an_alt. block ) ;
502
511
ret block_pp( fcx. ccx , an_alt. block ) ;
@@ -510,7 +519,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
510
519
intersect ( pp. postcondition , next. postcondition ) ;
511
520
ret pp;
512
521
}
513
- auto antec_pp = pp_clone ( expr_pp ( fcx. ccx , e ) ) ;
522
+ auto antec_pp = pp_clone ( expr_pp ( fcx. ccx , ex ) ) ;
514
523
auto e_pp = @rec ( precondition=empty_prestate ( num_local_vars) ,
515
524
postcondition=false_postcond ( num_local_vars) ) ;
516
525
auto g = bind combine_pp ( antec_pp, fcx, _, _) ;
0 commit comments