@@ -172,7 +172,7 @@ private module Config implements ProductFlow::StateConfigSig {
172
172
class FlowState2 = int ;
173
173
174
174
predicate isSourcePair (
175
- DataFlow:: Node allocSource , FlowState1 unit , DataFlow:: Node sizeSource , FlowState2 extra
175
+ DataFlow:: Node allocSource , FlowState1 unit , DataFlow:: Node sizeSource , FlowState2 sizeAddend
176
176
) {
177
177
// In the case of an allocation like
178
178
// ```cpp
@@ -181,16 +181,16 @@ private module Config implements ProductFlow::StateConfigSig {
181
181
// we use `state2` to remember that there was an offset (in this case an offset of `1`) added
182
182
// to the size of the allocation. This state is then checked in `isSinkPair`.
183
183
exists ( unit ) and
184
- hasSize ( allocSource .asConvertedExpr ( ) , sizeSource , extra )
184
+ hasSize ( allocSource .asConvertedExpr ( ) , sizeSource , sizeAddend )
185
185
}
186
186
187
187
predicate isSinkPair (
188
- DataFlow:: Node allocSink , FlowState1 unit , DataFlow:: Node sizeSink , FlowState2 extra
188
+ DataFlow:: Node allocSink , FlowState1 unit , DataFlow:: Node sizeSink , FlowState2 sizeAddend
189
189
) {
190
190
exists ( unit ) and
191
191
// We check that the delta computed by the range analysis matches the
192
192
// state value that we set in `isSourcePair`.
193
- pointerAddInstructionHasBounds0 ( _, allocSink , sizeSink , extra )
193
+ pointerAddInstructionHasBounds0 ( _, allocSink , sizeSink , sizeAddend )
194
194
}
195
195
196
196
predicate isBarrier2 ( DataFlow:: Node node , FlowState2 state ) {
0 commit comments