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

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)