fix alignment check when bytes is 0
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -143,7 +143,7 @@ void Pointer::is_dereferenceable(const expr &bytes0, unsigned align) {
cond &= offset.add_no_uoverflow(bytes);
// 2) check block's address is aligned
- cond &= is_aligned(align);
+ m.state->addUB(is_aligned(align));
// 3) check block is alive
cond &= is_block_alive();

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -201,7 +201,7 @@ public:
return error(i);
RETURN_IDENTIFIER(make_unique<Memset>(*ptr, *val, *bytes,
- i.getDestAlignment()));
+ min(1, i.getDestAlignment())));
}
RetTy visitMemTransferInst(llvm::MemTransferInst &i) {
@@ -213,8 +213,8 @@ public:
return error(i);
RETURN_IDENTIFIER(make_unique<Memcpy>(*dst, *src, *bytes,
- i.getDestAlignment(),
- i.getSourceAlignment(),
+ min(1, i.getDestAlignment()),
+ min(1, i.getSourceAlignment()),
isa<llvm::MemMoveInst>(&i)));
}

fix alignment check when bytes is 0 (#115)