| 2345 | } |
| 2346 | |
| 2347 | void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector<smtutil::Expression> const& _callArgs) |
| 2348 | { |
| 2349 | auto const& funParams = _function.parameters(); |
| 2350 | solAssert(funParams.size() == _callArgs.size(), ""); |
| 2351 | for (unsigned i = 0; i < funParams.size(); ++i) |
| 2352 | if (createVariable(*funParams[i])) |
| 2353 | { |
| 2354 | m_context.addAssertion(_callArgs[i] == m_context.newValue(*funParams[i])); |
| 2355 | if (funParams[i]->annotation().type->category() == Type::Category::Mapping) |
| 2356 | m_arrayAssignmentHappened = true; |
| 2357 | } |
| 2358 | |
| 2359 | std::vector<VariableDeclaration const*> localVars; |
| 2360 | if (auto const* fun = dynamic_cast<FunctionDefinition const*>(&_function)) |
| 2361 | localVars = localVariablesIncludingModifiers(*fun, m_currentContract); |
| 2362 | else |
| 2363 | localVars = _function.localVariables(); |
| 2364 | for (auto const& variable: localVars) |
| 2365 | if (createVariable(*variable)) |
| 2366 | { |
| 2367 | m_context.newValue(*variable); |
| 2368 | m_context.setZeroValue(*variable); |
| 2369 | } |
| 2370 | |
| 2371 | if (_function.returnParameterList()) |
| 2372 | for (auto const& retParam: _function.returnParameters()) |
| 2373 | if (createVariable(*retParam)) |
| 2374 | { |
| 2375 | m_context.newValue(*retParam); |
| 2376 | m_context.setZeroValue(*retParam); |
| 2377 | } |
| 2378 | } |
| 2379 | |
| 2380 | void SMTEncoder::createStateVariables(ContractDefinition const& _contract) |
| 2381 | { |
nothing calls this directly
no test coverage detected