Method mkInput

ir/memory.cpp:1729–1754

}

expr Memory::mkInput(const char *name, const ParamAttrs &attrs0) {
  unsigned max_bid = has_null_block + num_globals_src + next_ptr_input++;
  assert(max_bid < num_nonlocals_src);

  // FIXME: doesn't consider physical ptrs
  // consider how to do POR?

  auto attrs = attrs0;
  attrs.set(ParamAttrs::IsArg);
  Pointer p(*this, name, attrs);
  auto bid = p.getShortBid();

  state->addAxiom(bid.ule(max_bid));
  state->addAxiom(!Pointer(*this, max_bid, false).isStackAllocated(false));

  AliasSet alias(*this);
  alias.setMayAliasUpTo(false, max_bid);

  for (auto [byval_bid, is_const] : byval_blks) {
    state->addAxiom(bid != byval_bid);
    alias.setNoAlias(false, byval_bid);
  }
  ptr_alias.emplace(p.getBid(), std::move(alias));

  return std::move(p).release();
}

pair<expr, expr> Memory::mkUndefInput(const ParamAttrs &attrs0) {
  unsigned bits = bits_for_offset + bits_for_bid - Pointer::hasLocalBit();