| 760 | } |
| 761 | |
| 762 | void SMTEncoder::initFunction(FunctionDefinition const& _function) |
| 763 | { |
| 764 | solAssert(m_callStack.empty(), ""); |
| 765 | solAssert(m_currentContract, ""); |
| 766 | m_context.pushSolver(); |
| 767 | m_pathConditions.clear(); |
| 768 | pushCallStack({&_function, nullptr}); |
| 769 | m_uninterpretedTerms.clear(); |
| 770 | createStateVariables(*m_currentContract); |
| 771 | createLocalVariables(_function); |
| 772 | m_arrayAssignmentHappened = false; |
| 773 | clearIndices(m_currentContract, &_function); |
| 774 | m_checked = true; |
| 775 | } |
| 776 | |
| 777 | void SMTEncoder::visitAssert(FunctionCall const& _funCall) |
| 778 | { |
nothing calls this directly
no test coverage detected