| 1754 | } |
| 1755 | |
| 1756 | pair<expr, expr> Memory::mkUndefInput(const ParamAttrs &attrs0) { |
| 1757 | unsigned bits = bits_for_offset + bits_for_bid - Pointer::hasLocalBit(); |
| 1758 | expr undef = expr::mkFreshVar("undef", expr::mkUInt(0, bits)); |
| 1759 | |
| 1760 | auto attrs = attrs0; |
| 1761 | attrs.set(ParamAttrs::IsArg); |
| 1762 | Pointer ptr(*this, |
| 1763 | Pointer::mkLongBid(undef.extract(bits-1, bits_for_offset), false), |
| 1764 | undef.extract(bits_for_offset-1, 0), attrs); |
| 1765 | |
| 1766 | if (attrs0.has(ParamAttrs::NonNull)) |
| 1767 | state->addPre(!ptr.isNull()); |
| 1768 | |
| 1769 | return { std::move(ptr).release(), std::move(undef) }; |
| 1770 | } |
| 1771 | |
| 1772 | Memory::FnRetData Memory::FnRetData::mkIf(const expr &cond, const FnRetData &a, |
| 1773 | const FnRetData &b) { |