print a null pointer as 'null' in counterexamples
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -331,12 +331,15 @@ expr Pointer::is_readonly() const {
return m.blocks_readonly.load(get_bid());
}
-Pointer Pointer::mkNullPointer(Memory &m) {
+Pointer Pointer::mkNullPointer(const Memory &m) {
// A null pointer points to block 0.
return Pointer(m, 0, false);
}
ostream& operator<<(ostream &os, const Pointer &p) {
+ if ((p == Pointer::mkNullPointer(p.getMemory())).isTrue())
+ return os << "null";
+
os << "pointer(" << (p.is_local().simplify().isTrue() ? "local" : "non-local")
<< ", block_id=";
p.get_bid().simplify().printUnsigned(os);

MODIFY
ir/memory.h
ir/memory.h
@@ -87,7 +87,7 @@ public:
// 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(Memory &m);
+ static Pointer mkNullPointer(const Memory &m);
friend std::ostream& operator<<(std::ostream &os, const Pointer &p);
};

print a null pointer as 'null' in counterexamples