cerc-io/solidity
10
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

Fix internal error when the abstract-nondet SMTChecker natspec annotation is used with a wrong option multiple times for the same function

Browse Source
This commit is contained in:
Leo Alt 2022-11-28 16:59:35 +01:00
parent 4baeddc62b
commit a5dab6181c
3 changed files with 16 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
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)

6
libsolidity/formal/CHC.cpp
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;
}

10
test/libsolidity/smtCheckerTests/natspec/natspec_smtchecker_multi_errors_1.sol Normal file
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"