Method hasStored

ir/memory.cpp:1351–1373

expr Memory::hasStored(const Pointer &p, const expr &bytes) const {
  assert(has_initializes_attr);

  unsigned bytes_per_byte = bits_byte / 8;
  expr bid = p.getShortBid();
  expr offset = p.getShortOffset();
  uint64_t bytes_i;
  if (bytes.isUInt(bytes_i) && (bytes_i / bytes_per_byte) <= 8) {
    expr ret = true;
    for (uint64_t off = 0; off < (bytes_i / bytes_per_byte); ++off) {
      expr off_expr = expr::mkUInt(off, offset);
      ret &= has_stored_arg.load(bid.concat(offset + off_expr));
    }
    return ret;
  } else {
    expr var = expr::mkFreshVar("#off", offset);
    state->addQuantVar(var);
    expr bytes_div = bytes.zextOrTrunc(offset.bits())
                          .udiv(expr::mkUInt(bytes_per_byte, bytes));
    return (var.uge(offset) && var.ult(offset + bytes_div))
             .implies(has_stored_arg.load(bid.concat(var)));
  }
}

void Memory::record_store(const Pointer &p, const smt::expr &bytes) {
  assert(has_initializes_attr);