From 9199718ec0aa1210094ceb9ca587fe49fba70518 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Fri, 14 Dec 2018 12:21:43 +0100 Subject: Clear all mapping knowledge after array variable assignment --- test/libsolidity/smtCheckerTests/types/mapping_aliasing_1.sol | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'test') diff --git a/test/libsolidity/smtCheckerTests/types/mapping_aliasing_1.sol b/test/libsolidity/smtCheckerTests/types/mapping_aliasing_1.sol index 1c7e8b8a..39d096f5 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_aliasing_1.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_aliasing_1.sol @@ -7,9 +7,12 @@ contract C function f() public { require(a[1] == b[1]); + a[1] = 2; mapping (uint => uint) storage c = a; - c[1] = 2; + assert(c[1] == 2); // False negative! Needs aliasing. assert(a[1] == b[1]); } } +// ---- +// Warning: (261-281): Assertion violation happens here -- cgit v1.2.3