diff --git a/test/cmdlineTests/model_checker_invariants_all/err b/test/cmdlineTests/model_checker_invariants_all/err index 66a76b3c8..65228e880 100644 --- a/test/cmdlineTests/model_checker_invariants_all/err +++ b/test/cmdlineTests/model_checker_invariants_all/err @@ -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) || !( >= 3)) && (!(x <= 0) || (x' <= 0))) || true) -(true || true || ((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) || true) +(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) || true) = 0 -> no errors - = 1 -> Assertion failed at assert(x < 10) - = 3 -> Assertion failed at assert(x < 10) + = 1 -> Assertion failed at assert(x == 0) diff --git a/test/cmdlineTests/model_checker_invariants_all/input.sol b/test/cmdlineTests/model_checker_invariants_all/input.sol index f8601cf4f..8b90cb3c1 100644 --- a/test/cmdlineTests/model_checker_invariants_all/input.sol +++ b/test/cmdlineTests/model_checker_invariants_all/input.sol @@ -4,9 +4,6 @@ contract test { uint x; function f(address _a) public { _a.call(""); - assert(x < 10); + assert(x == 0); } - function g() public view { - assert(x < 10); - } } \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err index 694f512cd..855521836 100644 --- a/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err +++ b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err @@ -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) || !( >= 3)) && (!(x <= 0) || (x' <= 0))) || true) -(true || true || ((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) || true) +(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) || true) = 0 -> no errors - = 1 -> Assertion failed at assert(x < 10) - = 3 -> Assertion failed at assert(x < 10) + = 1 -> Assertion failed at assert(x == 0) diff --git a/test/cmdlineTests/model_checker_invariants_contract_reentrancy/input.sol b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/input.sol index f8601cf4f..8b90cb3c1 100644 --- a/test/cmdlineTests/model_checker_invariants_contract_reentrancy/input.sol +++ b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/input.sol @@ -4,9 +4,6 @@ contract test { uint x; function f(address _a) public { _a.call(""); - assert(x < 10); + assert(x == 0); } - function g() public view { - assert(x < 10); - } } \ No newline at end of file diff --git a/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/input.json b/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/input.json index 56139e6a5..38f658653 100644 --- a/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/input.json +++ b/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/input.json @@ -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); } }" } diff --git a/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json b/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json index d560ff288..64d63c46c 100644 --- a/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json +++ b/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json @@ -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) || !( >= 3)) && (!(x <= 0) || (x' <= 0))) || true) -(true || true || ((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) || true) - = 0 -> no errors - = 1 -> Assertion failed at assert(x < 10) - = 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) || !( >= 3)) && (!(x <= 0) || (x' <= 0))) || true) -(true || true || ((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) || true) - = 0 -> no errors - = 1 -> Assertion failed at assert(x < 10) - = 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}}} diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol index ca1b6b40a..f60d5f52b 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol index fd0229d78..31eca9e92 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes_2d.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes_2d.sol index 7151d9304..fcceeebfd 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes_2d.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes_2d.sol @@ -22,5 +22,6 @@ contract C { } // ==== // SMTEngine: all +// SMTIgnoreCex: yes // ---- // Warning 6328: (435-508): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol index 421c4fd4f..d44d15f28 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/overflow/unsigned_mul_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/unsigned_mul_overflow.sol index 0a6d85a7e..e809e041c 100644 --- a/test/libsolidity/smtCheckerTests/overflow/unsigned_mul_overflow.sol +++ b/test/libsolidity/smtCheckerTests/overflow/unsigned_mul_overflow.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_nested_2.sol b/test/libsolidity/smtCheckerTests/try_catch/try_nested_2.sol index 98a19731b..5c15fb54f 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_nested_2.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_nested_2.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol index 8779cd095..f9ae95e7c 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/unchecked/checked_called_by_unchecked.sol b/test/libsolidity/smtCheckerTests/unchecked/checked_called_by_unchecked.sol index d3589fed5..9d8df15eb 100644 --- a/test/libsolidity/smtCheckerTests/unchecked/checked_called_by_unchecked.sol +++ b/test/libsolidity/smtCheckerTests/unchecked/checked_called_by_unchecked.sol @@ -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.