@@ -284,14 +284,21 @@ class FatPointer extends TFatPointer {
284284predicate srcSinkLengthMap (
285285 FatPointer start , FatPointer end , int srcOffset , int sinkOffset , int length
286286) {
287- srcOffset = start .getOffset ( ) and
288- sinkOffset = end .getOffset ( ) and
289- (
290- /* Base case: The object is allocated and a fat pointer created. */
291- length = start .getLength ( )
292- or
293- /* Recursive case: A fat pointer is derived from a fat pointer. */
294- srcSinkLengthMap ( _, start , _, srcOffset , length )
287+ exists ( TrackArray:: PathNode src , TrackArray:: PathNode sink |
288+ TrackArray:: flowPath ( src , sink ) and
289+ /* Reiterate the data flow configuration here. */
290+ src .getNode ( ) = start .getNode ( ) and
291+ sink .getNode ( ) .asExpr ( ) = end .getBasePointer ( )
292+ |
293+ srcOffset = start .getOffset ( ) and
294+ sinkOffset = end .getOffset ( ) and
295+ (
296+ /* Base case: The object is allocated and a fat pointer created. */
297+ length = start .getLength ( )
298+ or
299+ /* Recursive case: A fat pointer is derived from a fat pointer. */
300+ srcSinkLengthMap ( _, start , _, srcOffset , length )
301+ )
295302 )
296303}
297304
@@ -318,10 +325,6 @@ where
318325 not isExcluded ( sink .getNode ( ) .asExpr ( ) ,
319326 Memory1Package:: pointerArithmeticFormsAnInvalidPointerQuery ( ) ) and
320327 exists ( FatPointer start , FatPointer end , int srcOffset , int sinkOffset , int length |
321- TrackArray:: flowPath ( src , sink ) and
322- /* Reiterate the data flow configuration here. */
323- src .getNode ( ) = start .getNode ( ) and
324- sink .getNode ( ) .asExpr ( ) = end .getBasePointer ( ) and
325328 srcSinkLengthMap ( start , end , srcOffset , sinkOffset , length ) and
326329 (
327330 srcOffset + sinkOffset < 0 or // Underflow detection
0 commit comments