SymbolicAddressMap { public boolean isSubset(SymbolicAddressMap other) { if(other.isTop()) return true; else if(this.isTop()) return false; else if(other == null) return false; for(Location l : this.mapP.keySet()) { BoundedSet<SymbolicAddress> thisEntry = mapP.get(l); BoundedSet<SymbolicAddress> otherEntry = other.mapP.get(l); if(otherEntry == null) return false; if(! thisEntry.isSubset(otherEntry)) return false; } for(String l : this.mapA.keySet()) { BoundedSet<SymbolicAddress> thisEntry = mapP.get(l); BoundedSet<SymbolicAddress> otherEntry = other.mapP.get(l); if(otherEntry == null) return false; if(! thisEntry.isSubset(otherEntry)) return false; } return true; } 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 testIsSubset() { SymbolicAddressMap m1 = map1(); SymbolicAddressMap m2 = map2(); SymbolicAddressMap top = SymbolicAddressMap.top(); assert(! m1.isSubset(m2)); assert(! m2.isSubset(m1)); assert(m1.isSubset(map1())); assert(m2.isSubset(map2())); assert(m1.isSubset(top)); assert(m2.isSubset(top)); assert(! top.isSubset(m1)); assert(! top.isSubset(m2)); SymbolicAddressMap m12 = m1.clone(); m12.join(m2); SymbolicAddressMap m21 = m2.clone(); m21.join(m1); assert(m12.equals(m21)); assert(m1.isSubset(m12)); assert(m1.isSubset(m12)); assert(m2.isSubset(m21)); assert(m2.isSubset(m21)); }