fix semantics of a free that doesn't free
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2364,6 +2364,7 @@ StateValue FnCall::toSMT(State &s) const {
m.copy(ptr_old, Pointer(m, p_new));
+ if (!hasAttribute(FnAttrs::NoFree)) {
// 1) realloc(ptr, 0) always free the ptr.
// 2) If allocation failed, we should not free previous ptr, unless it's
// reallocf (always frees the pointer)
@@ -2372,6 +2373,7 @@ StateValue FnCall::toSMT(State &s) const {
: expr::mkIf(size == 0 || allocated, allocptr, nullp);
m.free(freeptr, false);
}
+ }
// FIXME: for a realloc that zeroes the new stuff
if (attrs.has(AllocKind::Zeroed))
@@ -2384,12 +2386,15 @@ StateValue FnCall::toSMT(State &s) const {
}
else if (attrs.has(AllocKind::Free)) {
auto &allocptr = s.getAndAddPoisonUB(get_alloc_ptr()).value;
+
+ if (!hasAttribute(FnAttrs::NoFree)) {
m.free(allocptr, false);
if (s.getFn().getFnAttrs().has(FnAttrs::NoFree)) {
Pointer ptr(m, allocptr);
s.addUB(ptr.isNull() || ptr.isLocal());
}
+ }
assert(isVoid());
return {};
}

ADD
tests/alive-tv/memory/free-nofree.srctgt.ll
+declare void @free(ptr) memory(none)
+
+define void @src(ptr %0) {
+ call void @free(ptr %0)
+ ret void
+}
+
+define void @tgt(ptr %0) {
+ ret void
+}

fix #871: semantics of a free that doesn't free