fix false positive where the fncall block could store invalid ptrs
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1066,7 +1066,7 @@ void Memory::mkNonlocalValAxioms(bool skip_consts) {
return;
for (unsigned i = 0, e = numNonlocals(); i != e; ++i) {
- if (always_noread(i))
+ if (always_noread(i, true))
continue;
Byte byte(*this, non_local_block_val[i].val.load(offset));

MODIFY
ir/state.cpp
ir/state.cpp
@@ -663,7 +663,7 @@ void State::addNoReturn(const expr &cond) {
return_undef_vars.insert(domain.undef_vars.begin(), domain.undef_vars.end());
if (cond.isTrue())
undef_vars.clear();
- addUB(!cond);
+ domain.path &= !cond;
}
expr State::FnCallInput::operator==(const FnCallInput &rhs) const {

ADD
tests/alive-tv/calls/ptr-store.srctgt.ll
+define void @src(ptr %0, i1 %1) {
+ %3 = alloca i64, align 8
+ store ptr null, ptr %0, align 8
+ call void @fn()
+ br i1 %1, label %4, label %5
+
+4:
+ ret void
+
+5:
+ store i64 0, ptr %3, align 8
+ ret void
+}
+
+define void @tgt(ptr %0, i1 %1) {
+ store ptr null, ptr %0, align 8
+ call void @fn()
+ ret void
+}
+
+declare void @fn()

fix false positive where the fncall block could store invalid ptrs