aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal')
-rw-r--r--libsolidity/formal/SMTChecker.cpp36
1 files changed, 25 insertions, 11 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index c2f5c56d..12982204 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -262,14 +262,14 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
checkCondition(
value < minValue(intType),
_op.location(),
- "Underflow (resulting value less than " + intType.minValue().str() + ")",
+ "Underflow (resulting value less than " + formatNumber(intType.minValue()) + ")",
"value",
&value
);
checkCondition(
value > maxValue(intType),
_op.location(),
- "Overflow (resulting value larger than " + intType.maxValue().str() + ")",
+ "Overflow (resulting value larger than " + formatNumber(intType.maxValue()) + ")",
"value",
&value
);
@@ -341,16 +341,26 @@ void SMTChecker::checkCondition(
m_interface->addAssertion(_condition);
vector<smt::Expression> expressionsToEvaluate;
+ vector<string> expressionNames;
if (m_currentFunction)
{
if (_additionalValue)
+ {
expressionsToEvaluate.emplace_back(*_additionalValue);
+ expressionNames.push_back(_additionalValueName);
+ }
for (auto const& param: m_currentFunction->parameters())
if (knownVariable(*param))
+ {
expressionsToEvaluate.emplace_back(currentValue(*param));
+ expressionNames.push_back(param->name());
+ }
for (auto const& var: m_currentFunction->localVariables())
if (knownVariable(*var))
+ {
expressionsToEvaluate.emplace_back(currentValue(*var));
+ expressionNames.push_back(var->name());
+ }
}
smt::CheckResult result;
vector<string> values;
@@ -373,18 +383,22 @@ void SMTChecker::checkCondition(
{
std::ostringstream message;
message << _description << " happens here";
- size_t i = 0;
if (m_currentFunction)
{
message << " for:\n";
- if (_additionalValue)
- message << " " << _additionalValueName << " = " << values.at(i++) << "\n";
- for (auto const& param: m_currentFunction->parameters())
- if (knownVariable(*param))
- message << " " << param->name() << " = " << values.at(i++) << "\n";
- for (auto const& var: m_currentFunction->localVariables())
- if (knownVariable(*var))
- message << " " << var->name() << " = " << values.at(i++) << "\n";
+ solAssert(values.size() == expressionNames.size(), "");
+ for (size_t i = 0; i < values.size(); ++i)
+ {
+ string formattedValue = values.at(i);
+ try
+ {
+ // Parse and re-format nicely
+ formattedValue = formatNumber(bigint(formattedValue));
+ }
+ catch (...) { }
+
+ message << " " << expressionNames.at(i) << " = " << formattedValue << "\n";
+ }
}
else
message << ".";