mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Merge pull request #8902 from a3d4/partfix-5819-add-more-error-ids
Add error IDs to OverrideChecker, BMC and ContractLevelChecker
This commit is contained in:
commit
077cab0860
@ -112,7 +112,7 @@ void ContractLevelChecker::checkDuplicateFunctions(ContractDefinition const& _co
|
|||||||
functions[function->name()].push_back(function);
|
functions[function->name()].push_back(function);
|
||||||
}
|
}
|
||||||
|
|
||||||
findDuplicateDefinitions(functions, "Function with same name and arguments defined twice.");
|
findDuplicateDefinitions(functions);
|
||||||
}
|
}
|
||||||
|
|
||||||
void ContractLevelChecker::checkDuplicateEvents(ContractDefinition const& _contract)
|
void ContractLevelChecker::checkDuplicateEvents(ContractDefinition const& _contract)
|
||||||
@ -123,11 +123,11 @@ void ContractLevelChecker::checkDuplicateEvents(ContractDefinition const& _contr
|
|||||||
for (EventDefinition const* event: _contract.events())
|
for (EventDefinition const* event: _contract.events())
|
||||||
events[event->name()].push_back(event);
|
events[event->name()].push_back(event);
|
||||||
|
|
||||||
findDuplicateDefinitions(events, "Event with same name and arguments defined twice.");
|
findDuplicateDefinitions(events);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <class T>
|
template <class T>
|
||||||
void ContractLevelChecker::findDuplicateDefinitions(map<string, vector<T>> const& _definitions, string _message)
|
void ContractLevelChecker::findDuplicateDefinitions(map<string, vector<T>> const& _definitions)
|
||||||
{
|
{
|
||||||
for (auto const& it: _definitions)
|
for (auto const& it: _definitions)
|
||||||
{
|
{
|
||||||
@ -146,13 +146,27 @@ void ContractLevelChecker::findDuplicateDefinitions(map<string, vector<T>> const
|
|||||||
|
|
||||||
if (ssl.infos.size() > 0)
|
if (ssl.infos.size() > 0)
|
||||||
{
|
{
|
||||||
ssl.limitSize(_message);
|
ErrorId error;
|
||||||
|
string message;
|
||||||
|
if constexpr (is_same_v<T, FunctionDefinition const*>)
|
||||||
|
{
|
||||||
|
error = 1686_error;
|
||||||
|
message = "Function with same name and arguments defined twice.";
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
static_assert(is_same_v<T, EventDefinition const*>, "Expected \"FunctionDefinition const*\" or \"EventDefinition const*\"");
|
||||||
|
error = 5883_error;
|
||||||
|
message = "Event with same name and arguments defined twice.";
|
||||||
|
}
|
||||||
|
|
||||||
|
ssl.limitSize(message);
|
||||||
|
|
||||||
m_errorReporter.declarationError(
|
m_errorReporter.declarationError(
|
||||||
1686_error,
|
error,
|
||||||
overloads[i]->location(),
|
overloads[i]->location(),
|
||||||
ssl,
|
ssl,
|
||||||
_message
|
message
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@ -222,9 +236,8 @@ void ContractLevelChecker::checkAbstractDefinitions(ContractDefinition const& _c
|
|||||||
3656_error,
|
3656_error,
|
||||||
_contract.location(),
|
_contract.location(),
|
||||||
ssl,
|
ssl,
|
||||||
"Contract \"" + _contract.annotation().canonicalName
|
"Contract \"" + _contract.annotation().canonicalName + "\" should be marked as abstract."
|
||||||
+ "\" should be marked as abstract.");
|
);
|
||||||
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -60,7 +60,7 @@ private:
|
|||||||
void checkDuplicateFunctions(ContractDefinition const& _contract);
|
void checkDuplicateFunctions(ContractDefinition const& _contract);
|
||||||
void checkDuplicateEvents(ContractDefinition const& _contract);
|
void checkDuplicateEvents(ContractDefinition const& _contract);
|
||||||
template <class T>
|
template <class T>
|
||||||
void findDuplicateDefinitions(std::map<std::string, std::vector<T>> const& _definitions, std::string _message);
|
void findDuplicateDefinitions(std::map<std::string, std::vector<T>> const& _definitions);
|
||||||
/// Checks for unimplemented functions and modifiers.
|
/// Checks for unimplemented functions and modifiers.
|
||||||
void checkAbstractDefinitions(ContractDefinition const& _contract);
|
void checkAbstractDefinitions(ContractDefinition const& _contract);
|
||||||
/// Checks that the base constructor arguments are properly provided.
|
/// Checks that the base constructor arguments are properly provided.
|
||||||
|
@ -506,12 +506,13 @@ void OverrideChecker::checkOverride(OverrideProxy const& _overriding, OverridePr
|
|||||||
);
|
);
|
||||||
|
|
||||||
if (!_overriding.overrides())
|
if (!_overriding.overrides())
|
||||||
overrideError(_overriding, _super, "Overriding " + _overriding.astNodeName() + " is missing \"override\" specifier.");
|
overrideError(_overriding, _super, 9456_error, "Overriding " + _overriding.astNodeName() + " is missing \"override\" specifier.");
|
||||||
|
|
||||||
if (_super.isVariable())
|
if (_super.isVariable())
|
||||||
overrideError(
|
overrideError(
|
||||||
_super,
|
_super,
|
||||||
_overriding,
|
_overriding,
|
||||||
|
1452_error,
|
||||||
"Cannot override public state variable.",
|
"Cannot override public state variable.",
|
||||||
"Overriding " + _overriding.astNodeName() + " is here:"
|
"Overriding " + _overriding.astNodeName() + " is here:"
|
||||||
);
|
);
|
||||||
@ -519,6 +520,7 @@ void OverrideChecker::checkOverride(OverrideProxy const& _overriding, OverridePr
|
|||||||
overrideError(
|
overrideError(
|
||||||
_super,
|
_super,
|
||||||
_overriding,
|
_overriding,
|
||||||
|
4334_error,
|
||||||
"Trying to override non-virtual " + _super.astNodeName() + ". Did you forget to add \"virtual\"?",
|
"Trying to override non-virtual " + _super.astNodeName() + ". Did you forget to add \"virtual\"?",
|
||||||
"Overriding " + _overriding.astNodeName() + " is here:"
|
"Overriding " + _overriding.astNodeName() + " is here:"
|
||||||
);
|
);
|
||||||
@ -526,7 +528,7 @@ void OverrideChecker::checkOverride(OverrideProxy const& _overriding, OverridePr
|
|||||||
if (_overriding.isVariable())
|
if (_overriding.isVariable())
|
||||||
{
|
{
|
||||||
if (_super.visibility() != Visibility::External)
|
if (_super.visibility() != Visibility::External)
|
||||||
overrideError(_overriding, _super, "Public state variables can only override functions with external visibility.");
|
overrideError(_overriding, _super, 5225_error, "Public state variables can only override functions with external visibility.");
|
||||||
solAssert(_overriding.visibility() == Visibility::External, "");
|
solAssert(_overriding.visibility() == Visibility::External, "");
|
||||||
}
|
}
|
||||||
else if (_overriding.visibility() != _super.visibility())
|
else if (_overriding.visibility() != _super.visibility())
|
||||||
@ -537,7 +539,7 @@ void OverrideChecker::checkOverride(OverrideProxy const& _overriding, OverridePr
|
|||||||
_super.visibility() == Visibility::External &&
|
_super.visibility() == Visibility::External &&
|
||||||
_overriding.visibility() == Visibility::Public
|
_overriding.visibility() == Visibility::Public
|
||||||
))
|
))
|
||||||
overrideError(_overriding, _super, "Overriding " + _overriding.astNodeName() + " visibility differs.");
|
overrideError(_overriding, _super, 9098_error, "Overriding " + _overriding.astNodeName() + " visibility differs.");
|
||||||
}
|
}
|
||||||
|
|
||||||
if (_super.isFunction())
|
if (_super.isFunction())
|
||||||
@ -548,7 +550,7 @@ void OverrideChecker::checkOverride(OverrideProxy const& _overriding, OverridePr
|
|||||||
solAssert(functionType->hasEqualParameterTypes(*superType), "Override doesn't have equal parameters!");
|
solAssert(functionType->hasEqualParameterTypes(*superType), "Override doesn't have equal parameters!");
|
||||||
|
|
||||||
if (!functionType->hasEqualReturnTypes(*superType))
|
if (!functionType->hasEqualReturnTypes(*superType))
|
||||||
overrideError(_overriding, _super, "Overriding " + _overriding.astNodeName() + " return types differ.");
|
overrideError(_overriding, _super, 4822_error, "Overriding " + _overriding.astNodeName() + " return types differ.");
|
||||||
|
|
||||||
// This is only relevant for a function overriding a function.
|
// This is only relevant for a function overriding a function.
|
||||||
if (_overriding.isFunction())
|
if (_overriding.isFunction())
|
||||||
@ -557,6 +559,7 @@ void OverrideChecker::checkOverride(OverrideProxy const& _overriding, OverridePr
|
|||||||
overrideError(
|
overrideError(
|
||||||
_overriding,
|
_overriding,
|
||||||
_super,
|
_super,
|
||||||
|
2837_error,
|
||||||
"Overriding function changes state mutability from \"" +
|
"Overriding function changes state mutability from \"" +
|
||||||
stateMutabilityToString(_super.stateMutability()) +
|
stateMutabilityToString(_super.stateMutability()) +
|
||||||
"\" to \"" +
|
"\" to \"" +
|
||||||
@ -568,6 +571,7 @@ void OverrideChecker::checkOverride(OverrideProxy const& _overriding, OverridePr
|
|||||||
overrideError(
|
overrideError(
|
||||||
_overriding,
|
_overriding,
|
||||||
_super,
|
_super,
|
||||||
|
4593_error,
|
||||||
"Overriding an implemented function with an unimplemented function is not allowed."
|
"Overriding an implemented function with an unimplemented function is not allowed."
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
@ -577,6 +581,7 @@ void OverrideChecker::checkOverride(OverrideProxy const& _overriding, OverridePr
|
|||||||
void OverrideChecker::overrideListError(
|
void OverrideChecker::overrideListError(
|
||||||
OverrideProxy const& _item,
|
OverrideProxy const& _item,
|
||||||
set<ContractDefinition const*, CompareByID> _secondary,
|
set<ContractDefinition const*, CompareByID> _secondary,
|
||||||
|
ErrorId _error,
|
||||||
string const& _message1,
|
string const& _message1,
|
||||||
string const& _message2
|
string const& _message2
|
||||||
)
|
)
|
||||||
@ -594,7 +599,7 @@ void OverrideChecker::overrideListError(
|
|||||||
contractSingularPlural = "contracts ";
|
contractSingularPlural = "contracts ";
|
||||||
|
|
||||||
m_errorReporter.typeError(
|
m_errorReporter.typeError(
|
||||||
5883_error,
|
_error,
|
||||||
_item.overrides() ? _item.overrides()->location() : _item.location(),
|
_item.overrides() ? _item.overrides()->location() : _item.location(),
|
||||||
ssl,
|
ssl,
|
||||||
_message1 +
|
_message1 +
|
||||||
@ -605,10 +610,10 @@ void OverrideChecker::overrideListError(
|
|||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
void OverrideChecker::overrideError(Declaration const& _overriding, Declaration const& _super, string const& _message, string const& _secondaryMsg)
|
void OverrideChecker::overrideError(Declaration const& _overriding, Declaration const& _super, ErrorId _error, string const& _message, string const& _secondaryMsg)
|
||||||
{
|
{
|
||||||
m_errorReporter.typeError(
|
m_errorReporter.typeError(
|
||||||
9456_error,
|
_error,
|
||||||
_overriding.location(),
|
_overriding.location(),
|
||||||
SecondarySourceLocation().append(_secondaryMsg, _super.location()),
|
SecondarySourceLocation().append(_secondaryMsg, _super.location()),
|
||||||
_message
|
_message
|
||||||
@ -616,10 +621,10 @@ void OverrideChecker::overrideError(Declaration const& _overriding, Declaration
|
|||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
void OverrideChecker::overrideError(OverrideProxy const& _overriding, OverrideProxy const& _super, string const& _message, string const& _secondaryMsg)
|
void OverrideChecker::overrideError(OverrideProxy const& _overriding, OverrideProxy const& _super, ErrorId _error, string const& _message, string const& _secondaryMsg)
|
||||||
{
|
{
|
||||||
m_errorReporter.typeError(
|
m_errorReporter.typeError(
|
||||||
1452_error,
|
_error,
|
||||||
_overriding.location(),
|
_overriding.location(),
|
||||||
SecondarySourceLocation().append(_secondaryMsg, _super.location()),
|
SecondarySourceLocation().append(_secondaryMsg, _super.location()),
|
||||||
_message
|
_message
|
||||||
@ -810,6 +815,7 @@ void OverrideChecker::checkOverrideList(OverrideProxy _item, OverrideProxyBySign
|
|||||||
overrideListError(
|
overrideListError(
|
||||||
_item,
|
_item,
|
||||||
missingContracts,
|
missingContracts,
|
||||||
|
4327_error,
|
||||||
_item.astNodeNameCapitalized() + " needs to specify overridden ",
|
_item.astNodeNameCapitalized() + " needs to specify overridden ",
|
||||||
""
|
""
|
||||||
);
|
);
|
||||||
@ -819,6 +825,7 @@ void OverrideChecker::checkOverrideList(OverrideProxy _item, OverrideProxyBySign
|
|||||||
overrideListError(
|
overrideListError(
|
||||||
_item,
|
_item,
|
||||||
surplusContracts,
|
surplusContracts,
|
||||||
|
2353_error,
|
||||||
"Invalid ",
|
"Invalid ",
|
||||||
"specified in override list: "
|
"specified in override list: "
|
||||||
);
|
);
|
||||||
|
@ -32,6 +32,7 @@
|
|||||||
namespace solidity::langutil
|
namespace solidity::langutil
|
||||||
{
|
{
|
||||||
class ErrorReporter;
|
class ErrorReporter;
|
||||||
|
struct ErrorId;
|
||||||
struct SourceLocation;
|
struct SourceLocation;
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -160,18 +161,21 @@ private:
|
|||||||
void overrideListError(
|
void overrideListError(
|
||||||
OverrideProxy const& _item,
|
OverrideProxy const& _item,
|
||||||
std::set<ContractDefinition const*, CompareByID> _secondary,
|
std::set<ContractDefinition const*, CompareByID> _secondary,
|
||||||
|
langutil::ErrorId _error,
|
||||||
std::string const& _message1,
|
std::string const& _message1,
|
||||||
std::string const& _message2
|
std::string const& _message2
|
||||||
);
|
);
|
||||||
void overrideError(
|
void overrideError(
|
||||||
Declaration const& _overriding,
|
Declaration const& _overriding,
|
||||||
Declaration const& _super,
|
Declaration const& _super,
|
||||||
|
langutil::ErrorId _error,
|
||||||
std::string const& _message,
|
std::string const& _message,
|
||||||
std::string const& _secondaryMsg = "Overridden function is here:"
|
std::string const& _secondaryMsg = "Overridden function is here:"
|
||||||
);
|
);
|
||||||
void overrideError(
|
void overrideError(
|
||||||
OverrideProxy const& _overriding,
|
OverrideProxy const& _overriding,
|
||||||
OverrideProxy const& _super,
|
OverrideProxy const& _super,
|
||||||
|
langutil::ErrorId _error,
|
||||||
std::string const& _message,
|
std::string const& _message,
|
||||||
std::string const& _secondaryMsg = "Overridden function is here:"
|
std::string const& _secondaryMsg = "Overridden function is here:"
|
||||||
);
|
);
|
||||||
|
@ -21,8 +21,6 @@
|
|||||||
#include <libsolidity/formal/SymbolicState.h>
|
#include <libsolidity/formal/SymbolicState.h>
|
||||||
#include <libsolidity/formal/SymbolicTypes.h>
|
#include <libsolidity/formal/SymbolicTypes.h>
|
||||||
|
|
||||||
#include <boost/algorithm/string/replace.hpp>
|
|
||||||
|
|
||||||
using namespace std;
|
using namespace std;
|
||||||
using namespace solidity;
|
using namespace solidity;
|
||||||
using namespace solidity::util;
|
using namespace solidity::util;
|
||||||
@ -594,8 +592,7 @@ void BMC::checkConstantCondition(BMCVerificationTarget& _target)
|
|||||||
*_target.expression,
|
*_target.expression,
|
||||||
_target.constraints,
|
_target.constraints,
|
||||||
_target.value,
|
_target.value,
|
||||||
_target.callStack,
|
_target.callStack
|
||||||
"Condition is always $VALUE."
|
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -613,6 +610,8 @@ void BMC::checkUnderflow(BMCVerificationTarget& _target, smt::Expression const&
|
|||||||
_target.callStack,
|
_target.callStack,
|
||||||
_target.modelExpressions,
|
_target.modelExpressions,
|
||||||
_target.expression->location(),
|
_target.expression->location(),
|
||||||
|
4144_error,
|
||||||
|
8312_error,
|
||||||
"Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")",
|
"Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")",
|
||||||
"<result>",
|
"<result>",
|
||||||
&_target.value
|
&_target.value
|
||||||
@ -633,6 +632,8 @@ void BMC::checkOverflow(BMCVerificationTarget& _target, smt::Expression const& _
|
|||||||
_target.callStack,
|
_target.callStack,
|
||||||
_target.modelExpressions,
|
_target.modelExpressions,
|
||||||
_target.expression->location(),
|
_target.expression->location(),
|
||||||
|
2661_error,
|
||||||
|
8065_error,
|
||||||
"Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")",
|
"Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")",
|
||||||
"<result>",
|
"<result>",
|
||||||
&_target.value
|
&_target.value
|
||||||
@ -647,6 +648,8 @@ void BMC::checkDivByZero(BMCVerificationTarget& _target)
|
|||||||
_target.callStack,
|
_target.callStack,
|
||||||
_target.modelExpressions,
|
_target.modelExpressions,
|
||||||
_target.expression->location(),
|
_target.expression->location(),
|
||||||
|
3046_error,
|
||||||
|
5272_error,
|
||||||
"Division by zero",
|
"Division by zero",
|
||||||
"<result>",
|
"<result>",
|
||||||
&_target.value
|
&_target.value
|
||||||
@ -661,6 +664,8 @@ void BMC::checkBalance(BMCVerificationTarget& _target)
|
|||||||
_target.callStack,
|
_target.callStack,
|
||||||
_target.modelExpressions,
|
_target.modelExpressions,
|
||||||
_target.expression->location(),
|
_target.expression->location(),
|
||||||
|
1236_error,
|
||||||
|
4010_error,
|
||||||
"Insufficient funds",
|
"Insufficient funds",
|
||||||
"address(this).balance"
|
"address(this).balance"
|
||||||
);
|
);
|
||||||
@ -675,6 +680,8 @@ void BMC::checkAssert(BMCVerificationTarget& _target)
|
|||||||
_target.callStack,
|
_target.callStack,
|
||||||
_target.modelExpressions,
|
_target.modelExpressions,
|
||||||
_target.expression->location(),
|
_target.expression->location(),
|
||||||
|
4661_error,
|
||||||
|
7812_error,
|
||||||
"Assertion violation"
|
"Assertion violation"
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
@ -705,9 +712,11 @@ void BMC::addVerificationTarget(
|
|||||||
|
|
||||||
void BMC::checkCondition(
|
void BMC::checkCondition(
|
||||||
smt::Expression _condition,
|
smt::Expression _condition,
|
||||||
vector<SMTEncoder::CallStackEntry> const& callStack,
|
vector<SMTEncoder::CallStackEntry> const& _callStack,
|
||||||
pair<vector<smt::Expression>, vector<string>> const& _modelExpressions,
|
pair<vector<smt::Expression>, vector<string>> const& _modelExpressions,
|
||||||
SourceLocation const& _location,
|
SourceLocation const& _location,
|
||||||
|
ErrorId _errorHappens,
|
||||||
|
ErrorId _errorMightHappen,
|
||||||
string const& _description,
|
string const& _description,
|
||||||
string const& _additionalValueName,
|
string const& _additionalValueName,
|
||||||
smt::Expression const* _additionalValue
|
smt::Expression const* _additionalValue
|
||||||
@ -719,7 +728,7 @@ void BMC::checkCondition(
|
|||||||
vector<smt::Expression> expressionsToEvaluate;
|
vector<smt::Expression> expressionsToEvaluate;
|
||||||
vector<string> expressionNames;
|
vector<string> expressionNames;
|
||||||
tie(expressionsToEvaluate, expressionNames) = _modelExpressions;
|
tie(expressionsToEvaluate, expressionNames) = _modelExpressions;
|
||||||
if (callStack.size())
|
if (_callStack.size())
|
||||||
if (_additionalValue)
|
if (_additionalValue)
|
||||||
{
|
{
|
||||||
expressionsToEvaluate.emplace_back(*_additionalValue);
|
expressionsToEvaluate.emplace_back(*_additionalValue);
|
||||||
@ -750,7 +759,7 @@ void BMC::checkCondition(
|
|||||||
{
|
{
|
||||||
std::ostringstream message;
|
std::ostringstream message;
|
||||||
message << _description << " happens here";
|
message << _description << " happens here";
|
||||||
if (callStack.size())
|
if (_callStack.size())
|
||||||
{
|
{
|
||||||
std::ostringstream modelMessage;
|
std::ostringstream modelMessage;
|
||||||
modelMessage << " for:\n";
|
modelMessage << " for:\n";
|
||||||
@ -763,11 +772,11 @@ void BMC::checkCondition(
|
|||||||
for (auto const& eval: sortedModel)
|
for (auto const& eval: sortedModel)
|
||||||
modelMessage << " " << eval.first << " = " << eval.second << "\n";
|
modelMessage << " " << eval.first << " = " << eval.second << "\n";
|
||||||
m_errorReporter.warning(
|
m_errorReporter.warning(
|
||||||
4334_error,
|
_errorHappens,
|
||||||
_location,
|
_location,
|
||||||
message.str(),
|
message.str(),
|
||||||
SecondarySourceLocation().append(modelMessage.str(), SourceLocation{})
|
SecondarySourceLocation().append(modelMessage.str(), SourceLocation{})
|
||||||
.append(SMTEncoder::callStackMessage(callStack))
|
.append(SMTEncoder::callStackMessage(_callStack))
|
||||||
.append(move(secondaryLocation))
|
.append(move(secondaryLocation))
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
@ -781,7 +790,7 @@ void BMC::checkCondition(
|
|||||||
case smt::CheckResult::UNSATISFIABLE:
|
case smt::CheckResult::UNSATISFIABLE:
|
||||||
break;
|
break;
|
||||||
case smt::CheckResult::UNKNOWN:
|
case smt::CheckResult::UNKNOWN:
|
||||||
m_errorReporter.warning(5225_error, _location, _description + " might happen here.", secondaryLocation);
|
m_errorReporter.warning(_errorMightHappen, _location, _description + " might happen here.", secondaryLocation);
|
||||||
break;
|
break;
|
||||||
case smt::CheckResult::CONFLICTING:
|
case smt::CheckResult::CONFLICTING:
|
||||||
m_errorReporter.warning(1584_error, _location, "At least two SMT solvers provided conflicting answers. Results might not be sound.");
|
m_errorReporter.warning(1584_error, _location, "At least two SMT solvers provided conflicting answers. Results might not be sound.");
|
||||||
@ -798,8 +807,7 @@ void BMC::checkBooleanNotConstant(
|
|||||||
Expression const& _condition,
|
Expression const& _condition,
|
||||||
smt::Expression const& _constraints,
|
smt::Expression const& _constraints,
|
||||||
smt::Expression const& _value,
|
smt::Expression const& _value,
|
||||||
vector<SMTEncoder::CallStackEntry> const& _callStack,
|
vector<SMTEncoder::CallStackEntry> const& _callStack
|
||||||
string const& _description
|
|
||||||
)
|
)
|
||||||
{
|
{
|
||||||
// Do not check for const-ness if this is a constant.
|
// Do not check for const-ness if this is a constant.
|
||||||
@ -832,22 +840,22 @@ void BMC::checkBooleanNotConstant(
|
|||||||
m_errorReporter.warning(2512_error, _condition.location(), "Condition unreachable.", SMTEncoder::callStackMessage(_callStack));
|
m_errorReporter.warning(2512_error, _condition.location(), "Condition unreachable.", SMTEncoder::callStackMessage(_callStack));
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
string value;
|
string description;
|
||||||
if (positiveResult == smt::CheckResult::SATISFIABLE)
|
if (positiveResult == smt::CheckResult::SATISFIABLE)
|
||||||
{
|
{
|
||||||
solAssert(negatedResult == smt::CheckResult::UNSATISFIABLE, "");
|
solAssert(negatedResult == smt::CheckResult::UNSATISFIABLE, "");
|
||||||
value = "true";
|
description = "Condition is always true.";
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
solAssert(positiveResult == smt::CheckResult::UNSATISFIABLE, "");
|
solAssert(positiveResult == smt::CheckResult::UNSATISFIABLE, "");
|
||||||
solAssert(negatedResult == smt::CheckResult::SATISFIABLE, "");
|
solAssert(negatedResult == smt::CheckResult::SATISFIABLE, "");
|
||||||
value = "false";
|
description = "Condition is always false.";
|
||||||
}
|
}
|
||||||
m_errorReporter.warning(
|
m_errorReporter.warning(
|
||||||
6838_error,
|
6838_error,
|
||||||
_condition.location(),
|
_condition.location(),
|
||||||
boost::algorithm::replace_all_copy(_description, "$VALUE", value),
|
description,
|
||||||
SMTEncoder::callStackMessage(_callStack)
|
SMTEncoder::callStackMessage(_callStack)
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
@ -44,6 +44,7 @@ using solidity::util::h256;
|
|||||||
namespace solidity::langutil
|
namespace solidity::langutil
|
||||||
{
|
{
|
||||||
class ErrorReporter;
|
class ErrorReporter;
|
||||||
|
struct ErrorId;
|
||||||
struct SourceLocation;
|
struct SourceLocation;
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -144,22 +145,22 @@ private:
|
|||||||
/// Check that a condition can be satisfied.
|
/// Check that a condition can be satisfied.
|
||||||
void checkCondition(
|
void checkCondition(
|
||||||
smt::Expression _condition,
|
smt::Expression _condition,
|
||||||
std::vector<CallStackEntry> const& callStack,
|
std::vector<CallStackEntry> const& _callStack,
|
||||||
std::pair<std::vector<smt::Expression>, std::vector<std::string>> const& _modelExpressions,
|
std::pair<std::vector<smt::Expression>, std::vector<std::string>> const& _modelExpressions,
|
||||||
langutil::SourceLocation const& _location,
|
langutil::SourceLocation const& _location,
|
||||||
|
langutil::ErrorId _errorHappens,
|
||||||
|
langutil::ErrorId _errorMightHappen,
|
||||||
std::string const& _description,
|
std::string const& _description,
|
||||||
std::string const& _additionalValueName = "",
|
std::string const& _additionalValueName = "",
|
||||||
smt::Expression const* _additionalValue = nullptr
|
smt::Expression const* _additionalValue = nullptr
|
||||||
);
|
);
|
||||||
/// Checks that a boolean condition is not constant. Do not warn if the expression
|
/// Checks that a boolean condition is not constant. Do not warn if the expression
|
||||||
/// is a literal constant.
|
/// is a literal constant.
|
||||||
/// @param _description the warning string, $VALUE will be replaced by the constant value.
|
|
||||||
void checkBooleanNotConstant(
|
void checkBooleanNotConstant(
|
||||||
Expression const& _condition,
|
Expression const& _condition,
|
||||||
smt::Expression const& _constraints,
|
smt::Expression const& _constraints,
|
||||||
smt::Expression const& _value,
|
smt::Expression const& _value,
|
||||||
std::vector<CallStackEntry> const& _callStack,
|
std::vector<CallStackEntry> const& _callStack
|
||||||
std::string const& _description
|
|
||||||
);
|
);
|
||||||
std::pair<smt::CheckResult, std::vector<std::string>>
|
std::pair<smt::CheckResult, std::vector<std::string>>
|
||||||
checkSatisfiableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate);
|
checkSatisfiableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate);
|
||||||
|
Loading…
Reference in New Issue
Block a user