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 for osx nondeterminism

Browse Source
This commit is contained in:
Leo Alt 2022-05-04 16:29:50 +02:00
parent 4fd7de36f1
commit cba3d18f66
14 changed files with 54 additions and 52 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
test/cmdlineTests/model_checker_invariants_all/err
View File

@ -5,10 +5,8 @@ Warning: Return value of low-level calls not used.
| ^^^^^^^^^^^
Info: Contract invariant(s) for model_checker_invariants_all/input.sol:test:
((x <= 0) || true || true)
((x <= 0) || true)
Reentrancy property(ies) for model_checker_invariants_all/input.sol:test:
(true || true || ((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0))) || true)
(true || true || ((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)
<errorCode> = 3 -> Assertion failed at assert(x < 10)
<errorCode> = 1 -> Assertion failed at assert(x == 0)

5
test/cmdlineTests/model_checker_invariants_all/input.sol
View File

@ -4,9 +4,6 @@ contract test {
uint x;
function f(address _a) public {
_a.call("");
assert(x < 10);
}
function g() public view {
assert(x < 10);
assert(x == 0);
}
}

8
test/cmdlineTests/model_checker_invariants_contract_reentrancy/err
View File

@ -5,10 +5,8 @@ Warning: Return value of low-level calls not used.
| ^^^^^^^^^^^
Info: Contract invariant(s) for model_checker_invariants_contract_reentrancy/input.sol:test:
((x <= 0) || true || true)
((x <= 0) || true)
Reentrancy property(ies) for model_checker_invariants_contract_reentrancy/input.sol:test:
(true || true || ((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0))) || true)
(true || true || ((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)
<errorCode> = 3 -> Assertion failed at assert(x < 10)
<errorCode> = 1 -> Assertion failed at assert(x == 0)

5
test/cmdlineTests/model_checker_invariants_contract_reentrancy/input.sol
View File

@ -4,9 +4,6 @@ contract test {
uint x;
function f(address _a) public {
_a.call("");
assert(x < 10);
}
function g() public view {
assert(x < 10);
assert(x == 0);
}
}

5
test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/input.json
View File

@ -8,10 +8,7 @@
uint x;
function f(address _a) public {
_a.call(\"\");
assert(x < 10);
}
function g() public view {
assert(x < 10);
assert(x == 10);
}
}"
}

40
test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json
View File

@ -4,22 +4,28 @@
7 | \t\t\t\t\t\t_a.call(\"\");
| \t\t\t\t\t\t^^^^^^^^^^^
","message":"Return value of low-level calls not used.","severity":"warning","sourceLocation":{"end":143,"file":"A","start":132},"type":"Warning"},{"component":"general","errorCode":"1180","formattedMessage":"Info: Contract invariant(s) for A:test:
((x <= 0) || true || true)
Reentrancy property(ies) for A:test:
(true || true || ((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0))) || true)
(true || true || ((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)
<errorCode> = 3 -> Assertion failed at assert(x < 10)
","message":"Return value of low-level calls not used.","severity":"warning","sourceLocation":{"end":143,"file":"A","start":132},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
Counterexample:
x = 0
_a = 0x0
Transaction trace:
test.constructor()
State: x = 0
test.f(0x0)
_a.call(\"\") -- untrusted external call
--> A:8:7:
|
8 | \t\t\t\t\t\tassert(x == 10);
| \t\t\t\t\t\t^^^^^^^^^^^^^^^
","message":"Contract invariant(s) for A:test:
((x <= 0) || true || true)
Reentrancy property(ies) for A:test:
(true || true || ((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0))) || true)
(true || true || ((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)
<errorCode> = 3 -> Assertion failed at assert(x < 10)
","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}}
","message":"CHC: Assertion violation happens here.
Counterexample:
x = 0
_a = 0x0
Transaction trace:
test.constructor()
State: x = 0
test.f(0x0)
_a.call(\"\") -- untrusted external call","severity":"warning","sourceLocation":{"end":166,"file":"A","start":151},"type":"Warning"}],"sources":{"A":{"id":0}}}

16
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol
View File

@ -3,7 +3,8 @@ contract C {
require(a == b);
bytes memory b1 = abi.encodeWithSelector(sel, a, a, a, a);
bytes memory b2 = abi.encodeWithSelector(sel, b, a, b, a);
assert(keccak256(b1) == keccak256(b2));
// Disabled because of OSX nondeterminism
//assert(keccak256(b1) == keccak256(b2));
bytes memory b3 = abi.encodeWithSelector(0xcafecafe, a, a, a, a);
assert(keccak256(b1) == keccak256(b3)); // should fail
@ -13,9 +14,10 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (333-371): CHC: Error trying to invoke SMT solver.
// Warning 1218: (390-428): CHC: Error trying to invoke SMT solver.
// Warning 6328: (333-371): CHC: Assertion violation might happen here.
// Warning 6328: (390-428): CHC: Assertion violation might happen here.
// Warning 4661: (333-371): BMC: Assertion violation happens here.
// Warning 4661: (390-428): BMC: Assertion violation happens here.
// Warning 2072: (161-176): Unused local variable.
// Warning 1218: (379-417): CHC: Error trying to invoke SMT solver.
// Warning 1218: (436-474): CHC: Error trying to invoke SMT solver.
// Warning 6328: (379-417): CHC: Assertion violation might happen here.
// Warning 6328: (436-474): CHC: Assertion violation might happen here.
// Warning 4661: (379-417): BMC: Assertion violation happens here.
// Warning 4661: (436-474): BMC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol
View File

@ -18,5 +18,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (265-310): CHC: Assertion violation happens here.\nCounterexample:\nb = [0x01]\none = 0x01\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g()
// Warning 6328: (265-310): CHC: Assertion violation happens here.

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

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

3
test/libsolidity/smtCheckerTests/functions/getters/array_1.sol
View File

@ -14,6 +14,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (187-201): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0, 0, 0]\ny = 0\n\nTransaction trace:\nC.constructor()\nState: a = [0, 0, 0, 0]\nC.f()
// Warning 6328: (187-201): CHC: Assertion violation happens here.
// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 2)\n

3
test/libsolidity/smtCheckerTests/overflow/unsigned_mul_overflow.sol
View File

@ -5,5 +5,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 4984: (80-85): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 57896044618658097711785492504343953926634992332820282019728792003956564819968\ny = 2\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(57896044618658097711785492504343953926634992332820282019728792003956564819968, 2)
// Warning 4984: (80-85): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

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

@ -19,5 +19,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (342-362): CHC: Assertion violation happens here.\nCounterexample:\n\nchoice = 3\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (342-362): CHC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol
View File

@ -25,5 +25,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (307-327): CHC: Assertion violation happens here.\nCounterexample:\nt = {x: 10, s: {innerM, sum: 21239}}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: t = {x: 10, s: {innerM, sum: 21239}}\nC.g()
// Warning 6328: (307-327): CHC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/unchecked/checked_called_by_unchecked.sol
View File

@ -9,5 +9,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 65535) happens here.\nCounterexample:\n\na = 65535\nb = 1\n = 0\n\nTransaction trace:\nC.constructor()\nC.add(65535, 1)
// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 65535) happens here.