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

SMT model variables are sorted and printed as secondary source location

Browse Source
This commit is contained in:
Leonardo Alt 2018-08-01 23:27:46 +02:00
parent b6a2655513
commit 90f319615f
2 changed files with 12 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
libsolidity/formal/SMTChecker.cpp
View File

@ -601,15 +601,23 @@ void SMTChecker::checkCondition(
message << _description << " happens here"; message << _description << " happens here";
if (m_currentFunction) if (m_currentFunction)
{ {
message << " for:\n"; std::ostringstream modelMessage;
modelMessage << " for:\n";
solAssert(values.size() == expressionNames.size(), ""); solAssert(values.size() == expressionNames.size(), "");
map<string, string> sortedModel;
for (size_t i = 0; i < values.size(); ++i) for (size_t i = 0; i < values.size(); ++i)
if (expressionsToEvaluate.at(i).name != values.at(i)) if (expressionsToEvaluate.at(i).name != values.at(i))
message << " " << expressionNames.at(i) << " = " << values.at(i) << "\n"; sortedModel[expressionNames.at(i)] = values.at(i);
for (auto const& eval: sortedModel)
modelMessage << " " << eval.first << " = " << eval.second << "\n";
m_errorReporter.warning(_location, message.str() + loopComment, SecondarySourceLocation().append(modelMessage.str(), SourceLocation()));
} }
else else
{
message << "."; message << ".";
m_errorReporter.warning(_location, message.str() + loopComment); m_errorReporter.warning(_location, message.str() + loopComment);
}
break; break;
} }
case smt::CheckResult::UNSATISFIABLE: case smt::CheckResult::UNSATISFIABLE:

2
test/libsolidity/SMTChecker.cpp
View File

@ -110,7 +110,7 @@ BOOST_AUTO_TEST_CASE(simple_assert)
function f(uint a) public pure { assert(a == 2); } function f(uint a) public pure { assert(a == 2); }
} }
)"; )";
CHECK_WARNING(text, "Assertion violation happens here for"); CHECK_WARNING(text, "Assertion violation happens here");
} }
BOOST_AUTO_TEST_CASE(simple_assert_with_require) BOOST_AUTO_TEST_CASE(simple_assert_with_require)