| 2384 | } |
| 2385 | |
| 2386 | void SMTEncoder::initializeStateVariables(ContractDefinition const& _contract) |
| 2387 | { |
| 2388 | for (auto var: _contract.stateVariables()) |
| 2389 | { |
| 2390 | solAssert(m_context.knownVariable(*var), ""); |
| 2391 | m_context.setZeroValue(*var); |
| 2392 | } |
| 2393 | |
| 2394 | for (auto var: _contract.stateVariables()) |
| 2395 | if (var->value()) |
| 2396 | { |
| 2397 | var->value()->accept(*this); |
| 2398 | assignment(*var, *var->value()); |
| 2399 | } |
| 2400 | } |
| 2401 | |
| 2402 | void SMTEncoder::createLocalVariables(FunctionDefinition const& _function) |
| 2403 | { |
nothing calls this directly
no test coverage detected