C++: 'sizeAddend' instead of 'extra'.

This commit is contained in:
Mathias Vorreiter Pedersen
2023-07-24 10:57:25 +02:00
parent 83aef6fc16
commit c44507cc42

View File

@@ -172,7 +172,7 @@ private module Config implements ProductFlow::StateConfigSig {
class FlowState2 = int; class FlowState2 = int;
predicate isSourcePair( predicate isSourcePair(
DataFlow::Node allocSource, FlowState1 unit, DataFlow::Node sizeSource, FlowState2 extra DataFlow::Node allocSource, FlowState1 unit, DataFlow::Node sizeSource, FlowState2 sizeAddend
) { ) {
// In the case of an allocation like // In the case of an allocation like
// ```cpp // ```cpp
@@ -181,16 +181,16 @@ private module Config implements ProductFlow::StateConfigSig {
// we use `state2` to remember that there was an offset (in this case an offset of `1`) added // we use `state2` to remember that there was an offset (in this case an offset of `1`) added
// to the size of the allocation. This state is then checked in `isSinkPair`. // to the size of the allocation. This state is then checked in `isSinkPair`.
exists(unit) and exists(unit) and
hasSize(allocSource.asConvertedExpr(), sizeSource, extra) hasSize(allocSource.asConvertedExpr(), sizeSource, sizeAddend)
} }
predicate isSinkPair( predicate isSinkPair(
DataFlow::Node allocSink, FlowState1 unit, DataFlow::Node sizeSink, FlowState2 extra DataFlow::Node allocSink, FlowState1 unit, DataFlow::Node sizeSink, FlowState2 sizeAddend
) { ) {
exists(unit) and exists(unit) and
// We check that the delta computed by the range analysis matches the // We check that the delta computed by the range analysis matches the
// state value that we set in `isSourcePair`. // state value that we set in `isSourcePair`.
pointerAddInstructionHasBounds0(_, allocSink, sizeSink, extra) pointerAddInstructionHasBounds0(_, allocSink, sizeSink, sizeAddend)
} }
predicate isBarrier2(DataFlow::Node node, FlowState2 state) { predicate isBarrier2(DataFlow::Node node, FlowState2 state) {