Skip to content

Commit 394b7ad

Browse files
committed
Add an accumulating logic
1 parent 08c151b commit 394b7ad

1 file changed

Lines changed: 9 additions & 6 deletions

File tree

cpp/misra/src/rules/RULE-8-7-1/PointerArithmeticFormsAnInvalidPointer.ql

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -260,7 +260,7 @@ class PointerFormation extends TPointerFormation {
260260
result = this.asPointerArithmetic()
261261
}
262262

263-
private PointerAddInstruction getInstruction() { result.getAst() = this.asExpr() }
263+
private PointerArithmeticInstruction getInstruction() { result.getAst() = this.asExpr() }
264264

265265
/**
266266
* Gets the data-flow node associated with this pointer formation.
@@ -356,7 +356,7 @@ class FatPointer extends TFatPointer {
356356
* NOTE: Consult the configuration `TrackArrayConfig` for the actual definition of `src` and `sink`.
357357
*/
358358
predicate srcSinkLengthMap(
359-
FatPointer start, FatPointer end, int srcOffset, int sinkOffset, int length
359+
FatPointer start, FatPointer end, int srcOffset, int sinkOffset, int currentOffset, int length
360360
) {
361361
exists(TrackArray::PathNode src, TrackArray::PathNode sink |
362362
TrackArray::flowPath(src, sink) and
@@ -368,10 +368,14 @@ predicate srcSinkLengthMap(
368368
sinkOffset = end.getOffset() and
369369
(
370370
/* Base case: The object is allocated and a fat pointer created. */
371-
length = start.asAllocated().getLength(src.getNode())
371+
length = start.asAllocated().getLength(src.getNode()) and
372+
currentOffset = srcOffset + sinkOffset
372373
or
373374
/* Recursive case: A fat pointer is derived from a fat pointer. */
374-
srcSinkLengthMap(_, start, _, srcOffset, length)
375+
exists(int previousOffset |
376+
srcSinkLengthMap(_, start, _, srcOffset, previousOffset, length) and
377+
currentOffset = previousOffset + sinkOffset
378+
)
375379
)
376380
)
377381
}
@@ -403,8 +407,7 @@ where
403407
src.getNode() = start.getNode() and
404408
sink.getNode() = end.getBasePointerNode()
405409
|
406-
srcSinkLengthMap(start, end, srcOffset, sinkOffset, length) and
407-
totalOffset = srcOffset + sinkOffset and
410+
srcSinkLengthMap(start, end, srcOffset, sinkOffset, totalOffset, length) and
408411
(
409412
totalOffset < 0 or // Underflow detection
410413
totalOffset > length // Overflow detection

0 commit comments

Comments
 (0)