Merge pull request #6640 from ethereum/smt_inherited_state_vars

[SMTChecker] Fix ICE in inherited state var

Changelog.md

@@ -4,10 +4,12 @@ Language Features:
 
 
 Compiler Features:
+ * SMTChecker: Support inherited state variables.
 
 
 Bugfixes:
  * SMTChecker: Fix bad cast in base constructor modifier.
+ * SMTChecker: Fix internal error when visiting state variable inherited from base class.
 
 
 

libsolidity/formal/SMTChecker.cpp

@@ -78,8 +78,10 @@ void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _
 
 bool SMTChecker::visit(ContractDefinition const& _contract)
 {
-	for (auto _var : _contract.stateVariables())
-		createVariable(*_var);
+	for (auto const& contract: _contract.annotation().linearizedBaseContracts)
+		for (auto var : contract->stateVariables())
+			if (*contract == _contract || var->isVisibleInDerivedContracts())
+				createVariable(*var);
 	return true;
 }
 

test/libsolidity/smtCheckerTests/inheritance/state_variables.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract Base {
+	uint x;
+	uint z;
+	uint private t;
+}
+
+contract C is Base {
+	function f(uint y) public {
+		require(x < 10);
+		require(y < 100);
+		z = x + y;
+		assert(z < 150);
+	}
+}
+// ----

test/libsolidity/smtCheckerTests/inheritance/state_variables_2.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract Base1 {
+	uint x;
+	uint private t;
+}
+
+contract Base2 is Base1 {
+	uint z;
+	uint private t;
+}
+
+contract C is Base2 {
+	function f(uint y) public {
+		require(x < 10);
+		require(y < 100);
+		z = x + y;
+		assert(z < 150);
+	}
+}
+// ----

test/libsolidity/smtCheckerTests/inheritance/state_variables_3.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract Base {
+	uint x;
+	uint private t;
+}
+
+contract C is Base {
+
+	uint private z;
+	function f(uint y) public {
+		require(x < 10);
+		require(y < 100);
+		z = x + y;
+		assert(z < 150);
+	}
+}
+// ----