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

Adjust tests for nondeterminism

Browse Source
This commit is contained in:
Leo Alt 2021-11-23 18:54:44 +01:00
parent ff5c842d67
commit 0c34d9df88
5 changed files with 11 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol
View File

@ -13,7 +13,8 @@ contract C {
// ==== // ====
// SMTEngine: all // SMTEngine: all
// SMTIgnoreOS: macos // SMTIgnoreOS: macos
// SMTIgnoreCex: yes
// ---- // ----
// Warning 6368: (188-192): CHC: Out of bounds access happens here.\nCounterexample:\na = []\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f() // Warning 6368: (188-192): CHC: Out of bounds access happens here.
// Warning 6368: (188-195): CHC: Out of bounds access happens here.\nCounterexample:\n\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f() // Warning 6368: (188-195): CHC: Out of bounds access happens here.
// Warning 6328: (181-202): CHC: Assertion violation happens here.\nCounterexample:\n\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f() // Warning 6328: (181-202): CHC: Assertion violation happens here.

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

@ -7,7 +7,7 @@ contract C {
} }
// ==== // ====
// SMTEngine: all // SMTEngine: all
// SMTIgnoreInv: yes
// ---- // ----
// Warning 2072: (57-63): Unused local variable. // Warning 2072: (57-63): Unused local variable.
// Warning 2072: (65-82): Unused local variable. // Warning 2072: (65-82): Unused local variable.
// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n((!(x <= 0) || (<errorCode> <= 0)) && (!(x <= 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_single_inc.sol
View File

@ -22,5 +22,6 @@ contract C {
} }
// ==== // ====
// SMTEngine: all // SMTEngine: all
// SMTIgnoreCex: yes
// ---- // ----
// Warning 6328: (223-240): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, y = 1, d = 0\noldX = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0, d = 0\nC.inc()\nState: x = 0, y = 1, d = 0\nC.f()\n d.d() -- untrusted external call, synthesized as:\n C.inc() -- reentrant call // Warning 6328: (223-240): CHC: Assertion violation happens here.

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

@ -17,5 +17,4 @@ contract C
// ==== // ====
// SMTEngine: all // SMTEngine: all
// SMTIgnoreOS: macos // SMTIgnoreOS: macos
// ---- // SMTIgnoreInv: yes
// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n!(<errorCode> = 1)\n((!(<errorCode> >= 2) || !(x <= 0)) && (!(x <= 0) || (x' <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == y)\n<errorCode> = 2 -> Assertion failed at assert(x == y)\n

9
test/libsolidity/smtCheckerTests/try_catch/try_4.sol
View File

@ -14,7 +14,7 @@ contract C {
function f() public { function f() public {
x = 0; x = 0;
try d.d() { try d.d() {
assert(x == 0); // should fail, x can be anything here //assert(x == 0); // should fail, x can be anything here
} catch { } catch {
assert(x == 0); // should hold, all changes to x has been reverted assert(x == 0); // should hold, all changes to x has been reverted
assert(x == 1); // should fail assert(x == 1); // should fail
@ -25,8 +25,5 @@ contract C {
// SMTEngine: all // SMTEngine: all
// SMTIgnoreCex: yes // SMTIgnoreCex: yes
// ---- // ----
// Warning 1218: (178-192): CHC: Error trying to invoke SMT solver. // Warning 6328: (320-334): CHC: Assertion violation happens here.
// Warning 6328: (178-192): CHC: Assertion violation might happen here. // Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 1)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 0)\n<errorCode> = 2 -> Assertion failed at assert(x == 1)\n
// Warning 6328: (318-332): CHC: Assertion violation happens here.
// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 2)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 0)\n<errorCode> = 2 -> Assertion failed at assert(x == 0)\n<errorCode> = 3 -> Assertion failed at assert(x == 1)\n
// Warning 4661: (178-192): BMC: Assertion violation happens here.