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

[SMTChecker] Declaring all state vars before any function is visited

Browse Source
This commit is contained in:
Leonardo Alt 2018-04-30 16:30:41 +02:00 committed by chriseth
parent 2dbb35d4a8
commit 4117e859eb
4 changed files with 27 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Changelog.md
View File

@ -10,6 +10,7 @@ Features:
* Optimizer: Remove unnecessary masking of the result of known short instructions (``ADDRESS``, ``CALLER``, ``ORIGIN`` and ``COINBASE``). * Optimizer: Remove unnecessary masking of the result of known short instructions (``ADDRESS``, ``CALLER``, ``ORIGIN`` and ``COINBASE``).
* Parser: Display nicer error messages by showing the actual tokens and not internal names. * Parser: Display nicer error messages by showing the actual tokens and not internal names.
* Parser: Use the entire location of the token instead of only its starting position as source location for parser errors. * Parser: Use the entire location of the token instead of only its starting position as source location for parser errors.
* SMT Checker: Support state variables of integer and bool type.
* Type Checker: Deprecate the ``years`` unit denomination and raise a warning for it (or an error as experimental 0.5.0 feature). * Type Checker: Deprecate the ``years`` unit denomination and raise a warning for it (or an error as experimental 0.5.0 feature).
* Type Checker: Make literals (without explicit type casting) an error for tight packing as experimental 0.5.0 feature. * Type Checker: Make literals (without explicit type casting) an error for tight packing as experimental 0.5.0 feature.
* Type Checker: Warn about wildcard tuple assignments (this will turn into an error with version 0.5.0). * Type Checker: Warn about wildcard tuple assignments (this will turn into an error with version 0.5.0).
@ -25,7 +26,6 @@ Features:
* Build system: Support Ubuntu Bionic. * Build system: Support Ubuntu Bionic.
* SMTChecker: Integration with CVC4 SMT solver * SMTChecker: Integration with CVC4 SMT solver
* Syntax Checker: Warn about functions named "constructor". * Syntax Checker: Warn about functions named "constructor".
* SMTChecker: Support to integer and Bool state variables
Bugfixes: Bugfixes:
* Type Checker: Improve error message for failed function overload resolution. * Type Checker: Improve error message for failed function overload resolution.

15
libsolidity/formal/SMTChecker.cpp
View File

@ -58,12 +58,23 @@ void SMTChecker::analyze(SourceUnit const& _source)
_source.accept(*this); _source.accept(*this);
} }
bool SMTChecker::visit(ContractDefinition const& _contract)
{
for (auto _var : _contract.stateVariables())
if (_var->type()->isValueType())
createVariable(*_var);
return true;
}
void SMTChecker::endVisit(ContractDefinition const&)
{
m_stateVariables.clear();
}
void SMTChecker::endVisit(VariableDeclaration const& _varDecl) void SMTChecker::endVisit(VariableDeclaration const& _varDecl)
{ {
if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value()) if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value())
assignment(_varDecl, *_varDecl.value(), _varDecl.location()); assignment(_varDecl, *_varDecl.value(), _varDecl.location());
else if (_varDecl.isStateVariable() && _varDecl.type()->isValueType())
createVariable(_varDecl);
} }
bool SMTChecker::visit(FunctionDefinition const& _function) bool SMTChecker::visit(FunctionDefinition const& _function)

2
libsolidity/formal/SMTChecker.h
View File

@ -50,6 +50,8 @@ private:
// because the order of expression evaluation is undefined // because the order of expression evaluation is undefined
// TODO: or just force a certain order, but people might have a different idea about that. // TODO: or just force a certain order, but people might have a different idea about that.
virtual bool visit(ContractDefinition const& _node) override;
virtual void endVisit(ContractDefinition const& _node) override;
virtual void endVisit(VariableDeclaration const& _node) override; virtual void endVisit(VariableDeclaration const& _node) override;
virtual bool visit(FunctionDefinition const& _node) override; virtual bool visit(FunctionDefinition const& _node) override;
virtual void endVisit(FunctionDefinition const& _node) override; virtual void endVisit(FunctionDefinition const& _node) override;

11
test/libsolidity/SMTChecker.cpp
View File

@ -531,6 +531,17 @@ BOOST_AUTO_TEST_CASE(storage_value_vars)
} }
)"; )";
CHECK_SUCCESS_NO_WARNINGS(text); CHECK_SUCCESS_NO_WARNINGS(text);
text = R"(
contract C
{
function f() public view {
assert(c > 0);
}
uint c;
}
)";
CHECK_WARNING(text, "Assertion violation happens here");
} }
BOOST_AUTO_TEST_CASE(while_loop_simple) BOOST_AUTO_TEST_CASE(while_loop_simple)