SymbolicAddressMap { public SymbolicAddressMap cloneInvoke(int framePtr) { if(this.isTop()) return this; SymbolicAddressMap copy = new SymbolicAddressMap(this.bsFactory); for(Entry<Location, BoundedSet<SymbolicAddress>> entry : mapP.entrySet()) { Location loc = entry.getKey(); if(loc.isHeapLoc()) { copy.put(loc, entry.getValue()); } else if(loc.stackLoc >= framePtr) { copy.putStack(loc.stackLoc - framePtr, entry.getValue()); } } return copy; } SymbolicAddressMap(BoundedSetFactory<SymbolicAddress> bsFactory); private  SymbolicAddressMap(BoundedSetFactory<SymbolicAddress> bsFactory,
							   HashMap<Location,BoundedSet<SymbolicAddress>> initP,
							   HashMap<String,BoundedSet<SymbolicAddress>> initA); boolean isTop(); static SymbolicAddressMap top(); @Override int hashCode(); @Override boolean equals(Object obj); boolean isSubset(SymbolicAddressMap other); SymbolicAddressMap cloneFilterStack(int bound); SymbolicAddressMap cloneInvoke(int framePtr); void addStackUpto(SymbolicAddressMap in, int bound); void join(SymbolicAddressMap b); void joinReturned(SymbolicAddressMap returned, int framePtr); void copyStack(SymbolicAddressMap in, int dst, int src); BoundedSet<SymbolicAddress> getStack(int index); void putStack(int index, BoundedSet<SymbolicAddress> bs); BoundedSet<SymbolicAddress> getHeap(String staticfield); void putHeap(String staticfield, BoundedSet<SymbolicAddress> pointers); void put(Location l, BoundedSet<SymbolicAddress> bs); void addAlias(String ty, BoundedSet<SymbolicAddress> newAliases); BoundedSet<SymbolicAddress> getAliases(String fieldType); void print(PrintStream out, int indent); @Override String toString();  }
@Test public void testCloneInvoke() { SymbolicAddressMap m1 = map1(); SymbolicAddressMap m2 = map2(); SymbolicAddressMap top = SymbolicAddressMap.top(); assertEquals(m1, m1.cloneInvoke(0)); int framePtr = 2; SymbolicAddressMap m1i = m1.cloneInvoke(framePtr); SymbolicAddressMap m1a = new SymbolicAddressMap(bsf2); m1a.addStackUpto(m1, framePtr); m1a.joinReturned(m1i, framePtr); assertEquals(m1,m1a); framePtr = 1; SymbolicAddressMap m2i = m2.cloneInvoke(framePtr); SymbolicAddressMap m2a = new SymbolicAddressMap(bsf2); m2a.addStackUpto(m2, framePtr); m2a.joinReturned(m2i, framePtr); assertEquals(m2,m2a); try { m1a.joinReturned(null, 0); fail("joinReturned(null) should throw AssertionError"); } catch (AssertionError _) {} assertEquals(m1,m1a); m1a.joinReturned(SymbolicAddressMap.top(), 1); assertEquals(m1a,top); top.joinReturned(m1i, 1); assertEquals(SymbolicAddressMap.top(),top); }