@@ -123,7 +123,12 @@ abstract class MemoryLocation extends TMemoryLocation {
123123
124124 abstract predicate isMayAccess ( ) ;
125125
126- Allocation getAllocation ( ) { none ( ) }
126+ /**
127+ * Gets an allocation associated with this `MemoryLocation`.
128+ *
129+ * This always returns zero or one result.
130+ */
131+ Allocation getAnAllocation ( ) { none ( ) }
127132
128133 /**
129134 * Holds if the location cannot be overwritten except by definition of a `MemoryLocation` for
@@ -177,7 +182,7 @@ abstract class AllocationMemoryLocation extends MemoryLocation {
177182
178183 final override Location getLocation ( ) { result = var .getLocation ( ) }
179184
180- final override Allocation getAllocation ( ) { result = var }
185+ final override Allocation getAnAllocation ( ) { result = var }
181186
182187 final override predicate isMayAccess ( ) { isMayAccess = true }
183188
@@ -453,15 +458,15 @@ private Overlap getExtentOverlap(MemoryLocation def, MemoryLocation use) {
453458 result instanceof MustExactlyOverlap
454459 or
455460 not use instanceof EntireAllocationMemoryLocation and
456- if def .getAllocation ( ) = use .getAllocation ( )
461+ if def .getAnAllocation ( ) = use .getAnAllocation ( )
457462 then
458463 // EntireAllocationMemoryLocation totally overlaps any location within
459464 // the same allocation.
460465 result instanceof MustTotallyOverlap
461466 else (
462467 // There is no overlap with a location that's known to belong to a
463468 // different allocation, but all other locations may partially overlap.
464- not exists ( use .getAllocation ( ) ) and
469+ not exists ( use .getAnAllocation ( ) ) and
465470 result instanceof MayPartiallyOverlap
466471 )
467472 )
@@ -541,15 +546,15 @@ private predicate isCoveredOffset(Allocation var, int offsetRank, VariableMemory
541546 exists ( int startRank , int endRank , VirtualVariable vvar |
542547 vml .getStartBitOffset ( ) = rank [ startRank ] ( IntValue offset_ | isRelevantOffset ( vvar , offset_ ) ) and
543548 vml .getEndBitOffset ( ) = rank [ endRank ] ( IntValue offset_ | isRelevantOffset ( vvar , offset_ ) ) and
544- var = vml .getAllocation ( ) and
549+ var = vml .getAnAllocation ( ) and
545550 vvar = vml .getVirtualVariable ( ) and
546551 isRelatableMemoryLocation ( vml ) and
547552 offsetRank in [ startRank .. endRank ]
548553 )
549554}
550555
551556private predicate hasUnknownOffset ( Allocation var , VariableMemoryLocation vml ) {
552- vml .getAllocation ( ) = var and
557+ vml .getAnAllocation ( ) = var and
553558 (
554559 vml .getStartBitOffset ( ) = Ints:: unknown ( ) or
555560 vml .getEndBitOffset ( ) = Ints:: unknown ( )
@@ -564,9 +569,9 @@ private predicate overlappingIRVariableMemoryLocations(
564569 isCoveredOffset ( var , offsetRank , use )
565570 )
566571 or
567- hasUnknownOffset ( use .getAllocation ( ) , def )
572+ hasUnknownOffset ( use .getAnAllocation ( ) , def )
568573 or
569- hasUnknownOffset ( def .getAllocation ( ) , use )
574+ hasUnknownOffset ( def .getAnAllocation ( ) , use )
570575}
571576
572577private Overlap getVariableMemoryLocationOverlap (
0 commit comments