cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #6481 from ethereum/smt_inline_asm_warning

Browse Source 
[SMTChecker] Show unsupported warning for asm blocks
This commit is contained in:
Daniel Kirchner 2019-04-12 12:36:26 +02:00 committed by GitHub
commit 65991c0922
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 35 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -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.

9
libsolidity/formal/SMTChecker.cpp
View File

@ -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);

1
libsolidity/formal/SMTChecker.h
View File

@ -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.

11
test/libsolidity/smtCheckerTests/inline_assembly/empty.sol Normal file
View File

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

13
test/libsolidity/smtCheckerTests/inline_assembly/local_var.sol Normal file
View File

@ -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.