diff --git a/ir/pointer.cpp b/ir/pointer.cpp index 69780d174..a7cd7fbd0 100644 --- a/ir/pointer.cpp +++ b/ir/pointer.cpp @@ -529,7 +529,7 @@ Pointer::isDereferenceable(const expr &bytes0, uint64_t align, DisjointExpr UB(expr(false)), is_aligned(expr(false)), all_ptrs; for (auto &[ptr_expr, domain] : DisjointExpr(p, 3)) { - Pointer ptr(m, ptr_expr); + auto [ptr, inboundsd] = Pointer(m, ptr_expr).toLogical(); auto [ub, aligned] = ::is_dereferenceable(ptr, bytes_off, bytes, align, iswrite, ignore_accessability); @@ -537,8 +537,8 @@ Pointer::isDereferenceable(const expr &bytes0, uint64_t align, if (!ub.isFalse() && !aligned.isFalse() && !ptr.blockSize().isZero()) all_ptrs.add(std::move(ptr).release(), domain); - UB.add(std::move(ub), domain); - is_aligned.add(std::move(aligned), domain); + UB.add(ub && inboundsd, domain); + is_aligned.add(std::move(aligned), std::move(domain)); } AndExpr exprs; @@ -833,8 +833,10 @@ Pointer::mkIf(const expr &cond, const Pointer &then, const Pointer &els) { } ostream& operator<<(ostream &os, const Pointer &p) { + auto logical = p.isLogical(); + if (p.isNull().isTrue()) - return os << "null"; + return os << (logical.isFalse() ? "0x0" : "null"); #define P(field, fn) \ if (field.isConst()) \ @@ -842,7 +844,6 @@ ostream& operator<<(ostream &os, const Pointer &p) { else \ os << field - auto logical = p.isLogical(); os << (logical.isFalse() ? "phy-ptr(" : "pointer("); if (!logical.isFalse()) {