null block's alignment encoding was missing
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1472,7 +1472,7 @@ Memory::Memory(State &state) : state(&state), escaped_local_blks(*this) {
// Initialize a memory block for null pointer.
if (has_null_block)
- alloc(expr::mkUInt(0, bits_size_t), 1, GLOBAL, false, false, 0);
+ alloc(expr::mkUInt(0, bits_size_t), bits_byte / 8, GLOBAL, false, false, 0);
assert(bits_for_offset <= bits_size_t);
}
@@ -1855,8 +1855,8 @@ Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
}
} else {
state->addAxiom(p.blockSize() == size_zext);
- if (!has_null_block || bid != 0) {
state->addAxiom(p.isBlockAligned(align, true));
+ if (!has_null_block || bid != 0) {
state->addAxiom(p.getAllocType() == alloc_ty);
}

ADD
tests/alive-tv/memory/memset-align.srctgt.ll
+target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
+target triple = "x86_64-unknown-linux-gnu"
+
+declare void @llvm.memset.p0i8.i64(i8* nocapture writeonly, i8, i64, i1 immarg)
+
+define void @src(i8* %out) {
+entry:
+ call void @llvm.memset.p0i8.i64(i8* align 4 %out, i8 0, i64 0, i1 false)
+ ret void
+}
+
+; identity
+define void @tgt(i8* %out) {
+entry:
+ call void @llvm.memset.p0i8.i64(i8* align 4 %out, i8 0, i64 0, i1 false)
+ ret void
+}

null block's alignment encoding was missing (#549)