| 2413 | } |
| 2414 | |
| 2415 | void SMTEncoder::initializeLocalVariables(FunctionDefinition const& _function) |
| 2416 | { |
| 2417 | for (auto const& variable: localVariablesIncludingModifiers(_function, m_currentContract)) |
| 2418 | { |
| 2419 | solAssert(m_context.knownVariable(*variable), ""); |
| 2420 | m_context.setZeroValue(*variable); |
| 2421 | } |
| 2422 | |
| 2423 | for (auto const& param: _function.parameters()) |
| 2424 | { |
| 2425 | solAssert(m_context.knownVariable(*param), ""); |
| 2426 | m_context.setUnknownValue(*param); |
| 2427 | } |
| 2428 | |
| 2429 | if (_function.returnParameterList()) |
| 2430 | for (auto const& retParam: _function.returnParameters()) |
| 2431 | { |
| 2432 | solAssert(m_context.knownVariable(*retParam), ""); |
| 2433 | m_context.setZeroValue(*retParam); |
| 2434 | } |
| 2435 | } |
| 2436 | |
| 2437 | void SMTEncoder::resetStateVariables() |
| 2438 | { |
nothing calls this directly
no test coverage detected