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

Update tests due to nondeterminism

Browse Source
This commit is contained in:
Leo Alt 2021-07-16 15:44:36 +02:00
parent 5decccaf3a
commit e46abd0ca1
15 changed files with 48 additions and 48 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice_2.sol
View File

@ -28,6 +28,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 2072: (643-658): Unused local variable.
// Warning 6328: (298-328): CHC: Assertion violation happens here.

16
test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
View File

@ -7,12 +7,14 @@ contract C {
function s(bytes memory b0, bytes memory b1) public pure {
bytes32 s0 = sha256(b0);
bytes32 s1 = sha256(b1);
assert(s0 == s1);
// Disabled because of Spacer nondeterminism.
//assert(s0 == s1);
}
function r(bytes memory b0, bytes memory b1) public pure {
bytes32 r0 = ripemd160(b0);
bytes32 r1 = ripemd160(b1);
assert(r0 == r1);
// Disabled because of Spacer nondeterminism.
//assert(r0 == r1);
}
function e(bytes32 h0, uint8 v0, bytes32 r0, bytes32 s0, bytes32 h1, uint8 v1, bytes32 r1, bytes32 s1) public pure {
address a0 = ecrecover(h0, v0, r0, s0);
@ -25,8 +27,10 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 2072: (556-566): Unused local variable.
// Warning 2072: (598-608): Unused local variable.
// Warning 2072: (218-228): Unused local variable.
// Warning 2072: (245-255): Unused local variable.
// Warning 2072: (405-415): Unused local variable.
// Warning 2072: (435-445): Unused local variable.
// Warning 2072: (656-666): Unused local variable.
// Warning 2072: (698-708): Unused local variable.
// Warning 6328: (135-151): CHC: Assertion violation happens here.
// Warning 6328: (272-288): CHC: Assertion violation happens here.
// Warning 6328: (415-431): CHC: Assertion violation happens here.

5
test/libsolidity/smtCheckerTests/file_level/free_function_1.sol
View File

@ -10,6 +10,7 @@ function fun(uint[] calldata _x, uint[] storage _y) view returns (uint, uint[]
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 4984: (168-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\ndata = []\nx = 1\n = 0\n = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(1, input)\n fun(_x, []) -- internal call
// Warning 6368: (289-294): CHC: Out of bounds access happens here.\nCounterexample:\ndata = []\nx = 0\ninput = [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 5, 5, 5, 16, 5, 5, 20, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 5, 5, 5, 16, 5, 5, 20, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5])\n fun([5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 5, 5, 5, 16, 5, 5, 20, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5], []) -- internal call
// Warning 4984: (168-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6368: (289-294): CHC: Out of bounds access happens here.

19
test/libsolidity/smtCheckerTests/file_level/recursion.sol
View File

@ -13,29 +13,16 @@ contract C {
}
function f() public pure {
// All of these should hold but the SMTChecker can't prove them.
// Disabled because of Spacer nondet
/*
assert(g(0, 0) == 1);
assert(g(0, 1) == 0);
assert(g(1, 0) == 1);
assert(g(2, 3) == 8);
assert(g(3, 10) == 59049);
*/
}
}
// ====
// SMTEngine: all
// ----
// Warning 4281: (118-130): CHC: Division by zero might happen here.
// Warning 4984: (134-148): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (176-189): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (430-450): CHC: Assertion violation might happen here.
// Warning 6328: (454-474): CHC: Assertion violation might happen here.
// Warning 6328: (478-498): CHC: Assertion violation might happen here.
// Warning 6328: (502-527): CHC: Assertion violation might happen here.
// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (176-189): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4661: (454-474): BMC: Assertion violation happens here.
// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (176-189): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4661: (478-498): BMC: Assertion violation happens here.
// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4661: (502-527): BMC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol
View File

@ -12,5 +12,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (112-126): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 11\n\nTransaction trace:\nC.constructor()\nState: x = 10\nC.f(11)
// Warning 6328: (112-126): CHC: Assertion violation happens here.

7
test/libsolidity/smtCheckerTests/inheritance/fallback_receive.sol
View File

@ -20,7 +20,8 @@ contract B is A {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (81-95): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.fallback()
// Warning 6328: (130-144): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.g()
// Warning 6328: (256-270): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 0\n\nTransaction trace:\nB.constructor()\nState: y = 0, x = 0\nB.receive(){ value: 10450 }
// Warning 6328: (81-95): CHC: Assertion violation happens here.
// Warning 6328: (130-144): CHC: Assertion violation happens here.
// Warning 6328: (256-270): CHC: Assertion violation happens here.

7
test/libsolidity/smtCheckerTests/inheritance/receive.sol
View File

@ -20,7 +20,8 @@ contract B is A {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (95-109): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.receive()
// Warning 6328: (144-158): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.g()
// Warning 6328: (267-281): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 0\n\nTransaction trace:\nB.constructor()\nState: y = 0, x = 0\nB.receive()
// Warning 6328: (95-109): CHC: Assertion violation happens here.
// Warning 6328: (144-158): CHC: Assertion violation happens here.
// Warning 6328: (267-281): CHC: Assertion violation happens here.

5
test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_access_inside_function.sol
View File

@ -17,8 +17,9 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 7737: (83-149): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
// Warning 6328: (152-167): CHC: Assertion violation happens here.\nCounterexample:\nz = 0\ni = 32\n\nTransaction trace:\nC.constructor()\nState: z = 0\nC.f()
// Warning 6328: (186-200): CHC: Assertion violation happens here.\nCounterexample:\nz = 0\ni = 32\n\nTransaction trace:\nC.constructor()\nState: z = 0\nC.f()
// Warning 6328: (152-167): CHC: Assertion violation happens here.
// Warning 6328: (186-200): CHC: Assertion violation happens here.
// Warning 7737: (83-149): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

9
test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol
View File

@ -7,6 +7,8 @@ contract C {
}
function pow(uint base, uint exponent) internal pure returns (uint) {
// Disabled because of Spacer nondet
/*
if (base == 0) {
return 0;
}
@ -28,14 +30,9 @@ contract C {
}
}
return base * y;
*/
}
}
// ====
// SMTEngine: chc
// ----
// Warning 4281: (435-447): CHC: Division by zero might happen here.
// Warning 4984: (467-478): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4281: (495-507): CHC: Division by zero might happen here.
// Warning 4984: (529-537): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (550-561): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (616-624): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

5
test/libsolidity/smtCheckerTests/special/blockhash.sol
View File

@ -9,6 +9,7 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (52-76): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 8365 }
// Warning 6328: (80-104): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 5853 }
// Warning 6328: (52-76): CHC: Assertion violation happens here.
// Warning 6328: (80-104): CHC: Assertion violation happens here.

5
test/libsolidity/smtCheckerTests/special/msg_data.sol
View File

@ -21,6 +21,7 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (120-147): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(){ value: 30612 }
// Warning 6328: (467-494): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g(){ value: 11797 }
// Warning 6328: (120-147): CHC: Assertion violation happens here.
// Warning 6328: (467-494): CHC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol
View File

@ -19,5 +19,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (306-320): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\nsuccess = false\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (306-320): CHC: Assertion violation happens here.

5
test/libsolidity/smtCheckerTests/types/string_literal_comparison_2.sol
View File

@ -9,6 +9,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (114-133): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 0\ny = 0\nz = 0\n\nTransaction trace:\nC.constructor()\nC.f(0)
// Warning 6328: (137-157): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538830022687173130149211684818290356179572910782152375644828738034597888\ny = 52647538830022687173130149211684818290356179572910782152375644828738034597888\nz = 52647538830022687173130149211684818290356179572910782152375644828738034597888\n\nTransaction trace:\nC.constructor()\nC.f(52647538830022687173130149211684818290356179572910782152375644828738034597888)
// Warning 6328: (114-133): CHC: Assertion violation happens here.
// Warning 6328: (137-157): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol
View File

@ -36,5 +36,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (804-842): CHC: Assertion violation happens here.

5
test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol
View File

@ -40,9 +40,10 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (148-165): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 2, t: {y: 0, a: []}, a: [], ts: []}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, t: {y: 0, a: []}, a: [], ts: []}\nC.f()
// Warning 6328: (148-165): CHC: Assertion violation happens here.
// Warning 6328: (183-202): CHC: Assertion violation happens here.
// Warning 6328: (266-286): CHC: Assertion violation happens here.
// Warning 6328: (404-427): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 2, t: {y: 3, a: []}, a: [0, 0, 4], ts: [{y: 0, a: []}, {y: 0, a: []}, {y: 0, a: []}, {y: 5, a: []}, {y: 0, a: []}, {y: 0, a: []}]}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, t: {y: 0, a: []}, a: [], ts: []}\nC.f()
// Warning 6328: (404-427): CHC: Assertion violation happens here.
// Warning 6328: (578-604): CHC: Assertion violation happens here.