Method mkUndef

ir/pointer.cpp:137–168

}

expr Pointer::mkUndef(State &s) {
  auto &m = s.getMemory();
  bool force_local = false, force_nonlocal = false;
  if (hasLocalBit()) {
    force_nonlocal = m.numLocals() == 0;
    force_local    = !force_nonlocal && m.numNonlocals() == 0;
  }

  unsigned bits_phy = hasLogicalBit() * bits_ptr_address;
  unsigned bits_log
    = bits_for_bid + bits_for_offset - (force_local | force_nonlocal);
  unsigned var_bits = hasLogicalBit() + max(bits_log, bits_phy);

  expr var = expr::mkFreshVar("undef", expr::mkUInt(0, var_bits));

  expr ptr;
  if (bits_log >= bits_phy) {
    ptr = var.trunc(bits_log);
    if (force_local || force_nonlocal)
      ptr = mkLongBid(ptr, force_local);
    if (hasLogicalBit())
      ptr = var.sign().concat(ptr);
  } else {
    ptr = var;
  }

  ptr = ptr.concat_zeros(bits_for_ptrattrs);

  s.addUndefVar(std::move(var));
  assert(ptr.bits() == totalBits());
  return ptr;
}

unsigned Pointer::totalBits() {
  return max(total_bits_logical(), total_bits_physical());