cerc-io/solidity
10
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 #9050 from ethereum/smt_fix_nonvalue_asgn

Browse Source 
[SMTChecker] Fix ICE on index access assignment inside single branches
This commit is contained in:
chriseth 2020-05-28 16:25:46 +02:00 committed by GitHub
commit 0b216f5771
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 26 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -27,6 +27,7 @@ Bugfixes:
* Code Generator: Trigger proper unimplemented errors on certain array copy operations. * Code Generator: Trigger proper unimplemented errors on certain array copy operations.
* SMTChecker: Fix internal error when applying arithmetic operators to fixed point variables. * SMTChecker: Fix internal error when applying arithmetic operators to fixed point variables.
* SMTChecker: Fix internal error when short circuiting Boolean expressions with function calls in state variable initialization. * SMTChecker: Fix internal error when short circuiting Boolean expressions with function calls in state variable initialization.
* SMTChecker: Fix internal error when assigning to index access inside branches.
### 0.6.8 (2020-05-14) ### 0.6.8 (2020-05-14)

7
libsolidity/formal/SMTEncoder.cpp
View File

@ -361,7 +361,12 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
else if (!smt::isSupportedType(_assignment.annotation().type->category())) else if (!smt::isSupportedType(_assignment.annotation().type->category()))
{ {
// Give it a new index anyway to keep the SSA scheme sound. // Give it a new index anyway to keep the SSA scheme sound.
if (auto varDecl = identifierToVariable(_assignment.leftHandSide()))
Expression const* base = &_assignment.leftHandSide();
if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(base))
base = leftmostBase(*indexAccess);
if (auto varDecl = identifierToVariable(*base))
m_context.newValue(*varDecl); m_context.newValue(*varDecl);
} }
else else

19
test/libsolidity/smtCheckerTests/types/mapping_struct_assignment.sol Normal file
View File

@ -0,0 +1,19 @@
pragma experimental SMTChecker;
contract C
{
struct S {
uint x;
}
mapping (uint => S) smap;
function f(uint y, uint v) public {
if (0==1)
smap[y] = S(v);
}
}
// ----
// Warning: (140-144): Condition is always false.
// Warning: (149-156): Assertion checker does not yet implement type struct C.S storage ref
// Warning: (159-160): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning: (159-163): Assertion checker does not yet implement type struct C.S memory
// Warning: (159-163): Assertion checker does not yet implement this expression.
// Warning: (149-163): Assertion checker does not yet implement type struct C.S storage ref