From 1ab6ad79d8302557f83764ffca2e4d22990eb036 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 18 May 2020 16:33:27 +0200 Subject: [PATCH] Update test expectation --- .../array_members/pop_2d_unsafe.sol | 2 ++ .../array_members/pop_constructor_unsafe.sol | 2 ++ .../array_members/pop_loop_unsafe.sol | 2 ++ .../array_members/push_2d_arg_1_unsafe.sol | 3 +++ .../push_storage_ref_safe_aliasing.sol | 16 ++++++++++++++++ .../push_storage_ref_unsafe_aliasing.sol | 15 +++++++++++++++ .../array_members/push_zero_2d_unsafe.sol | 2 ++ .../array_members/push_zero_unsafe.sol | 2 ++ 8 files changed, 44 insertions(+) create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol index 1b7713089..1161ab92e 100644 --- a/test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol +++ b/test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol @@ -8,3 +8,5 @@ contract C { a[1].pop(); } } +// ---- +// Warning: (111-121): Empty array "pop" detected here. diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol index f94bdcd68..a86d1a3f3 100644 --- a/test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol +++ b/test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol @@ -6,3 +6,5 @@ contract C { a.pop(); } } +// ---- +// Warning: (83-90): Empty array "pop" detected here. diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol index 2218c6665..5d4241984 100644 --- a/test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol +++ b/test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol @@ -10,3 +10,5 @@ contract C { a.pop(); } } +// ---- +// Warning: (150-157): Empty array "pop" detected here. diff --git a/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol index 23b8f6f00..d5bd19bb1 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol @@ -9,3 +9,6 @@ contract C { assert(a[0][a[0].length - 1] == y); } } +// ---- +// Warning: (162-177): Underflow (resulting value less than 0) happens here +// Warning: (150-184): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol new file mode 100644 index 000000000..8ad5cdcad --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C { + uint[][] a; + function f() public { + a.push(); + uint[] storage b = a[0]; + b.push(8); + assert(b[b.length - 1] == 8); + // Safe but fails due to aliasing. + assert(a[0][a[0].length - 1] == 8); + } +} +// ---- +// Warning: (217-232): Underflow (resulting value less than 0) happens here +// Warning: (205-239): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol new file mode 100644 index 000000000..f54fc8d83 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; + +contract C { + uint[][] a; + function f() public { + a.push(); + a[0].push(); + a[0][0] = 16; + uint[] storage b = a[0]; + b[0] = 32; + assert(a[0][0] == 16); + } +} +// ---- +// Warning: (167-188): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol index 91fcd90b1..9b9516ccd 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol @@ -8,3 +8,5 @@ contract C { assert(a[a.length - 1][0] == 100); } } +// ---- +// Warning: (111-144): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol index b99f42fa4..966b4e1bd 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol @@ -7,3 +7,5 @@ contract C { assert(a[a.length - 1] == 100); } } +// ---- +// Warning: (94-124): Assertion violation happens here