diff options
| -rw-r--r-- | Changelog.md | 2 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 15 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 2 | ||||
| -rw-r--r-- | test/libsolidity/SMTChecker.cpp | 11 |
4 files changed, 27 insertions, 3 deletions
diff --git a/Changelog.md b/Changelog.md index e0b8cbc6..0817faab 100644 --- a/Changelog.md +++ b/Changelog.md @@ -10,6 +10,7 @@ Features: * 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: 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: 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). @@ -25,7 +26,6 @@ Features: * Build system: Support Ubuntu Bionic. * SMTChecker: Integration with CVC4 SMT solver * Syntax Checker: Warn about functions named "constructor". - * SMTChecker: Support to integer and Bool state variables Bugfixes: * Type Checker: Improve error message for failed function overload resolution. diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 358f1c58..425c5c1e 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -58,12 +58,23 @@ void SMTChecker::analyze(SourceUnit const& _source) _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) { if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value()) assignment(_varDecl, *_varDecl.value(), _varDecl.location()); - else if (_varDecl.isStateVariable() && _varDecl.type()->isValueType()) - createVariable(_varDecl); } bool SMTChecker::visit(FunctionDefinition const& _function) diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 6e64235e..50d40ab9 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -50,6 +50,8 @@ private: // because the order of expression evaluation is undefined // 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 bool visit(FunctionDefinition const& _node) override; virtual void endVisit(FunctionDefinition const& _node) override; diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index ce3569f3..5f54db6d 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -531,6 +531,17 @@ BOOST_AUTO_TEST_CASE(storage_value_vars) } )"; 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) |