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

[SMTChecker] Reset reference variables on assignment to a variable of reference type

Browse Source
This commit is contained in:
Martin Blicha 2021-03-12 19:33:45 +01:00
parent ccd9de137a
commit 6aa6c5f5f9
3 changed files with 27 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libsolidity/formal/SMTEncoder.cpp
View File

@ -2034,7 +2034,11 @@ void SMTEncoder::assignment(
m_context.newValue(*varDecl); m_context.newValue(*varDecl);
} }
else if (auto varDecl = identifierToVariable(*left)) else if (auto varDecl = identifierToVariable(*left))
{
if (varDecl->hasReferenceOrMappingType())
resetReferences(*varDecl);
assignment(*varDecl, _right); assignment(*varDecl, _right);
}
else if ( else if (
dynamic_cast<IndexAccess const*>(left) || dynamic_cast<IndexAccess const*>(left) ||
dynamic_cast<MemberAccess const*>(left) dynamic_cast<MemberAccess const*>(left)

21
test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array_3.sol Normal file
View File

@ -0,0 +1,21 @@
pragma experimental SMTChecker;
contract A {
int[] a;
function f() public {
require(a.length == 1 && a[0] == 1);
int[] storage u = a;
assert(u[0] == 1); // should hold
int[] memory b = new int[](2);
a = b;
assert(u[0] == 1); // should fail
A.a = b;
assert(u[0] == 1); // should fail
}
function push_v(int x) public {
a.push(x);
}
}
// ----
// Warning 6328: (220-237): CHC: Assertion violation happens here.
// Warning 6328: (267-284): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/types/bytes_2.sol
View File

@ -7,3 +7,5 @@ contract C
assert(b1[1] == b2[1]); assert(b1[1] == b2[1]);
} }
} }
// ----
// Warning 6328: (119-141): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(b1, b2)