[SMTChecker] Show unsupported warning for asm blocks

Changelog.md

@@ -13,6 +13,7 @@ Compiler Features:
  * ABI Decoder: Raise a runtime error on dirty inputs when using the experimental decoder.
  * SMTChecker: Support arithmetic compound assignment operators.
  * SMTChecker: Support unary increment and decrement for array and mapping access.
+ * SMTChecker: Show unsupported warning for inline assembly blocks.
  * Optimizer: Add rule for shifts by constants larger than 255 for Constantinople.
  * Optimizer: Add rule to simplify certain ANDs and SHL combinations
  * Yul: Adds break and continue keywords to for-loop syntax.

libsolidity/formal/SMTChecker.cpp

@@ -192,6 +192,15 @@ void SMTChecker::endVisit(FunctionDefinition const&)
 	m_modifierDepthStack.pop_back();
 }
 
+bool SMTChecker::visit(InlineAssembly const& _inlineAsm)
+{
+	m_errorReporter.warning(
+		_inlineAsm.location(),
+		"Assertion checker does not support inline assembly."
+	);
+	return false;
+}
+
 bool SMTChecker::visit(IfStatement const& _node)
 {
 	_node.condition().accept(*this);

libsolidity/formal/SMTChecker.h

@@ -87,6 +87,7 @@ private:
 	void endVisit(Return const& _node) override;
 	bool visit(MemberAccess const& _node) override;
 	void endVisit(IndexAccess const& _node) override;
+	bool visit(InlineAssembly const& _node) override;
 
 	/// Do not visit subtree if node is a RationalNumber.
 	/// Symbolic _expr is the rational literal.

test/libsolidity/smtCheckerTests/inline_assembly/empty.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		assembly {
+		}
+	}
+}
+// ----
+// Warning: (76-93): Assertion checker does not support inline assembly.

test/libsolidity/smtCheckerTests/inline_assembly/local_var.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure returns (uint) {
+		assembly {
+			x := 2
+		}
+		return x;
+	}
+}
+// ----
+// Warning: (97-130): Assertion checker does not support inline assembly.