Merge pull request #11097 from blishko/smt-reset-reference-variables

[SMTChecker] Reset reference variables on assignment to a variable of reference type
This commit is contained in:
Leonardo 2021-03-15 12:06:37 +01:00 committed by GitHub
commit 2c00939ad8
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 27 additions and 0 deletions

View File

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

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.

View File

@ -7,3 +7,5 @@ contract C
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)