cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

SMTCheckerTests: Use SMT callback

Browse Source
This commit is contained in:
Martin Blicha 2023-08-09 11:08:30 +02:00
parent 1d60559551
commit 58d0579ba6
2 changed files with 11 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
test/libsolidity/SMTCheckerTest.cpp
View File

@ -133,6 +133,11 @@ void SMTCheckerTest::setupCompiler()
compiler().setModelCheckerSettings(m_modelCheckerSettings);
}
std::unique_ptr<CompilerStack> SMTCheckerTest::createStack() const
{
return std::make_unique<CompilerStack>(m_smtCommand.solver());
}
void SMTCheckerTest::filterObtainedErrors()
{
SyntaxTest::filterObtainedErrors();

6
test/libsolidity/SMTCheckerTest.h
View File

@ -23,6 +23,7 @@
#include <libsmtutil/SolverInterface.h>
#include <libsolidity/formal/ModelChecker.h>
#include <libsolidity/interface/SMTSolverCommand.h>
#include <string>
@ -39,6 +40,9 @@ public:
SMTCheckerTest(std::string const& _filename);
void setupCompiler() override;
std::unique_ptr<CompilerStack> createStack() const override;
void filterObtainedErrors() override;
void printUpdatedExpectations(std::ostream& _stream, std::string const& _linePrefix) const override;
@ -65,6 +69,8 @@ protected:
bool m_ignoreCex = false;
std::vector<SyntaxTestError> m_unfilteredErrorList;
mutable SMTSolverCommand m_smtCommand;
};
}