@@ -80,12 +80,13 @@ fn seq_preconds(fcx: fn_ctxt, pps: [pre_and_post]) -> precond {
80
80
let sz: uint = vec:: len ( pps) ;
81
81
let num_vars: uint = num_constraints ( fcx. enclosing ) ;
82
82
83
- fn seq_preconds_go ( fcx : fn_ctxt , pps : [ pre_and_post ] , first : pre_and_post )
83
+ fn seq_preconds_go ( fcx : fn_ctxt , pps : [ pre_and_post ] ,
84
+ idx : uint , first : pre_and_post )
84
85
-> precond {
85
- let mut pps = pps ;
86
+ let mut idx = idx ;
86
87
let mut first = first;
87
88
loop {
88
- let sz: uint = vec:: len ( pps) ;
89
+ let sz: uint = vec:: len ( pps) - idx ;
89
90
if sz >= 1 u {
90
91
let second = pps[ 0 ] ;
91
92
assert ( pps_len ( second) == num_constraints ( fcx. enclosing ) ) ;
@@ -95,7 +96,7 @@ fn seq_preconds(fcx: fn_ctxt, pps: [pre_and_post]) -> precond {
95
96
union ( next_first, second_pre) ;
96
97
let next_first_post = clone ( first. postcondition ) ;
97
98
seq_tritv ( next_first_post, second. postcondition ) ;
98
- pps = vec :: slice ( pps , 1 u , sz ) ;
99
+ idx += 1 u ;
99
100
first = @{ precondition: next_first,
100
101
postcondition: next_first_post} ;
101
102
} else { ret first. precondition ; }
@@ -105,7 +106,7 @@ fn seq_preconds(fcx: fn_ctxt, pps: [pre_and_post]) -> precond {
105
106
if sz >= 1 u {
106
107
let first = pps[ 0 ] ;
107
108
assert ( pps_len ( first) == num_vars) ;
108
- ret seq_preconds_go ( fcx, vec :: slice ( pps, 1 u, sz ) , first) ;
109
+ ret seq_preconds_go ( fcx, pps, 1 u, first) ;
109
110
} else { ret true_precond ( num_vars) ; }
110
111
}
111
112
0 commit comments