| 1345 | } |
| 1346 | |
| 1347 | void SMTEncoder::bytesToFixedBytesAssertions( |
| 1348 | smt::SymbolicArrayVariable& _symArray, |
| 1349 | Expression const& _fixedBytes |
| 1350 | ) |
| 1351 | { |
| 1352 | auto const& fixed = dynamic_cast<FixedBytesType const&>(*_fixedBytes.annotation().type); |
| 1353 | auto intType = TypeProvider::uint256(); |
| 1354 | std::string suffix = std::to_string(_fixedBytes.id()) + "_" + std::to_string(m_context.newUniqueId()); |
| 1355 | smt::SymbolicIntVariable k(intType, intType, "k_" + suffix, m_context); |
| 1356 | m_context.addAssertion(k.currentValue() == 0); |
| 1357 | size_t n = fixed.numBytes(); |
| 1358 | for (size_t i = 0; i < n; i++) |
| 1359 | { |
| 1360 | auto kPrev = k.currentValue(); |
| 1361 | m_context.addAssertion((smtutil::Expression::select(_symArray.elements(), i) * (u256(1) << ((n - i - 1) * 8))) + kPrev == k.increaseIndex()); |
| 1362 | } |
| 1363 | m_context.addAssertion(expr(_fixedBytes) == k.currentValue()); |
| 1364 | } |
| 1365 | |
| 1366 | void SMTEncoder::endVisit(Return const& _return) |
| 1367 | { |
nothing calls this directly
no test coverage detected