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

Update docker images and tests

Browse Source
This commit is contained in:
Leo Alt
2022-08-30 11:51:59 +02:00
parent fa5ea38ab3
commit 16c0838f75
36 changed files with 86 additions and 65 deletions
Download Patch File Download Diff File Expand all files Collapse all files
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_hash.sol
+2 -3
View File
@@ -11,7 +11,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 1218: (281-319): CHC: Error trying to invoke SMT solver.
// Warning 6328: (281-319): CHC: Assertion violation might happen here.
// Warning 4661: (281-319): BMC: Assertion violation happens here.
// Warning 6328: (281-319): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nb = 0\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedHash(0, 0)
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol
+3 -6
View File
@@ -13,11 +13,8 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// 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.
// Warning 6328: (379-417): CHC: Assertion violation happens here.
// Warning 6328: (436-474): CHC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol
+1
View File
@@ -9,5 +9,6 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (294-324): CHC: Error trying to invoke SMT solver.
// Warning 6328: (294-324): CHC: Assertion violation might happen here.
// Warning 7812: (294-324): BMC: Assertion violation might happen here.
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol
+1 -3
View File
@@ -13,7 +13,5 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (394-432): CHC: Error trying to invoke SMT solver.
// Warning 6328: (337-375): CHC: Assertion violation happens here.
// Warning 6328: (394-432): CHC: Assertion violation might happen here.
// Warning 4661: (394-432): BMC: Assertion violation happens here.
// Warning 6328: (394-432): CHC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_simple.sol
+1 -1
View File
@@ -25,7 +25,7 @@ contract C {
// ----
// Warning 5667: (107-122): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 1218: (824-854): CHC: Error trying to invoke SMT solver.
// Warning 6328: (543-573): CHC: Assertion violation happens here.
// Warning 6328: (543-573): CHC: Assertion violation happens here.\nCounterexample:\n\nt = false\nx = 0\ny = 0\nz = 0\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSimple(sig, false, 0, 0, 0, a, b)
// Warning 6328: (664-694): CHC: Assertion violation happens here.
// Warning 6328: (713-743): CHC: Assertion violation happens here.
// Warning 6328: (824-854): CHC: Assertion violation might happen here.
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_bytes.sol
+2 -1
View File
@@ -12,5 +12,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (203-244): CHC: Assertion violation happens here.
// Warning 6328: (203-244): CHC: Assertion violation happens here.\nCounterexample:\nb = [0x0, 0x0]\nlength = 2\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f()
test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol
+1 -1
View File
@@ -12,5 +12,5 @@ contract C {
// ----
// Warning 9302: (96-117): Return value of low-level calls not used.
// Warning 6328: (121-156): CHC: Assertion violation might happen here.
// Warning 6328: (175-211): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0x0\n\nTransaction trace:\nC.constructor()\nC.g(0x0)\n i.call{value: 10}("") -- untrusted external call
// Warning 6328: (175-211): CHC: Assertion violation happens here.
// Warning 4661: (121-156): BMC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/external_calls/call_with_value_2.sol
+1 -1
View File
@@ -11,5 +11,5 @@ contract C {
// ----
// Warning 9302: (96-116): Return value of low-level calls not used.
// Warning 6328: (120-156): CHC: Assertion violation might happen here.
// Warning 6328: (175-210): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0x0\n\nTransaction trace:\nC.constructor()\nC.g(0x0)\n i.call{value: 0}("") -- untrusted external call
// Warning 6328: (175-210): CHC: Assertion violation happens here.
// Warning 4661: (120-156): BMC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol
+2 -1
View File
@@ -18,6 +18,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100)
// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 0\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 0\nC.f()
// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 3\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 3\nC.f()
test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol
+1 -1
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.
test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_3.sol
+1 -3
View File
@@ -14,8 +14,6 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 1218: (202-236): CHC: Error trying to invoke SMT solver.
// Warning 6328: (150-183): CHC: Assertion violation might happen here.
// Warning 6328: (202-236): CHC: Assertion violation might happen here.
// Warning 6328: (202-236): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n i.f{value: 20}() -- untrusted external call
// Warning 4661: (150-183): BMC: Assertion violation happens here.
// Warning 4661: (202-236): BMC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol
+1 -3
View File
@@ -42,6 +42,4 @@ contract C {
// SMTIgnoreOS: macos
// ----
// Warning 2018: (33-88): Function state mutability can be restricted to view
// Warning 1218: (367-381): CHC: Error trying to invoke SMT solver.
// Warning 6328: (367-381): CHC: Assertion violation might happen here.
// Warning 4661: (367-381): BMC: Assertion violation happens here.
// Warning 6328: (367-381): CHC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol
+3 -1
View File
@@ -44,5 +44,7 @@ contract C {
// SMTIgnoreCex: yes
// SMTIgnoreOS: macos
// ----
// Warning 1218: (437-463): CHC: Error trying to invoke SMT solver.
// Warning 6328: (419-433): CHC: Assertion violation happens here.
// Warning 6328: (437-463): CHC: Assertion violation happens here.
// Warning 6328: (437-463): CHC: Assertion violation might happen here.
// Warning 4661: (437-463): BMC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol
+1
View File
@@ -15,6 +15,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 1218: (206-220): CHC: Error trying to invoke SMT solver.
// Warning 6328: (206-220): CHC: Assertion violation might happen here.
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol
+1 -3
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
test/libsolidity/smtCheckerTests/function_selector/homer.sol
+1 -1
View File
@@ -43,4 +43,4 @@ contract Homer is ERC165, Simpson {
// ====
// SMTEngine: all
// ----
// Warning 6328: (1340-1395): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nHomer.constructor()\nHomer.check()\n Homer.supportsInterface(0x73b6b492) -- internal call\n Homer.supportsInterface(0x01ffc9a7) -- internal call\n Homer.supportsInterface(0x8b9eb9ca) -- internal call
// Warning 6328: (1340-1395): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nHomer.constructor()\nHomer.supportsInterface(0x01ffc9a7)\nHomer.check()\n Homer.supportsInterface(0x73b6b492) -- internal call\n Homer.supportsInterface(0x01ffc9a7) -- internal call\n Homer.supportsInterface(0x8b9eb9ca) -- internal call
test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol
+1
View File
@@ -13,5 +13,6 @@ contract C
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (112-125): CHC: Assertion violation happens here.\nCounterexample:\na = 0\n\nTransaction trace:\nC.constructor()\nState: a = 0\nC.g()\n C.f(0) -- internal call
test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol
+6 -2
View File
@@ -18,5 +18,9 @@ function f(uint _x) pure {
// ====
// SMTEngine: all
// ----
// Warning 6328: (A:50-64): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n s1.sol:f(200) -- internal call\n s1.sol:f(0) -- internal call\n A:f(10) -- internal call\n A:f(0) -- internal call
// Warning 6328: (s1.sol:28-44): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n s1.sol:f(200) -- internal call\n s1.sol:f(0) -- internal call
// Warning 1218: (A:50-64): CHC: Error trying to invoke SMT solver.
// Warning 1218: (s1.sol:28-44): CHC: Error trying to invoke SMT solver.
// Warning 6328: (A:50-64): CHC: Assertion violation might happen here.
// Warning 6328: (s1.sol:28-44): CHC: Assertion violation might happen here.
// Warning 4661: (s1.sol:28-44): BMC: Assertion violation happens here.
// Warning 4661: (A:50-64): BMC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/inheritance/receive_fallback.sol
+1 -1
View File
@@ -21,6 +21,6 @@ contract B is A {
// ====
// SMTEngine: all
// ----
// Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.receive(){ msg.value: 2 }
// Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.receive(){ msg.value: 1 }
// Warning 6328: (136-150): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.g()
// Warning 6328: (255-269): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 0\n\nTransaction trace:\nB.constructor()\nState: y = 0, x = 0\nB.fallback()
test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment.sol
+3 -1
View File
@@ -20,4 +20,6 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (254-267): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, owner = 0x0\ny = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, owner = 0x0\nC.g(1)\n C.f() -- internal call
// Warning 1218: (254-267): CHC: Error trying to invoke SMT solver.
// Warning 6328: (254-267): CHC: Assertion violation might happen here.
// Warning 4661: (254-267): BMC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol
+1 -1
View File
@@ -12,4 +12,4 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (162-181): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\np = 0\n\nTransaction trace:\nC.constructor()\nC.f(2, 0)
// Warning 6328: (162-181): CHC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal_3.sol
+1 -2
View File
@@ -18,5 +18,4 @@ contract C {
// SMTEngine: all
// ----
// Warning 6328: (229-276): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 0x6062606464666060606260646466606060626064646660606062606464666060\nz = 0x6062606464666060606260646466606060626064646660606062606464666060\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (394-437): CHC: Assertion violation might happen here.
// Warning 4661: (394-437): BMC: Assertion violation happens here.
// Warning 6328: (394-437): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 0x63666566676e616263666566676e616263666566676e616263666566676e6162\nz = 0x63666566676e616263666566676e616263666566676e616263666566676e6162\n\nTransaction trace:\nC.constructor()\nC.f()
test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol
+2 -1
View File
@@ -21,6 +21,7 @@ contract C {
// SMTIgnoreOS: macos
// ----
// Warning 4984: (112-115): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 3944: (181-184): CHC: Underflow (resulting value less than 0) might happen here.
// Warning 6368: (259-263): CHC: Out of bounds access happens here.\nCounterexample:\na = [0], l = 1\n = 0\n\nTransaction trace:\nC.constructor()\nState: a = [], l = 0\nC.p()\nState: a = [0], l = 1\nC.r()
// Info 1180: Contract invariant(s) for :C:\n((a.length + ((- 1) * l)) <= 0)\n
// Warning 2661: (112-115): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4144: (181-184): BMC: Underflow (resulting value less than 0) happens here.
test/libsolidity/smtCheckerTests/overflow/signed_guard_sub_overflow.sol
+1 -1
View File
@@ -8,4 +8,4 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = 0\ny = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, (- 57896044618658097711785492504343953926634992332820282019728792003956564819968))
// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = 57896044618658097711785492504343953926634992332820282019728792003956564819967\ny = (- 1)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(57896044618658097711785492504343953926634992332820282019728792003956564819967, (- 1))
test/libsolidity/smtCheckerTests/overflow/simple_overflow.sol
+1 -1
View File
@@ -4,4 +4,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 4984: (80-85): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\na = 1\nb = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935)
// Warning 4984: (80-85): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\na = 115792089237316195423570985008687907853269984665640564039457584007913129639935\nb = 1\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(115792089237316195423570985008687907853269984665640564039457584007913129639935, 1)
test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol
+2 -1
View File
@@ -31,5 +31,6 @@ contract C {
}
// ====
// SMTEngine: chc
// SMTIgnoreOS: macos
// ----
// Warning 6328: (770-799): CHC: Assertion violation happens here.\nCounterexample:\ncoin = 0x1e28, dif = 0, gas = 0, number = 0, timestamp = 0\n\nTransaction trace:\nC.constructor()\nState: coin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\nC.f(){ block.coinbase: 0x1e28, block.difficulty: 0, block.gaslimit: 0, block.number: 0, block.timestamp: 0 }\n C.g() -- internal call
// Warning 6328: (770-799): CHC: Assertion violation happens here.\nCounterexample:\ncoin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\n\nTransaction trace:\nC.constructor()\nState: coin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\nC.f(){ block.coinbase: 0x0, block.difficulty: 0, block.gaslimit: 0, block.number: 0, block.timestamp: 0 }\n C.g() -- internal call
test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol
+1 -1
View File
@@ -13,4 +13,4 @@ contract C {
// SMTEngine: all
// 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
// Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 868\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 500 }\n _i.f() -- untrusted external call, synthesized as:\n C.g(0){ msg.value: 0 } -- reentrant call\n _i.f() -- untrusted external call
test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol
+1 -1
View File
@@ -21,4 +21,4 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (280-300): CHC: Assertion violation happens here.
// Warning 6328: (280-300): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol
-8
View File
@@ -3,20 +3,12 @@ contract C {
bytes memory b = hex"00010203040506070809000102030405060708090001020304050607080900010203040506070809";
bytes8 c = bytes8(b);
assert(c == 0x0001020304050607); // should hold
assert(c == 0x0001020304050608); // should fail
bytes16 d = bytes16(b);
assert(d == 0x00010203040506070809000102030405);
assert(d == 0x00010203040506070809000102030406); // should fail
bytes24 e = bytes24(b);
assert(e == 0x000102030405060708090001020304050607080900010203); // should hold
assert(e == 0x000102030405060708090001020304050607080900010204); // should fail
bytes32 g = bytes32(b);
assert(g == 0x0001020304050607080900010203040506070809000102030405060708090001); // should hold
assert(g == 0x0001020304050607080900010203040506070809000102030405060708090002); // should fail
}
}
// ----
// Warning 6328: (225-256): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x0\ne = 0x0\ng = 0x0\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (352-399): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x010203040506070809000102030405\ne = 0x0\ng = 0x0\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (526-589): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x010203040506070809000102030405\ne = 0x0102030405060708090001020304050607080900010203\ng = 0x0\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (732-811): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x010203040506070809000102030405\ne = 0x0102030405060708090001020304050607080900010203\ng = 0x01020304050607080900010203040506070809000102030405060708090001\n\nTransaction trace:\nC.constructor()\nC.f()
test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1_fail.sol
+25
View File
@@ -0,0 +1,25 @@
contract C {
function f() external pure {
bytes memory b = hex"00010203040506070809000102030405060708090001020304050607080900010203040506070809";
bytes8 c = bytes8(b);
//assert(c == 0x0001020304050607); // should hold
assert(c == 0x0001020304050608); // should fail
bytes16 d = bytes16(b);
//assert(d == 0x00010203040506070809000102030405);
assert(d == 0x00010203040506070809000102030406); // should fail
bytes24 e = bytes24(b);
//assert(e == 0x000102030405060708090001020304050607080900010203); // should hold
assert(e == 0x000102030405060708090001020304050607080900010204); // should fail
bytes32 g = bytes32(b);
//assert(g == 0x0001020304050607080900010203040506070809000102030405060708090001); // should hold
assert(g == 0x0001020304050607080900010203040506070809000102030405060708090002); // should fail
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (227-258): CHC: Assertion violation happens here.
// Warning 6328: (356-403): CHC: Assertion violation happens here.
// Warning 6328: (532-595): CHC: Assertion violation happens here.
// Warning 6328: (740-819): CHC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol
+1 -1
View File
@@ -11,4 +11,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (132-160): CHC: Assertion violation happens here.\nCounterexample:\nx = [0x61, 0x62, 0x63, 0x61]\n\nTransaction trace:\nC.constructor()\nState: x = []\nC.s()
// Warning 6328: (132-160): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nState: x = []\nC.s()
test/libsolidity/smtCheckerTests/types/array_branch_1d.sol
+3 -1
View File
@@ -12,4 +12,6 @@ contract C
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (143-159): CHC: Assertion violation happens here.
// Warning 1218: (143-159): CHC: Error trying to invoke SMT solver.
// Warning 6328: (143-159): CHC: Assertion violation might happen here.
// Warning 4661: (143-159): BMC: Assertion violation happens here.