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 #9070 from ethereum/smt_push

Browse Source 
[SMTChecker] Fix ICE on push for member access
This commit is contained in:
Leonardo 2020-06-02 12:57:48 +02:00 committed by GitHub
commit 22f7a9f089
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 66 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
libsolidity/formal/SMTEncoder.cpp
View File

@ -1150,6 +1150,12 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression
}
else if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(&_expr))
arrayIndexAssignment(*indexAccess, _array);
else if (dynamic_cast<MemberAccess const*>(&_expr))
m_errorReporter.warning(
9599_error,
_expr.location(),
"Assertion checker does not yet implement this expression."
);
else
solAssert(false, "");
}

27
test/libsolidity/smtCheckerTests/array_members/push_struct_member_1.sol Normal file
View File

@ -0,0 +1,27 @@
pragma experimental SMTChecker;
contract C {
struct S {
int[] b;
}
S s;
struct T {
S s;
}
T t;
function f() public {
s.b.push();
t.s.b.push();
}
}
// ----
// Warning: (72-75): Assertion checker does not yet support the type of this variable.
// Warning: (100-103): Assertion checker does not yet support the type of this variable.
// Warning: (130-133): Assertion checker does not yet support this expression.
// Warning: (130-131): Assertion checker does not yet implement type struct C.S storage ref
// Warning: (130-133): Assertion checker does not yet implement this expression.
// Warning: (144-149): Assertion checker does not yet support this expression.
// Warning: (144-147): Assertion checker does not yet implement type struct C.S storage ref
// Warning: (144-147): Assertion checker does not yet support this expression.
// Warning: (144-145): Assertion checker does not yet implement type struct C.T storage ref
// Warning: (144-149): Assertion checker does not yet implement this expression.

33
test/libsolidity/smtCheckerTests/array_members/push_struct_member_2.sol Normal file
View File

@ -0,0 +1,33 @@
pragma experimental SMTChecker;
contract C {
struct S {
int[] b;
}
S s;
struct T {
S[] s;
}
T t;
function f() public {
s.b.push();
t.s.push();
t.s[0].b.push();
}
}
// ----
// Warning: (72-75): Assertion checker does not yet support the type of this variable.
// Warning: (102-105): Assertion checker does not yet support the type of this variable.
// Warning: (132-135): Assertion checker does not yet support this expression.
// Warning: (132-133): Assertion checker does not yet implement type struct C.S storage ref
// Warning: (132-135): Assertion checker does not yet implement this expression.
// Warning: (146-149): Assertion checker does not yet support this expression.
// Warning: (146-147): Assertion checker does not yet implement type struct C.T storage ref
// Warning: (146-156): Assertion checker does not yet implement type struct C.S storage ref
// Warning: (146-149): Assertion checker does not yet implement this expression.
// Warning: (160-168): Assertion checker does not yet support this expression.
// Warning: (160-163): Assertion checker does not yet support this expression.
// Warning: (160-161): Assertion checker does not yet implement type struct C.T storage ref
// Warning: (160-166): Assertion checker does not yet implement type struct C.S storage ref
// Warning: (160-166): Assertion checker does not yet implement this expression.
// Warning: (160-168): Assertion checker does not yet implement this expression.