fix last bit of false prencondition when using -disable-poison-input
in programs without mem accesses and input ptrs
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1052,7 +1052,8 @@ void Memory::mkNonlocalValAxioms(bool skip_consts) {
= expr::mkFreshVar("#off", expr::mkUInt(0, Pointer::bitsShortOffset()));
// Users may request the initial memory to be non-poisonous
- if (config::disable_poison_input && state->isSource()) {
+ if (config::disable_poison_input && state->isSource() &&
+ (does_int_mem_access || does_ptr_mem_access)) {
for (auto &block : non_local_block_val) {
if (isInitialMemBlock(block.val))
state->addAxiom(

ADD
tests/alive-tv/memory/non-poison-mem.srctgt.ll
+; TEST-ARGS: -disable-poison-input
+
+define void @src(ptr %p) {
+ ret void
+}
+
+define void @tgt(ptr %p) {
+ ret void
+}

fix last bit of #831: false prencondition when using -disable-poison-input
in programs without mem accesses and input ptrs