@@ -123,7 +123,12 @@ abstract class MemoryLocation extends TMemoryLocation {
123
123
124
124
abstract predicate isMayAccess ( ) ;
125
125
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 ( ) }
127
132
128
133
/**
129
134
* Holds if the location cannot be overwritten except by definition of a `MemoryLocation` for
@@ -177,7 +182,7 @@ abstract class AllocationMemoryLocation extends MemoryLocation {
177
182
178
183
final override Location getLocation ( ) { result = var .getLocation ( ) }
179
184
180
- final override Allocation getAllocation ( ) { result = var }
185
+ final override Allocation getAnAllocation ( ) { result = var }
181
186
182
187
final override predicate isMayAccess ( ) { isMayAccess = true }
183
188
@@ -453,15 +458,15 @@ private Overlap getExtentOverlap(MemoryLocation def, MemoryLocation use) {
453
458
result instanceof MustExactlyOverlap
454
459
or
455
460
not use instanceof EntireAllocationMemoryLocation and
456
- if def .getAllocation ( ) = use .getAllocation ( )
461
+ if def .getAnAllocation ( ) = use .getAnAllocation ( )
457
462
then
458
463
// EntireAllocationMemoryLocation totally overlaps any location within
459
464
// the same allocation.
460
465
result instanceof MustTotallyOverlap
461
466
else (
462
467
// There is no overlap with a location that's known to belong to a
463
468
// different allocation, but all other locations may partially overlap.
464
- not exists ( use .getAllocation ( ) ) and
469
+ not exists ( use .getAnAllocation ( ) ) and
465
470
result instanceof MayPartiallyOverlap
466
471
)
467
472
)
@@ -541,15 +546,15 @@ private predicate isCoveredOffset(Allocation var, int offsetRank, VariableMemory
541
546
exists ( int startRank , int endRank , VirtualVariable vvar |
542
547
vml .getStartBitOffset ( ) = rank [ startRank ] ( IntValue offset_ | isRelevantOffset ( vvar , offset_ ) ) and
543
548
vml .getEndBitOffset ( ) = rank [ endRank ] ( IntValue offset_ | isRelevantOffset ( vvar , offset_ ) ) and
544
- var = vml .getAllocation ( ) and
549
+ var = vml .getAnAllocation ( ) and
545
550
vvar = vml .getVirtualVariable ( ) and
546
551
isRelatableMemoryLocation ( vml ) and
547
552
offsetRank in [ startRank .. endRank ]
548
553
)
549
554
}
550
555
551
556
private predicate hasUnknownOffset ( Allocation var , VariableMemoryLocation vml ) {
552
- vml .getAllocation ( ) = var and
557
+ vml .getAnAllocation ( ) = var and
553
558
(
554
559
vml .getStartBitOffset ( ) = Ints:: unknown ( ) or
555
560
vml .getEndBitOffset ( ) = Ints:: unknown ( )
@@ -564,9 +569,9 @@ private predicate overlappingIRVariableMemoryLocations(
564
569
isCoveredOffset ( var , offsetRank , use )
565
570
)
566
571
or
567
- hasUnknownOffset ( use .getAllocation ( ) , def )
572
+ hasUnknownOffset ( use .getAnAllocation ( ) , def )
568
573
or
569
- hasUnknownOffset ( def .getAllocation ( ) , use )
574
+ hasUnknownOffset ( def .getAnAllocation ( ) , use )
570
575
}
571
576
572
577
private Overlap getVariableMemoryLocationOverlap (
0 commit comments