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 #11052 from blishko/issue-10986

Browse Source 
[SMTChecker] Correct handling of FixedBytes constants initialized with string literal
This commit is contained in:
Leonardo 2021-03-04 16:51:22 +01:00 committed by GitHub
commit d42d0faf41
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 22 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Changelog.md
View File

@ -7,8 +7,8 @@ Compiler Features:
Bugfixes: Bugfixes:
* SMTChecker: Fix internal error on ``FixedBytes`` constant initialized with string literal.
* SMTChecker: Fix internal error on pushing to ``string`` casted to ``bytes``. * SMTChecker: Fix internal error on pushing to ``string`` casted to ``bytes``.
AST Changes: AST Changes:

1
libsmtutil/SolverInterface.h
View File

@ -260,6 +260,7 @@ public:
} }
friend Expression operator==(Expression _a, Expression _b) friend Expression operator==(Expression _a, Expression _b)
{ {
smtAssert(_a.sort->kind == _b.sort->kind, "Trying to create an 'equal' expression with different sorts");
return Expression("=", std::move(_a), std::move(_b), Kind::Bool); return Expression("=", std::move(_a), std::move(_b), Kind::Bool);
} }
friend Expression operator!=(Expression _a, Expression _b) friend Expression operator!=(Expression _a, Expression _b)

2
libsolidity/formal/SMTEncoder.cpp
View File

@ -940,7 +940,7 @@ void SMTEncoder::endVisit(Identifier const& _identifier)
{ {
solAssert(decl->value(), ""); solAssert(decl->value(), "");
decl->value()->accept(*this); decl->value()->accept(*this);
defineExpr(_identifier, expr(*decl->value())); defineExpr(_identifier, expr(*decl->value(), _identifier.annotation().type));
} }
} }
else else

10
test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_constant_initialization_1.sol Normal file
View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract MockContract {
bytes4 public constant SENTINEL_ANY_MOCKS = hex"01";
mapping(bytes4 => bytes4) methodIdMocks;
constructor() {
methodIdMocks[SENTINEL_ANY_MOCKS] = 0;
}
}

9
test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_constant_initialization_2.sol Normal file
View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract MockContract {
bytes4 public constant SENTINEL_ANY_MOCKS = hex"01";
constructor() {
assert(SENTINEL_ANY_MOCKS >= 0);
}
}