| 2792 | } |
| 2793 | |
| 2794 | expr Memory::checkInitializes() const { |
| 2795 | if (!has_initializes_attr) |
| 2796 | return true; |
| 2797 | |
| 2798 | expr ret = true; |
| 2799 | |
| 2800 | for (auto &input0 : state->getFn().getInputs()) { |
| 2801 | auto &input = static_cast<const Input&>(input0); |
| 2802 | auto &inits = input.getAttributes().initializes; |
| 2803 | if (inits.empty()) |
| 2804 | continue; |
| 2805 | |
| 2806 | Pointer arg(*this, (*state)[input].value); |
| 2807 | for (auto [l, h] : inits) { |
| 2808 | ret &= hasStored(arg + l, expr::mkUInt(h - l, bits_size_t)); |
| 2809 | } |
| 2810 | } |
| 2811 | return ret; |
| 2812 | } |
| 2813 | |
| 2814 | void Memory::record_stored_pointer(uint64_t bid, const expr &offset) { |
| 2815 | auto &set = stored_pointers[bid]; |