add Pointer::isNull()
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -244,7 +244,7 @@ expr Pointer::add_no_overflow(const expr &offset) const {
}
expr Pointer::operator==(const Pointer &rhs) const {
- return get_bid() == rhs.get_bid() && get_offset() == rhs.get_offset();
+ return p == rhs.p;
}
expr Pointer::operator!=(const Pointer &rhs) const {
@@ -341,8 +341,12 @@ Pointer Pointer::mkNullPointer(const Memory &m) {
return Pointer(m, 0, false);
}
+expr Pointer::isNull() const {
+ return *this == mkNullPointer(m);
+}
+
ostream& operator<<(ostream &os, const Pointer &p) {
- if ((p == Pointer::mkNullPointer(p.getMemory())).isTrue())
+ if (p.isNull().isTrue())
return os << "null";
os << "pointer(" << (p.is_local().simplify().isTrue() ? "local" : "non-local")
@@ -486,9 +490,7 @@ expr Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
void Memory::free(const expr &ptr) {
Pointer p(*this, ptr);
- auto isNullPointer = p == Pointer::mkNullPointer(*this);
-
- state->addUB(isNullPointer || (p.get_offset() == 0 &&
+ state->addUB(p.isNull() || (p.get_offset() == 0 &&
p.is_block_alive() &&
p.is_at_heap()));
blocks_liveness = blocks_liveness.store(p.get_bid(), false);

MODIFY
ir/memory.h
ir/memory.h
@@ -91,11 +91,8 @@ public:
const Memory& getMemory() const { return m; }
- // Makes a null pointer.
- // TODO: add a bool flag that says whether the twin memory model is used.
- // In the twin memory model, a null pointer is a physical pointer with
- // absolute address 0.
static Pointer mkNullPointer(const Memory &m);
+ smt::expr isNull() const;
friend std::ostream& operator<<(std::ostream &os, const Pointer &p);
};

add Pointer::isNull()