Non local block's address cannot be zero if it is not null blk
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1309,11 +1309,11 @@ void Memory::mkAxioms(const Memory &other) const {
auto addr = p1.getAddress();
auto sz = p1.blockSize();
- expr disj = addr != 0;
+ state->addAxiom(addr != 0);
// Ensure block doesn't spill to local memory
auto bit = bits_size_t - 1;
- disj &= (addr + sz).extract(bit, bit) == 0;
+ expr disj = (addr + sz).extract(bit, bit) == 0;
// disjointness constraint
for (unsigned bid2 = bid + 1; bid2 < num_nonlocals; ++bid2) {

ADD
tests/alive-tv/attrs/nonnull-bugfix.srctgt.ll
+target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i8:64-f80:128-n8:16:32:64-S128"
+target triple = "x86_64-unknown-linux-gnu"
+
+; Function Attrs: nounwind uwtable
+define void @src(i8* %db, i8* %p) {
+entry:
+ %0 = ptrtoint i8* %p to i8
+ %1 = getelementptr i8, i8* %db, i32 0
+ %2 = load i8, i8* %1, align 8 ; It was loaded, so %db cannot be null
+ %call6 = call i8* @g(i8* %db)
+ ret void
+}
+
+define void @tgt(i8* %db, i8* %p) {
+entry:
+ %0 = ptrtoint i8* %p to i8
+ %1 = getelementptr i8, i8* %db, i32 0
+ %2 = load i8, i8* %1, align 8
+ %call6 = call i8* @g(i8* nonnull %db)
+ ret void
+}
+
+declare i8* @g(i8*)

Non local block's address cannot be zero if it is not null blk (#440)