fix memset to make poison ptrs always UB
This is necessary as addresses must be sufficiently aligned, hence not poison
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -3208,8 +3208,9 @@ StateValue Memset::toSMT(State &s) const {
} else {
auto &sv_ptr = s[*ptr];
auto &sv_ptr2 = s[*ptr];
- s.addUB((vbytes != 0).implies(
- sv_ptr.non_poison && (sv_ptr.value == sv_ptr2.value)));
+ // can't be poison even if bytes=0 as address must be aligned regardless
+ s.addUB(sv_ptr.non_poison);
+ s.addUB((vbytes != 0).implies(sv_ptr.value == sv_ptr2.value));
vptr = sv_ptr.value;
}
check_can_store(s, vptr);

fix memset to make poison ptrs always UB
This is necessary as addresses must be sufficiently aligned, hence not poison