cerc-io/solidity
11
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

adjust old tests

Browse Source
This commit is contained in:
Leo Alt 2022-03-07 13:28:13 +01:00
parent d982e1613c
commit e7dede36d0
27 changed files with 35 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol
View File

@ -22,4 +22,4 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Info 1180: Contract invariant(s) for :C:\n!(s1.arr.length <= 0)\n!(s2.arr.length <= 0)\n(((s2.arr[0].length + ((- 1) * s1.arr[0].length)) <= 0) && ((s1.arr[0].length + ((- 1) * s2.arr[0].length)) <= 0))\n
// Info 1180: Contract invariant(s) for :C:\n!(s1.arr.length <= 0)\n!(s2.arr.length <= 0)\n(((s1.arr[0].length + ((- 1) * s2.arr[0].length)) <= 0) && ((s2.arr[0].length + ((- 1) * s1.arr[0].length)) <= 0))\n

2
test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol
View File

@ -31,4 +31,4 @@ contract C {
// Warning 6328: (349-375): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
// Warning 6328: (379-402): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
// Warning 6328: (406-432): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 7)\n!(arr.length <= 8)\n
// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 5)\n!(arr.length <= 7)\n!(arr.length <= 8)\n

1
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol
View File

@ -18,5 +18,6 @@ contract C {
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// SMTIgnoreCex: yes
// ----
// Warning 6328: (199-229): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/complex/slither/external_function.sol
View File

@ -83,6 +83,6 @@ contract InternalCall {
// Warning 2018: (1111-1173): Function state mutability can be restricted to pure
// Warning 2018: (1179-1241): Function state mutability can be restricted to pure
// Warning 2018: (1247-1309): Function state mutability can be restricted to pure
// Warning 4588: (681-716): Assertion checker does not yet implement this type of function call.
// Warning 4588: (854-886): Assertion checker does not yet implement this type of function call.
// Warning 8729: (681-716): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
// Warning 8729: (854-886): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
// Warning 5729: (1370-1375): BMC does not yet implement this type of function call.

2
test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol
View File

@ -15,4 +15,4 @@ contract C {
// Warning 2519: (106-112): This declaration shadows an existing declaration.
// Warning 2072: (106-112): Unused local variable.
// Warning 2072: (114-131): Unused local variable.
// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 0)\n
// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n((!(x <= 0) || (x' <= 0)) && ((<errorCode> <= 0) || !(x <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 0)\n

3
test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol
View File

@ -36,5 +36,6 @@ contract C {
// SMTEngine: chc
// SMTExtCalls: trusted
// ----
// Warning 6328: (256-277): CHC: Assertion violation happens here.
// Warning 1218: (256-277): CHC: Error trying to invoke SMT solver.
// Warning 6328: (256-277): CHC: Assertion violation might happen here.
// Warning 6328: (533-554): CHC: Assertion violation might happen here.

1
test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_4.sol
View File

@ -44,5 +44,4 @@ contract C {
// SMTEngine: chc
// SMTExtCalls: trusted
// ----
// Warning 1218: (641-662): CHC: Error trying to invoke SMT solver.
// Warning 6328: (641-662): CHC: Assertion violation might happen here.

2
test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol
View File

@ -13,4 +13,4 @@ contract C {
// SMTExtCalls: trusted
// SMTTargets: assert
// ----
// Warning 6328: (147-161): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()\n C.i() -- trusted external call
// Warning 6328: (147-161): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_2.sol
View File

@ -13,4 +13,4 @@ contract C {
// SMTExtCalls: trusted
// SMTTargets: assert
// ----
// Warning 6328: (151-165): CHC: Assertion violation happens here.
// Warning 6328: (151-165): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()\n C.i() -- trusted external call

2
test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol
View File

@ -11,4 +11,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (157-192): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.h() -- trusted external call
// Warning 6328: (157-192): CHC: Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_2.sol
View File

@ -1,7 +1,11 @@
contract C {
function g(uint i) public {
require(address(this).balance == 100);
// if called address is same as this, don't do anything with the value stuff
// or fix the receiving end
this.h{value: i}();
uint x = address(this).balance;
assert(x == 100); // should hold
assert(address(this).balance == 100); // should hold
assert(address(this).balance == 90); // should fail
}
@ -12,4 +16,4 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (162-197): CHC: Assertion violation happens here.
// Warning 6328: (340-375): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol
View File

@ -16,6 +16,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (206-220): CHC: Error trying to invoke SMT solver.
// Warning 6328: (206-220): CHC: Assertion violation might happen here.
// Warning 4661: (206-220): BMC: Assertion violation happens here.
// Warning 6328: (206-220): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0x0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0x0)\n D(target).e() -- untrusted external call, synthesized as:\n C.broken() -- reentrant call

4
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol
View File

@ -13,6 +13,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (117-131): CHC: Error trying to invoke SMT solver.
// Warning 6328: (117-131): CHC: Assertion violation might happen here.
// Warning 4661: (117-131): BMC: Assertion violation happens here.
// Warning 6328: (117-131): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0x0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0x0)\n D(target).e() -- untrusted external call, synthesized as:\n C.call(0x0) -- reentrant call

2
test/libsolidity/smtCheckerTests/file_level/new_operator.sol
View File

@ -14,5 +14,5 @@ contract D {
// ====
// SMTEngine: all
// ----
// Warning 4588: (78-85): Assertion checker does not yet implement this type of function call.
// Warning 8729: (78-85): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
// Warning 6328: (133-152): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nD.constructor()\nD.f()\n test() -- internal call\n (new C()).x() -- untrusted external call

2
test/libsolidity/smtCheckerTests/functions/functions_external_2.sol
View File

@ -25,4 +25,4 @@ contract C
// SMTIgnoreOS: macos
// ----
// Warning 6328: (234-253): CHC: Assertion violation happens here.
// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 1)\n((!((map[1] + ((- 1) * map[0])) <= 0) || ((map'[1] + ((- 1) * map'[0])) <= 0)) && !(<errorCode> = 2) && (!((map[1] + ((- 1) * map[0])) >= 0) || ((map'[0] + ((- 1) * map'[1])) <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 2 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 3 -> Assertion failed at assert(map[0] == 0)\n
// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 1)\n((!((map[1] + ((- 1) * map[0])) >= 0) || ((map'[0] + ((- 1) * map'[1])) <= 0)) && !(<errorCode> = 2) && (!((map[1] + ((- 1) * map[0])) <= 0) || ((map'[1] + ((- 1) * map'[0])) <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 2 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 3 -> Assertion failed at assert(map[0] == 0)\n

2
test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol
View File

@ -27,4 +27,4 @@ contract C is A {
// ----
// Warning 6328: (199-214): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nA.constructor()\nState: x = 2\nA.i()
// Warning 6328: (387-401): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\n\nTransaction trace:\nC.constructor()\nState: x = 10\nC.i()
// Info 1180: Contract invariant(s) for :A:\n(!(x <= 1) && !(x >= 3))\nContract invariant(s) for :C:\n(!(x >= 11) && !(x <= 9))\n
// Info 1180: Contract invariant(s) for :A:\n(!(x <= 1) && !(x >= 3))\nContract invariant(s) for :C:\n(!(x <= 9) && !(x >= 11))\n

2
test/libsolidity/smtCheckerTests/imports/ExtCall.sol
View File

@ -39,4 +39,4 @@ contract ExtCallTest {
// SMTIgnoreCex: yes
// ----
// Warning 6328: (ExtCall.sol:362-381): CHC: Assertion violation happens here.
// Warning 4588: (ExtCall.t.sol:110-123): Assertion checker does not yet implement this type of function call.
// Warning 8729: (ExtCall.t.sol:110-123): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.

2
test/libsolidity/smtCheckerTests/modifiers/modifier_same_local_variables.sol
View File

@ -12,4 +12,4 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (88-102): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\nx = 2\n\nTransaction trace:\nC.constructor()\nC.f(0)
// Warning 6328: (88-102): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\nx = 2\n\nTransaction trace:\nC.constructor()\nC.f(3)

2
test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol
View File

@ -20,4 +20,4 @@ contract C
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (262-284): CHC: Assertion violation happens here.\nCounterexample:\narray = [200, 0]\nx = 0\np = 0\n\nTransaction trace:\nC.constructor()\nState: array = [0, 0]\nC.f(0, 0)
// Warning 6328: (262-284): CHC: Assertion violation happens here.\nCounterexample:\narray = [299, 0]\nx = 99\np = 0\n\nTransaction trace:\nC.constructor()\nState: array = [0, 0]\nC.f(99, 0)

1
test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol
View File

@ -12,7 +12,6 @@ contract C {
// SMTIgnoreOS: macos
// ----
// Warning 6368: (76-81): CHC: Out of bounds access might happen here.
// Warning 6368: (76-84): CHC: Out of bounds access might happen here.
// Warning 6368: (119-124): CHC: Out of bounds access might happen here.
// Warning 6368: (119-127): CHC: Out of bounds access might happen here.
// Warning 6368: (149-154): CHC: Out of bounds access might happen here.

4
test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol
View File

@ -25,4 +25,6 @@ contract C {
// SMTIgnoreCex: yes
// ----
// Warning 2072: (249-255): Unused local variable.
// Warning 6328: (271-295): CHC: Assertion violation happens here.
// Warning 1218: (271-295): CHC: Error trying to invoke SMT solver.
// Warning 6328: (271-295): CHC: Assertion violation might happen here.
// Warning 4661: (271-295): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol
View File

@ -25,4 +25,4 @@ contract C {
// SMTIgnoreOS: macos
// ----
// Warning 2072: (255-261): Unused local variable.
// Info 1180: Reentrancy property(ies) for :C:\n((!(x' >= 3) || (a' = a)) && (<errorCode> <= 0) && (!(x' <= 0) || !(x >= 2)) && (!(x <= 2) || !(x' >= 3)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 2 || x == 1)\n
// Info 1180: Reentrancy property(ies) for :C:\n((!(x <= 2) || !(x' >= 3)) && (<errorCode> <= 0) && (!(x' <= 0) || !(x >= 2)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 2 || x == 1)\n

2
test/libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol
View File

@ -21,4 +21,4 @@ contract C {
// SMTEngine: chc
// SMTIgnoreOS: macos
// ----
// Warning 6328: (343-377): CHC: Assertion violation happens here.\nCounterexample:\ngas = 0, origin = 0x52f7\n\nTransaction trace:\nC.constructor()\nState: gas = 0, origin = 0x0\nC.f(){ tx.gasprice: 0, tx.origin: 0x52f7 }\n C.g() -- internal call
// Warning 6328: (343-377): CHC: Assertion violation happens here.\nCounterexample:\ngas = 0, origin = 0x0\n\nTransaction trace:\nC.constructor()\nState: gas = 0, origin = 0x0\nC.f(){ tx.gasprice: 0, tx.origin: 0x0 }\n C.g() -- internal call

1
test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol
View File

@ -11,6 +11,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// SMTIgnoreOS: macos
// ----
// Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 9726\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 2070 }\n _i.f() -- untrusted external call, synthesized as:\n C.g(0){ msg.value: 0 } -- reentrant call\n _i.f() -- untrusted external call

4
test/libsolidity/smtCheckerTests/try_catch/try_new.sol
View File

@ -28,5 +28,5 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 4588: (231-245): Assertion checker does not yet implement this type of function call.
// Warning 4588: (492-507): Assertion checker does not yet implement this type of function call.
// Warning 8729: (231-245): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
// Warning 8729: (492-507): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.

2
test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol
View File

@ -22,4 +22,4 @@ contract C {
// SMTIgnoreOS: macos
// ----
// Warning 6328: (280-300): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Info 1180: Contract invariant(s) for :C:\n!(m[0].length <= 1)\n(!(m[0][1] >= 43) && !(m[0][1] <= 41))\n
// Info 1180: Contract invariant(s) for :C:\n!(m[0].length <= 1)\n(!(m[0][1] <= 41) && !(m[0][1] >= 43))\n

3
test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol
View File

@ -32,5 +32,6 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6368: (374-381): CHC: Out of bounds access might happen here.
// Warning 6368: (456-462): CHC: Out of bounds access happens here.
// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 4)\n!(a[2].length <= 2)\n
// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 4)\n