| 946 | } |
| 947 | |
| 948 | pair<Pointer, expr> Pointer::findLogicalLocalPointer(const expr &addr) const { |
| 949 | DisjointExpr<Pointer> ret(mkNullPointer(m)); |
| 950 | |
| 951 | for (unsigned i = 0, e = m.numLocals(); i != e; ++i) { |
| 952 | // address not observed; can't alias with that |
| 953 | if (!m.observed_addrs.mayAlias(true, i)) |
| 954 | continue; |
| 955 | |
| 956 | Pointer p(m, i, true); |
| 957 | expr blk_addr = p.getLogAddress(); |
| 958 | |
| 959 | ret.add(p + (addr - blk_addr), |
| 960 | addr.uge(blk_addr) && |
| 961 | addr.ult((p + p.blockSize()).getLogAddress())); |
| 962 | } |
| 963 | return { *std::move(ret)(), ret.domain() }; |
| 964 | } |
| 965 | |
| 966 | pair<Pointer, expr> Pointer::toLogicalLocal() const { |
| 967 | if (isLogical().isTrue()) |