Merge pull request #13751 from ethereum/smt_fix_natspec

Fix internal error in multiple wrong options for SMTChecker natspec
This commit is contained in:
Leo 2022-11-28 17:51:41 +01:00 committed by GitHub
commit 764569be16
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 16 additions and 1 deletions

View File

@ -24,6 +24,7 @@ Bugfixes:
* SMTChecker: Fix display error for negative integers that are one more than powers of two.
* SMTChecker: Improved readability for large integers that are powers of two or almost powers of two in error messages.
* SMTChecker: Fix internal error when a public library function is called internally.
* SMTChecker: Fix internal error on multiple wrong SMTChecker natspec entries.
### 0.8.17 (2022-09-08)

View File

@ -1102,14 +1102,18 @@ set<CHC::CHCNatspecOption> CHC::smtNatspecTags(FunctionDefinition const& _functi
{
set<CHC::CHCNatspecOption> options;
string smtStr = "custom:smtchecker";
bool errorSeen = false;
for (auto const& [tag, value]: _function.annotation().docTags)
if (tag == smtStr)
{
string const& content = value.content;
if (auto option = natspecOptionFromString(content))
options.insert(*option);
else
else if (!errorSeen)
{
errorSeen = true;
m_errorReporter.warning(3130_error, _function.location(), "Unknown option for \"" + smtStr + "\": \"" + content + "\"");
}
}
return options;
}

View File

@ -0,0 +1,10 @@
contract C {
/// @custom:smtchecker b
/// @custom:smtchecker
/// @custom:smtchecker a b c
function f() internal {}
}
contract D is C {}
// ----
// Warning 3130: (106-130): Unknown option for "custom:smtchecker": "b"