Skip to content

Commit

Permalink
allow memory blocks to be zero-sized
Browse files Browse the repository at this point in the history
  • Loading branch information
nunoplopes committed Sep 25, 2023
1 parent 8146409 commit dd3e2cf
Showing 1 changed file with 1 addition and 3 deletions.
4 changes: 1 addition & 3 deletions ir/memory.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1244,10 +1244,8 @@ void Memory::mkAxioms(const Memory &tgt) const {
auto sz = p1.blockSize().zextOrTrunc(bits_ptr_address);
auto align = p1.blockAlignment();

if (!has_null_block || bid != 0) {
if (!has_null_block || bid != 0)
state->addAxiom(addr != 0);
state->addAxiom(p1.blockSize() != 0);
}

// address must be properly aligned
state->addAxiom(
Expand Down

0 comments on commit dd3e2cf

Please sign in to comment.