@@ -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 */
358358predicate 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