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

SMTChecker: Ignore model checking without callback

Browse Source
This commit is contained in:
Martin Blicha 2023-08-14 22:06:52 +02:00
parent b6326f4d4d
commit 1b68b5764d
2 changed files with 16 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
libsolidity/interface/CompilerStack.cpp
View File

@ -608,12 +608,21 @@ bool CompilerStack::analyze()
if (m_modelCheckerSettings.engine.any()) if (m_modelCheckerSettings.engine.any())
m_modelCheckerSettings.solvers = ModelChecker::checkRequestedSolvers(m_modelCheckerSettings.solvers, m_errorReporter); m_modelCheckerSettings.solvers = ModelChecker::checkRequestedSolvers(m_modelCheckerSettings.solvers, m_errorReporter);
ModelChecker modelChecker(m_errorReporter, *this, m_smtlib2Responses, m_modelCheckerSettings, m_readFile); if (m_modelCheckerSettings.engine.any() && !m_readFile)
modelChecker.checkRequestedSourcesAndContracts(allSources); m_errorReporter.warning(
for (Source const* source: m_sourceOrder) 7126_error,
if (source->ast) SourceLocation(),
modelChecker.analyze(*source->ast); "Model checker analysis requested but no callback for SMT queries was provided, ignoring!"
m_unhandledSMTLib2Queries += modelChecker.unhandledQueries(); );
else
{
ModelChecker modelChecker(m_errorReporter, *this, m_smtlib2Responses, m_modelCheckerSettings, m_readFile);
modelChecker.checkRequestedSourcesAndContracts(allSources);
for (Source const* source: m_sourceOrder)
if (source->ast)
modelChecker.analyze(*source->ast);
m_unhandledSMTLib2Queries += modelChecker.unhandledQueries();
}
} }
} }
catch (FatalError const&) catch (FatalError const&)

1
scripts/error_codes.py
View File

@ -207,6 +207,7 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False):
"2961", # SMTChecker, covered by CL tests "2961", # SMTChecker, covered by CL tests
"6240", # SMTChecker, covered by CL tests "6240", # SMTChecker, covered by CL tests
"9576", # SMTChecker, covered by CL tests "9576", # SMTChecker, covered by CL tests
"7126", # SMTChecker, analysis without callback (not sure how to cover this)
} }
assert len(test_ids & white_ids) == 0, "The sets are not supposed to intersect" assert len(test_ids & white_ids) == 0, "The sets are not supposed to intersect"
test_ids |= white_ids test_ids |= white_ids