Merge pull request #7823 from ethereum/smt_typetype_msg

[SMTChecker] Do not visit the name of a modifier invocation

libsolidity/formal/SMTEncoder.cpp

@@ -537,6 +537,15 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 	}
 }
 
+bool SMTEncoder::visit(ModifierInvocation const& _node)
+{
+	if (auto const* args = _node.arguments())
+		for (auto const& arg: *args)
+			if (arg)
+				arg->accept(*this);
+	return false;
+}
+
 void SMTEncoder::initContract(ContractDefinition const& _contract)
 {
 	solAssert(m_currentContract == nullptr, "");
@@ -605,9 +614,7 @@ void SMTEncoder::endVisit(Identifier const& _identifier)
 		defineExpr(_identifier, m_context.thisAddress());
 		m_uninterpretedTerms.insert(&_identifier);
 	}
-	else if (
-		_identifier.annotation().type->category() != Type::Category::Modifier
-	)
+	else
 		createExpr(_identifier);
 }
 

libsolidity/formal/SMTEncoder.h

@@ -82,6 +82,7 @@ class SMTEncoder: public ASTConstVisitor
 	bool visit(BinaryOperation const& _node) override;
 	void endVisit(BinaryOperation const& _node) override;
 	void endVisit(FunctionCall const& _node) override;
+	bool visit(ModifierInvocation const& _node) override;
 	void endVisit(Identifier const& _node) override;
 	void endVisit(ElementaryTypeNameExpression const& _node) override;
 	void endVisit(Literal const& _node) override;

test/libsolidity/smtCheckerTests/functions/constructor_base_basic.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x;
+	constructor() public {
+		x = 2;
+	}
+}
+
+contract B is A {
+	constructor() A() public {
+		x = 3;
+	}
+}
+// ----
+// Warning: (56-90): Assertion checker does not yet support constructors.
+// Warning: (113-151): Assertion checker does not yet support constructors.