Merge pull request #10310 from blishko/issue-10306

[SMTChecker] Adding a dummy frame to the call stack for the implicit constructor

libsolidity/formal/BMC.cpp

@@ -120,7 +120,10 @@ void BMC::endVisit(ContractDefinition const& _contract)
 		constructor->accept(*this);
 	else
 	{
+		/// Visiting implicit constructor - we need a dummy callstack frame
+		pushCallStack({nullptr, nullptr});
 		inlineConstructorHierarchy(_contract);
+		popCallStack();
 		/// Check targets created by state variable initialization.
 		smtutil::Expression constraints = m_context.assertions();
 		checkVerificationTargets(constraints);
@@ -831,10 +834,9 @@ void BMC::checkCondition(
 	{
 	case smtutil::CheckResult::SATISFIABLE:
 	{
+		solAssert(!_callStack.empty(), "");
 		std::ostringstream message;
 		message << "BMC: " << _description << " happens here.";
-		if (_callStack.size())
-		{
 		std::ostringstream modelMessage;
 		modelMessage << "Counterexample:\n";
 		solAssert(values.size() == expressionNames.size(), "");
@@ -854,9 +856,6 @@ void BMC::checkCondition(
 			.append(SMTEncoder::callStackMessage(_callStack))
 			.append(move(secondaryLocation))
 		);
-		}
-		else
-			m_errorReporter.warning(6084_error, _location, message.str(), secondaryLocation);
 		break;
 	}
 	case smtutil::CheckResult::UNSATISFIABLE:

test/libsolidity/smtCheckerTests/bmc_coverage/assert_in_constructor.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint x = initX();
+
+	function initX() internal pure returns (uint) {
+		return 42;
+	}
+}
+
+contract D is C {
+	uint y;
+
+	constructor() {
+		assert(x == 42);
+		y = x;
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----

test/libsolidity/smtCheckerTests/bmc_coverage/implicit_constructor_with_function_calls.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint x = initX();
+	uint y = initY();
+
+    function initX() internal pure returns (uint) {
+		return 42;
+	}
+
+	function initY() internal view returns (uint) {
+		assert(x == 42);
+		return x;
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (205-220): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/bmc_coverage/math.sol

@@ -22,4 +22,4 @@ contract C {
 // Warning 4144: (217-222): BMC: Underflow (resulting value less than 0) happens here.
 // Warning 2661: (293-298): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 3046: (369-374): BMC: Division by zero happens here.
-// Warning 6084: (68-73): BMC: Underflow (resulting value less than 0) happens here.
+// Warning 4144: (68-73): BMC: Underflow (resulting value less than 0) happens here.