@@ -148,13 +148,9 @@ private module SizeBarrier {
148
148
// We know:
149
149
// 1. result <= value + delta (by `bounded`)
150
150
// 2. value < right + k + 1 (by `operandGuardChecks`).
151
- // Condition 2 implies: value <= right + k, so if we know
152
- // that `state >= k + delta` then we have:
151
+ // Note that condition 2 implies: value <= right + k. So we have:
153
152
// result <= value + delta (by 1.)
154
153
// <= right + k + delta (by 2.)
155
- // <= right + state (by the assumption).
156
- // Callers of `getABarrierInstruction0` should ensure that `state >= k + delta`
157
- // is satisfied.
158
154
operandGuardChecks ( pragma [ only_bind_into ] ( g ) , pragma [ only_bind_into ] ( left ) , right ,
159
155
pragma [ only_bind_into ] ( k + 1 ) , pragma [ only_bind_into ] ( edge ) ) and
160
156
bounded ( result , value .getAnInstruction ( ) , delta ) and
@@ -171,9 +167,9 @@ private module SizeBarrier {
171
167
pragma [ inline_late]
172
168
Instruction getABarrierInstruction ( int state ) {
173
169
exists ( int delta , int k |
174
- // See the implementation comments in `getABarrierInstruction0` for why
175
- // this conjunct is necessary.
176
170
state >= k + delta and
171
+ // result <= "size of allocation" + delta + k
172
+ // <= "size of allocation" + state
177
173
result = getABarrierInstruction0 ( delta , k )
178
174
)
179
175
}
@@ -199,9 +195,10 @@ private module SizeBarrier {
199
195
ValidForStateFlow:: flow ( source , result ) and
200
196
hasSize ( _, source , state ) and
201
197
ValidForStateConfig:: isSink ( result , delta , k ) and
202
- // See the implementation comments in `getABarrierInstruction0` for why
203
- // this conjunct is necessary.
204
198
state >= k + delta
199
+ // so now we have:
200
+ // result <= "size of allocation" + delta + k
201
+ // <= "size of allocation" + state
205
202
)
206
203
}
207
204
}
0 commit comments