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 SMTChecker tests

Browse Source
This commit is contained in:
Leo Alt 2021-08-27 11:40:44 +02:00
parent 4d414a6d58
commit 0cc9162fb5
62 changed files with 0 additions and 350 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
test/libsolidity/smtCheckerTests/abi/abi_decode_1_tuple.sol
View File

@ -8,5 +8,3 @@ contract C {
// ----
// Warning 8364: (116-125): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (115-126): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (116-125): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (115-126): Assertion checker does not yet implement type type(uint256[] memory)

14
test/libsolidity/smtCheckerTests/abi/abi_decode_array.sol
View File

@ -59,20 +59,6 @@ contract C {
// Warning 6328: (1009-1037): CHC: Assertion violation might happen here.
// Warning 6328: (1056-1084): CHC: Assertion violation might happen here.
// Warning 6328: (1103-1131): CHC: Assertion violation might happen here.
// Warning 8364: (162-168): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (170-176): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (283-289): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (291-297): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (532-538): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (540-546): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (548-554): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (769-775): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (769-777): Assertion checker does not yet implement type type(uint256[] memory[] memory)
// Warning 8364: (779-785): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (779-787): Assertion checker does not yet implement type type(uint256[] memory[] memory)
// Warning 8364: (779-789): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory)
// Warning 8364: (989-995): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (997-1003): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 4661: (1009-1037): BMC: Assertion violation happens here.
// Warning 4661: (1056-1084): BMC: Assertion violation happens here.
// Warning 4661: (1103-1131): BMC: Assertion violation happens here.

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

@ -7,4 +7,3 @@ contract C {
// SMTEngine: all
// ----
// Warning 6031: (54-60): Internal error: Expression undefined for SMT solver.
// Warning 6031: (54-60): Internal error: Expression undefined for SMT solver.

1
test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol
View File

@ -24,4 +24,3 @@ contract C {
// ----
// Warning 6328: (315-331): CHC: Assertion violation happens here.
// Warning 1236: (87-100): BMC: Insufficient funds happens here.
// Warning 1236: (87-100): BMC: Insufficient funds happens here.

1
test/libsolidity/smtCheckerTests/blockchain_state/library_public_1.sol
View File

@ -21,4 +21,3 @@ contract C {
// Warning 4588: (219-224): Assertion checker does not yet implement this type of function call.
// Warning 6328: (263-279): CHC: Assertion violation happens here.
// Warning 6328: (359-373): CHC: Assertion violation happens here.
// Warning 4588: (219-224): Assertion checker does not yet implement this type of function call.

1
test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol
View File

@ -24,4 +24,3 @@ contract C {
// Warning 6328: (282-298): CHC: Assertion violation happens here.
// Warning 6328: (317-331): CHC: Assertion violation happens here.
// Warning 1236: (54-67): BMC: Insufficient funds happens here.
// Warning 4588: (238-243): Assertion checker does not yet implement this type of function call.

1
test/libsolidity/smtCheckerTests/blockchain_state/library_public_3.sol
View File

@ -26,4 +26,3 @@ contract C {
// Warning 6328: (309-325): CHC: Assertion violation happens here.
// Warning 6328: (405-419): CHC: Assertion violation happens here.
// Warning 6328: (464-486): CHC: Assertion violation happens here.
// Warning 4588: (265-270): Assertion checker does not yet implement this type of function call.

1
test/libsolidity/smtCheckerTests/blockchain_state/library_public_4.sol
View File

@ -27,4 +27,3 @@ contract C {
// Warning 6328: (316-332): CHC: Assertion violation happens here.
// Warning 6328: (412-426): CHC: Assertion violation happens here.
// Warning 6328: (471-494): CHC: Assertion violation happens here.
// Warning 4588: (272-277): Assertion checker does not yet implement this type of function call.

1
test/libsolidity/smtCheckerTests/bmc_coverage/unchecked_function_call_with_unchecked_block.sol
View File

@ -13,4 +13,3 @@ contract C {
// SMTEngine: bmc
// ----
// Warning 4661: (85-98): BMC: Assertion violation happens here.
// Warning 4661: (85-98): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/complex/slither/external_function.sol
View File

@ -85,6 +85,4 @@ contract InternalCall {
// Warning 2018: (1247-1309): Function state mutability can be restricted to pure
// Warning 4588: (681-716): Assertion checker does not yet implement this type of function call.
// Warning 4588: (854-886): Assertion checker does not yet implement this type of function call.
// Warning 4588: (681-716): Assertion checker does not yet implement this type of function call.
// Warning 4588: (854-886): Assertion checker does not yet implement this type of function call.
// Warning 5729: (1370-1375): BMC does not yet implement this type of function call.

1
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol
View File

@ -27,6 +27,5 @@ contract C {
// SMTEngine: all
// ----
// Warning 1218: (302-333): CHC: Error trying to invoke SMT solver.
// Warning 1218: (302-333): CHC: Error trying to invoke SMT solver.
// Warning 6328: (302-333): CHC: Assertion violation might happen here.
// Warning 4661: (302-333): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/file_level/file_level_call_via_module.sol
View File

@ -22,5 +22,3 @@ contract C {
// Warning 8364: (b.sol:103-104): Assertion checker does not yet implement type module "a.sol"
// Warning 6328: (b.sol:208-222): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7\nb = 3\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call\n a.sol:f(2) -- internal call\n a.sol:f([97, 98, 99]) -- internal call
// Warning 6328: (b.sol:274-288): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7\nb = 3\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call\n a.sol:f(2) -- internal call\n a.sol:f([97, 98, 99]) -- internal call
// Warning 8364: (b.sol:95-96): Assertion checker does not yet implement type module "a.sol"
// Warning 8364: (b.sol:103-104): Assertion checker does not yet implement type module "a.sol"

2
test/libsolidity/smtCheckerTests/file_level/free_runtimecode.sol
View File

@ -15,6 +15,4 @@ contract D {
// SMTEngine: all
// ----
// Warning 7507: (82-101): Assertion checker does not yet support this expression.
// Warning 7507: (82-101): Assertion checker does not yet support this expression.
// Warning 6328: (161-175): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nD.constructor()\nD.f()\n test() -- internal call
// Warning 7507: (82-101): Assertion checker does not yet support this expression.

1
test/libsolidity/smtCheckerTests/file_level/import.sol
View File

@ -25,4 +25,3 @@ contract C {
// Warning 8364: (B:115-116): Assertion checker does not yet implement type module "A"
// Warning 6328: (B:238-252): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 0}\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n C.f(7) -- internal call\n A:set({x: 0}, 7) -- internal call\n A:set({x: 0}, 8) -- internal call
// Warning 6328: (B:308-322): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 0}\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n C.f(7) -- internal call\n A:set({x: 0}, 7) -- internal call\n A:set({x: 0}, 8) -- internal call
// Warning 8364: (B:115-116): Assertion checker does not yet implement type module "A"

2
test/libsolidity/smtCheckerTests/file_level/libraries_from_free.sol
View File

@ -23,7 +23,5 @@ contract C {
// SMTIgnoreCex: yes
// ----
// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.
// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.
// Warning 6328: (284-298): CHC: Assertion violation happens here.
// Warning 6328: (363-377): CHC: Assertion violation happens here.
// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.

2
test/libsolidity/smtCheckerTests/file_level/new_operator.sol
View File

@ -15,6 +15,4 @@ contract D {
// SMTEngine: all
// ----
// Warning 4588: (78-85): Assertion checker does not yet implement this type of function call.
// Warning 4588: (78-85): Assertion checker does not yet implement this type of function call.
// Warning 6328: (133-152): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nD.constructor()\nD.f()\n test() -- internal call\n (new C()).x() -- untrusted external call
// Warning 4588: (78-85): Assertion checker does not yet implement this type of function call.

3
test/libsolidity/smtCheckerTests/file_level/same_constants_different_files.sol
View File

@ -32,6 +32,3 @@ contract C {
// Warning 7650: (s2.sol:182-185): Assertion checker does not yet support this expression.
// Warning 8364: (s2.sol:182-183): Assertion checker does not yet implement type module "s1.sol"
// Warning 6328: (s2.sol:334-349): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 13\ny = 89\nz = 0\nt = 89\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call\n s1.sol:fre() -- internal call
// Warning 7650: (s2.sol:182-185): Assertion checker does not yet support this expression.
// Warning 8364: (s2.sol:182-183): Assertion checker does not yet implement type module "s1.sol"
// Warning 7650: (s2.sol:182-185): Assertion checker does not yet support this expression.

2
test/libsolidity/smtCheckerTests/function_selector/function_types_sig.sol
View File

@ -27,5 +27,3 @@ contract C {
// Warning 7650: (251-263): Assertion checker does not yet support this expression.
// Warning 6328: (437-462): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.check()\n C.f() -- internal call\n C.g() -- internal call
// Warning 6328: (507-532): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.check()\n C.f() -- internal call\n C.g() -- internal call\n C.i() -- internal call\n C.i() -- internal call
// Warning 7650: (251-263): Assertion checker does not yet support this expression.
// Warning 7650: (251-263): Assertion checker does not yet support this expression.

2
test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol
View File

@ -22,5 +22,3 @@ function f(uint _x) pure {
// Warning 8364: (A:145-146): Assertion checker does not yet implement type module "s1.sol"
// 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 8364: (A:118-119): Assertion checker does not yet implement type module "s1.sol"
// Warning 8364: (A:145-146): Assertion checker does not yet implement type module "s1.sol"

1
test/libsolidity/smtCheckerTests/imports/imported_fail_1.sol
View File

@ -23,5 +23,4 @@ contract C is B {
// SMTEngine: all
// ----
// Warning 6328: (B.sol:71-85): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n_x = 0\n\nTransaction trace:\nB.constructor()\nState: x = 0\nB.g(0)
// Warning 6328: (B.sol:71-85): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n_x = 0\n\nTransaction trace:\nB.constructor()\nState: x = 0\nB.g(0)
// Warning 6328: (C.sol:71-85): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n_x = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.h(0)

1
test/libsolidity/smtCheckerTests/imports/imported_fail_2.sol
View File

@ -23,5 +23,4 @@ contract C is B {
// SMTEngine: all
// ----
// Warning 6328: (B.sol:71-85): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n_x = 0\n\nTransaction trace:\nB.constructor()\nState: x = 0\nB.g(0)
// Warning 6328: (B.sol:71-85): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n_x = 0\n\nTransaction trace:\nB.constructor()\nState: x = 0\nB.g(0)
// Warning 6328: (C.sol:71-85): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n_x = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.h(0)

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

@ -17,8 +17,3 @@ contract C {
// Warning 7737: (70-89): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
// Warning 6328: (239-250): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call
// Warning 6328: (282-294): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call\n C.f() -- internal call
// Warning 7737: (70-89): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
// Warning 7737: (70-89): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
// Warning 7737: (70-89): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
// Warning 7737: (70-89): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
// Warning 7737: (70-89): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

1
test/libsolidity/smtCheckerTests/inline_assembly/assembly_2.sol
View File

@ -13,4 +13,3 @@ contract C {
// ----
// Warning 7737: (82-101): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
// Warning 6328: (138-147): CHC: Assertion violation happens here.\nCounterexample:\n\n = false\nb = false\nx = 42\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 7737: (82-101): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

1
test/libsolidity/smtCheckerTests/inline_assembly/assembly_3.sol
View File

@ -13,4 +13,3 @@ contract C {
// ----
// Warning 7737: (106-125): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
// Warning 6328: (203-212): CHC: Assertion violation happens here.\nCounterexample:\n\n = false\nb = false\nc = true\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 7737: (106-125): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

1
test/libsolidity/smtCheckerTests/inline_assembly/assembly_4.sol
View File

@ -13,4 +13,3 @@ contract C {
// SMTEngine: all
// ----
// Warning 7737: (82-101): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
// Warning 7737: (82-101): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

1
test/libsolidity/smtCheckerTests/inline_assembly/assembly_5.sol
View File

@ -23,4 +23,3 @@ contract C {
// SMTEngine: all
// ----
// Warning 7737: (156-187): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
// Warning 7737: (156-187): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

1
test/libsolidity/smtCheckerTests/inline_assembly/assembly_6.sol
View File

@ -22,4 +22,3 @@ contract C {
// SMTEngine: all
// ----
// Warning 7737: (157-193): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
// Warning 7737: (157-193): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

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

@ -22,4 +22,3 @@ contract C {
// Warning 7737: (83-149): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
// 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).

1
test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_pointer.sol
View File

@ -21,4 +21,3 @@ contract C {
// Warning 7737: (170-205): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
// Warning 6328: (208-229): CHC: Assertion violation happens here.
// Warning 6328: (248-269): CHC: Assertion violation happens here.
// Warning 7737: (170-205): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

1
test/libsolidity/smtCheckerTests/inline_assembly/assembly_memory_write.sol
View File

@ -26,4 +26,3 @@ contract C {
// Warning 7737: (156-187): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
// Warning 6328: (190-208): CHC: Assertion violation happens here.
// Warning 6328: (227-244): CHC: Assertion violation happens here.
// Warning 7737: (156-187): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

1
test/libsolidity/smtCheckerTests/inline_assembly/empty.sol
View File

@ -9,4 +9,3 @@ contract C
// SMTEngine: all
// ----
// Warning 7737: (43-57): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
// Warning 7737: (43-57): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

1
test/libsolidity/smtCheckerTests/inline_assembly/local_var.sol
View File

@ -11,4 +11,3 @@ contract C
// SMTEngine: all
// ----
// Warning 7737: (64-88): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
// Warning 7737: (64-88): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

1
test/libsolidity/smtCheckerTests/natspec/natspec_smtchecker_empty.sol
View File

@ -8,4 +8,3 @@ contract C {
// SMTEngine: chc
// ----
// Warning 3130: (38-102): Unknown option for "custom:smtchecker": ""
// Warning 3130: (38-102): Unknown option for "custom:smtchecker": ""

1
test/libsolidity/smtCheckerTests/natspec/natspec_smtchecker_error_1.sol
View File

@ -8,4 +8,3 @@ contract C {
// SMTEngine: chc
// ----
// Warning 3130: (56-120): Unknown option for "custom:smtchecker": "abstract-function"
// Warning 3130: (56-120): Unknown option for "custom:smtchecker": "abstract-function"

1
test/libsolidity/smtCheckerTests/operators/exp.sol
View File

@ -8,4 +8,3 @@ contract D {
// ----
// Warning 5188: (56-60): Assertion checker does not yet implement this operator.
// Warning 6328: (49-66): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nD.constructor()\nD.f(0)
// Warning 5188: (56-60): Assertion checker does not yet implement this operator.

3
test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol
View File

@ -12,6 +12,3 @@ contract C {
// Warning 8364: (183-189): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (183-192): Assertion checker does not yet implement type type(uint256[] memory[2] memory)
// Warning 8364: (173-174): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning 8364: (183-189): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (183-192): Assertion checker does not yet implement type type(uint256[] memory[2] memory)
// Warning 8364: (173-174): Assertion checker does not yet implement type type(struct C.S storage pointer)

2
test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol
View File

@ -16,5 +16,3 @@ contract C {
// Warning 8364: (123-124): Assertion checker does not yet implement type type(contract C)
// Warning 8364: (193-194): Assertion checker does not yet implement type type(contract C)
// Warning 6328: (220-236): CHC: Assertion violation happens here.\nCounterexample:\n\na1 = 2437\nb1 = 10\nc1 = 9\na2 = 2437\nb2 = 10\nc2 = 9\n\nTransaction trace:\nC.constructor()\nC.f(data)
// Warning 8364: (123-124): Assertion checker does not yet implement type type(contract C)
// Warning 8364: (193-194): Assertion checker does not yet implement type type(contract C)

2
test/libsolidity/smtCheckerTests/try_catch/try_new.sol
View File

@ -30,5 +30,3 @@ contract C {
// ----
// Warning 4588: (231-245): Assertion checker does not yet implement this type of function call.
// Warning 4588: (492-507): Assertion checker does not yet implement this type of function call.
// Warning 4588: (231-245): Assertion checker does not yet implement this type of function call.
// Warning 4588: (492-507): Assertion checker does not yet implement this type of function call.

4
test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol
View File

@ -20,7 +20,3 @@ contract C {
// Warning 6328: (199-213): CHC: Assertion violation happens here.\nCounterexample:\na = 0, b = 0\n\nTransaction trace:\nC.constructor()\nState: a = 0, b = 0\nC.g()\n C.f(0, 0) -- internal call
// Warning 5729: (182-186): BMC does not yet implement this type of function call.
// Warning 5729: (190-194): BMC does not yet implement this type of function call.
// Warning 7229: (206-212): Assertion checker does not yet implement the type function (uint256) returns (uint256) for comparisons
// Warning 5729: (182-186): BMC does not yet implement this type of function call.
// Warning 5729: (190-194): BMC does not yet implement this type of function call.
// Warning 7229: (206-212): Assertion checker does not yet implement the type function (uint256) returns (uint256) for comparisons

1
test/libsolidity/smtCheckerTests/types/address_delegatecall.sol
View File

@ -24,4 +24,3 @@ contract C
// Warning 6328: (254-268): CHC: Assertion violation happens here.
// Warning 6328: (272-291): CHC: Assertion violation happens here.
// Warning 6328: (295-319): CHC: Assertion violation happens here.
// Warning 4588: (211-231): Assertion checker does not yet implement this type of function call.

1
test/libsolidity/smtCheckerTests/types/array_aliasing_storage_3.sol
View File

@ -43,4 +43,3 @@ contract C
// Warning 6328: (948-965): CHC: Assertion violation might happen here.
// Warning 6368: (976-980): CHC: Out of bounds access might happen here.
// Warning 4661: (948-965): BMC: Assertion violation happens here.
// Warning 4661: (948-965): BMC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/types/function_type_call.sol
View File

@ -11,4 +11,3 @@ contract C {
// SMTEngine: all
// ----
// Warning 5729: (89-93): BMC does not yet implement this type of function call.
// Warning 5729: (89-93): BMC does not yet implement this type of function call.

1
test/libsolidity/smtCheckerTests/types/function_type_external_address.sol
View File

@ -8,4 +8,3 @@ contract C {
// SMTEngine: all
// ----
// Warning 7650: (96-105): Assertion checker does not yet support this expression.
// Warning 7650: (96-105): Assertion checker does not yet support this expression.

1
test/libsolidity/smtCheckerTests/types/function_type_members.sol
View File

@ -8,4 +8,3 @@ contract C {
// SMTEngine: all
// ----
// Warning 7650: (76-86): Assertion checker does not yet support this expression.
// Warning 7650: (76-86): Assertion checker does not yet support this expression.

4
test/libsolidity/smtCheckerTests/types/function_type_nested.sol
View File

@ -18,8 +18,4 @@ contract C {
// Warning 6031: (223-225): Internal error: Expression undefined for SMT solver.
// Warning 8364: (223-225): Assertion checker does not yet implement type function (function (uint256))
// Warning 5729: (91-96): BMC does not yet implement this type of function call.
// Warning 8364: (180-182): Assertion checker does not yet implement type function (function (uint256))
// Warning 5729: (180-187): BMC does not yet implement this type of function call.
// Warning 6031: (223-225): Internal error: Expression undefined for SMT solver.
// Warning 8364: (223-225): Assertion checker does not yet implement type function (function (uint256))
// Warning 5729: (180-187): BMC does not yet implement this type of function call.

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

@ -22,9 +22,4 @@ contract C {
// Warning 6031: (295-297): Internal error: Expression undefined for SMT solver.
// Warning 8364: (295-297): Assertion checker does not yet implement type function (function (uint256))
// Warning 5729: (163-168): BMC does not yet implement this type of function call.
// Warning 8364: (252-254): Assertion checker does not yet implement type function (function (uint256))
// Warning 1695: (255-256): Assertion checker does not yet support this global variable.
// Warning 5729: (252-259): BMC does not yet implement this type of function call.
// Warning 6031: (295-297): Internal error: Expression undefined for SMT solver.
// Warning 8364: (295-297): Assertion checker does not yet implement type function (function (uint256))
// Warning 5729: (252-259): BMC does not yet implement this type of function call.

2
test/libsolidity/smtCheckerTests/types/no_effect_statements.sol
View File

@ -19,5 +19,3 @@ contract test {
// Warning 6133: (129-136): Statement has no effect.
// Warning 8364: (113-117): Assertion checker does not yet implement type type(struct test.s memory[7] memory)
// Warning 8364: (129-136): Assertion checker does not yet implement type type(uint256[7] memory)
// Warning 8364: (113-117): Assertion checker does not yet implement type type(struct test.s memory[7] memory)
// Warning 8364: (129-136): Assertion checker does not yet implement type type(uint256[7] memory)

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

@ -11,4 +11,3 @@ contract Test {
// ----
// Warning 2072: (104-133): Unused local variable.
// Warning 8364: (138-180): Assertion checker does not yet implement type struct Test.RecursiveStruct memory
// Warning 8364: (138-180): Assertion checker does not yet implement type struct Test.RecursiveStruct memory

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

@ -16,6 +16,3 @@ contract Test {
// Warning 7650: (199-204): Assertion checker does not yet support this expression.
// Warning 8364: (199-202): Assertion checker does not yet implement type struct Test.RecursiveStruct memory
// Warning 6328: (192-210): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nTest.constructor()\nTest.func()
// Warning 8364: (143-188): Assertion checker does not yet implement type struct Test.RecursiveStruct memory
// Warning 7650: (199-204): Assertion checker does not yet support this expression.
// Warning 8364: (199-202): Assertion checker does not yet implement type struct Test.RecursiveStruct memory

8
test/libsolidity/smtCheckerTests/types/struct/struct_recursive_1.sol
View File

@ -25,11 +25,3 @@ contract C {
// Warning 8364: (137-139): Assertion checker does not yet implement type struct C.S storage ref
// Warning 6328: (91-111): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (115-149): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 7650: (98-102): Assertion checker does not yet support this expression.
// Warning 8364: (98-100): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (106-110): Assertion checker does not yet support this expression.
// Warning 8364: (106-108): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (122-126): Assertion checker does not yet support this expression.
// Warning 8364: (122-124): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (137-141): Assertion checker does not yet support this expression.
// Warning 8364: (137-139): Assertion checker does not yet implement type struct C.S storage ref

40
test/libsolidity/smtCheckerTests/types/struct/struct_recursive_2.sol
View File

@ -71,43 +71,3 @@ contract C {
// Warning 6328: (153-183): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6368: (269-276): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()
// Warning 6368: (287-294): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()
// Warning 7650: (98-102): Assertion checker does not yet support this expression.
// Warning 8364: (98-100): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (106-110): Assertion checker does not yet support this expression.
// Warning 8364: (106-108): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (122-126): Assertion checker does not yet support this expression.
// Warning 8364: (122-124): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (137-141): Assertion checker does not yet support this expression.
// Warning 8364: (137-139): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (160-169): Assertion checker does not yet support this expression.
// Warning 7650: (160-164): Assertion checker does not yet support this expression.
// Warning 8364: (160-162): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (160-167): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (173-182): Assertion checker does not yet support this expression.
// Warning 7650: (173-177): Assertion checker does not yet support this expression.
// Warning 8364: (173-175): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (173-180): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (213-217): Assertion checker does not yet support this expression.
// Warning 8364: (213-215): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (213-217): Assertion checker does not support recursive structs.
// Warning 7650: (226-230): Assertion checker does not yet support this expression.
// Warning 8364: (226-228): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (226-230): Assertion checker does not support recursive structs.
// Warning 7650: (239-243): Assertion checker does not yet support this expression.
// Warning 8364: (239-241): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (239-250): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (239-243): Assertion checker does not support recursive structs.
// Warning 7650: (254-258): Assertion checker does not yet support this expression.
// Warning 8364: (254-256): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (254-265): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (254-258): Assertion checker does not support recursive structs.
// Warning 7650: (269-278): Assertion checker does not yet support this expression.
// Warning 7650: (269-273): Assertion checker does not yet support this expression.
// Warning 8364: (269-271): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (269-276): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (269-278): Assertion checker does not support recursive structs.
// Warning 7650: (287-296): Assertion checker does not yet support this expression.
// Warning 7650: (287-291): Assertion checker does not yet support this expression.
// Warning 8364: (287-289): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (287-294): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (287-296): Assertion checker does not support recursive structs.

86
test/libsolidity/smtCheckerTests/types/struct/struct_recursive_3.sol
View File

@ -141,89 +141,3 @@ contract C {
// Warning 6368: (681-693): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()
// Warning 6368: (704-711): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()
// Warning 6368: (704-716): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()
// Warning 7650: (98-102): Assertion checker does not yet support this expression.
// Warning 8364: (98-100): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (106-110): Assertion checker does not yet support this expression.
// Warning 8364: (106-108): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (122-126): Assertion checker does not yet support this expression.
// Warning 8364: (122-124): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (137-141): Assertion checker does not yet support this expression.
// Warning 8364: (137-139): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (161-165): Assertion checker does not yet support this expression.
// Warning 8364: (161-163): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (189-193): Assertion checker does not yet support this expression.
// Warning 8364: (189-191): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (216-225): Assertion checker does not yet support this expression.
// Warning 7650: (216-220): Assertion checker does not yet support this expression.
// Warning 8364: (216-218): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (216-223): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (229-238): Assertion checker does not yet support this expression.
// Warning 7650: (229-233): Assertion checker does not yet support this expression.
// Warning 8364: (229-231): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (229-236): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (251-260): Assertion checker does not yet support this expression.
// Warning 7650: (251-255): Assertion checker does not yet support this expression.
// Warning 8364: (251-253): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (251-258): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (284-293): Assertion checker does not yet support this expression.
// Warning 7650: (284-288): Assertion checker does not yet support this expression.
// Warning 8364: (284-286): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (284-291): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (316-325): Assertion checker does not yet support this expression.
// Warning 7650: (316-320): Assertion checker does not yet support this expression.
// Warning 8364: (316-318): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (316-323): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (336-345): Assertion checker does not yet support this expression.
// Warning 7650: (336-340): Assertion checker does not yet support this expression.
// Warning 8364: (336-338): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (336-343): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (549-553): Assertion checker does not yet support this expression.
// Warning 8364: (549-551): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (549-553): Assertion checker does not support recursive structs.
// Warning 7650: (562-566): Assertion checker does not yet support this expression.
// Warning 8364: (562-564): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (562-566): Assertion checker does not support recursive structs.
// Warning 7650: (575-579): Assertion checker does not yet support this expression.
// Warning 8364: (575-577): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (575-586): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (575-579): Assertion checker does not support recursive structs.
// Warning 7650: (590-594): Assertion checker does not yet support this expression.
// Warning 8364: (590-592): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (590-601): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (590-594): Assertion checker does not support recursive structs.
// Warning 7650: (605-614): Assertion checker does not yet support this expression.
// Warning 7650: (605-609): Assertion checker does not yet support this expression.
// Warning 8364: (605-607): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (605-612): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (605-614): Assertion checker does not support recursive structs.
// Warning 7650: (623-632): Assertion checker does not yet support this expression.
// Warning 7650: (623-627): Assertion checker does not yet support this expression.
// Warning 8364: (623-625): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (623-630): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (623-632): Assertion checker does not support recursive structs.
// Warning 7650: (641-650): Assertion checker does not yet support this expression.
// Warning 7650: (641-645): Assertion checker does not yet support this expression.
// Warning 8364: (641-643): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (641-648): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (641-657): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (641-650): Assertion checker does not support recursive structs.
// Warning 7650: (661-670): Assertion checker does not yet support this expression.
// Warning 7650: (661-665): Assertion checker does not yet support this expression.
// Warning 8364: (661-663): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (661-668): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (661-677): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (661-670): Assertion checker does not support recursive structs.
// Warning 7650: (681-695): Assertion checker does not yet support this expression.
// Warning 7650: (681-690): Assertion checker does not yet support this expression.
// Warning 7650: (681-685): Assertion checker does not yet support this expression.
// Warning 8364: (681-683): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (681-688): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (681-693): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (681-695): Assertion checker does not support recursive structs.
// Warning 7650: (704-718): Assertion checker does not yet support this expression.
// Warning 7650: (704-713): Assertion checker does not yet support this expression.
// Warning 7650: (704-708): Assertion checker does not yet support this expression.
// Warning 8364: (704-706): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (704-711): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (704-716): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (704-718): Assertion checker does not support recursive structs.

29
test/libsolidity/smtCheckerTests/types/struct/struct_recursive_4.sol
View File

@ -55,32 +55,3 @@ contract C {
// Warning 6328: (164-200): CHC: Assertion violation happens here.
// Warning 6328: (204-240): CHC: Assertion violation happens here.
// Warning 6328: (326-358): CHC: Assertion violation happens here.
// Warning 8364: (122-124): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (127-129): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (117-129): Assertion checker does not yet implement type struct C.S storage pointer
// Warning 8364: (153-155): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (158-160): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (148-160): Assertion checker does not yet implement type struct C.S storage pointer
// Warning 7650: (171-175): Assertion checker does not yet support this expression.
// Warning 8364: (171-173): Assertion checker does not yet implement type struct C.S storage pointer
// Warning 7650: (179-183): Assertion checker does not yet support this expression.
// Warning 8364: (179-181): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (187-191): Assertion checker does not yet support this expression.
// Warning 8364: (187-189): Assertion checker does not yet implement type struct C.S storage pointer
// Warning 7650: (195-199): Assertion checker does not yet support this expression.
// Warning 8364: (195-197): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (211-215): Assertion checker does not yet support this expression.
// Warning 8364: (211-213): Assertion checker does not yet implement type struct C.S storage pointer
// Warning 7650: (219-223): Assertion checker does not yet support this expression.
// Warning 8364: (219-221): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (227-231): Assertion checker does not yet support this expression.
// Warning 8364: (227-229): Assertion checker does not yet implement type struct C.S storage pointer
// Warning 7650: (235-239): Assertion checker does not yet support this expression.
// Warning 8364: (235-237): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (244-248): Assertion checker does not yet support this expression.
// Warning 8364: (244-246): Assertion checker does not yet implement type struct C.S storage pointer
// Warning 4375: (244-248): Assertion checker does not support recursive structs.
// Warning 7650: (333-337): Assertion checker does not yet support this expression.
// Warning 8364: (333-335): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (347-351): Assertion checker does not yet support this expression.
// Warning 8364: (347-349): Assertion checker does not yet implement type struct C.S storage ref

10
test/libsolidity/smtCheckerTests/types/struct/struct_recursive_5.sol
View File

@ -27,13 +27,3 @@ contract C {
// Warning 7650: (188-195): Assertion checker does not yet support this expression.
// Warning 8364: (188-193): Assertion checker does not yet implement type struct C.S storage ref
// Warning 6328: (159-203): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 8364: (93-102): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (120-133): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (137-148): Assertion checker does not yet support this expression.
// Warning 8364: (137-146): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (137-155): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (137-148): Assertion checker does not support recursive structs.
// Warning 7650: (166-177): Assertion checker does not yet support this expression.
// Warning 8364: (166-175): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (188-195): Assertion checker does not yet support this expression.
// Warning 8364: (188-193): Assertion checker does not yet implement type struct C.S storage ref

29
test/libsolidity/smtCheckerTests/types/struct/struct_recursive_6.sol
View File

@ -60,32 +60,3 @@ contract C {
// Warning 6328: (152-176): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (180-214): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (231-248): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 7650: (86-90): Assertion checker does not yet support this expression.
// Warning 8364: (86-88): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (86-90): Assertion checker does not support recursive structs.
// Warning 7650: (101-105): Assertion checker does not yet support this expression.
// Warning 8364: (101-103): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (101-105): Assertion checker does not support recursive structs.
// Warning 7650: (109-113): Assertion checker does not yet support this expression.
// Warning 8364: (109-111): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (109-113): Assertion checker does not support recursive structs.
// Warning 7650: (119-123): Assertion checker does not yet support this expression.
// Warning 8364: (119-121): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (119-123): Assertion checker does not support recursive structs.
// Warning 7650: (134-138): Assertion checker does not yet support this expression.
// Warning 8364: (134-136): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (134-138): Assertion checker does not support recursive structs.
// Warning 7650: (142-146): Assertion checker does not yet support this expression.
// Warning 8364: (142-144): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (142-146): Assertion checker does not support recursive structs.
// Warning 7650: (159-163): Assertion checker does not yet support this expression.
// Warning 8364: (159-161): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (167-171): Assertion checker does not yet support this expression.
// Warning 8364: (167-169): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (187-191): Assertion checker does not yet support this expression.
// Warning 8364: (187-189): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (202-206): Assertion checker does not yet support this expression.
// Warning 8364: (202-204): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (225-227): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (238-242): Assertion checker does not yet support this expression.
// Warning 8364: (238-240): Assertion checker does not yet implement type struct C.S storage ref

8
test/libsolidity/smtCheckerTests/types/struct/struct_recursive_indirect_1.sol
View File

@ -29,11 +29,3 @@ contract C {
// Warning 8364: (171-173): Assertion checker does not yet implement type struct C.S storage ref
// Warning 6328: (125-145): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (149-183): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 7650: (132-136): Assertion checker does not yet support this expression.
// Warning 8364: (132-134): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (140-144): Assertion checker does not yet support this expression.
// Warning 8364: (140-142): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (156-160): Assertion checker does not yet support this expression.
// Warning 8364: (156-158): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (171-175): Assertion checker does not yet support this expression.
// Warning 8364: (171-173): Assertion checker does not yet implement type struct C.S storage ref

32
test/libsolidity/smtCheckerTests/types/struct/struct_recursive_indirect_2.sol
View File

@ -61,35 +61,3 @@ contract C {
// Warning 6368: (215-222): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6368: (215-227): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (190-230): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 7650: (120-124): Assertion checker does not yet support this expression.
// Warning 8364: (120-122): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (120-131): Assertion checker does not yet implement type struct C.T storage ref
// Warning 4375: (120-124): Assertion checker does not support recursive structs.
// Warning 7650: (135-139): Assertion checker does not yet support this expression.
// Warning 8364: (135-137): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (135-146): Assertion checker does not yet implement type struct C.T storage ref
// Warning 4375: (135-139): Assertion checker does not support recursive structs.
// Warning 7650: (150-159): Assertion checker does not yet support this expression.
// Warning 7650: (150-154): Assertion checker does not yet support this expression.
// Warning 8364: (150-152): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (150-157): Assertion checker does not yet implement type struct C.T storage ref
// Warning 8364: (150-166): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (150-159): Assertion checker does not support recursive structs.
// Warning 7650: (170-179): Assertion checker does not yet support this expression.
// Warning 7650: (170-174): Assertion checker does not yet support this expression.
// Warning 8364: (170-172): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (170-177): Assertion checker does not yet implement type struct C.T storage ref
// Warning 8364: (170-186): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4375: (170-179): Assertion checker does not support recursive structs.
// Warning 7650: (197-211): Assertion checker does not yet support this expression.
// Warning 7650: (197-206): Assertion checker does not yet support this expression.
// Warning 7650: (197-201): Assertion checker does not yet support this expression.
// Warning 8364: (197-199): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (197-204): Assertion checker does not yet implement type struct C.T storage ref
// Warning 8364: (197-209): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (215-229): Assertion checker does not yet support this expression.
// Warning 7650: (215-224): Assertion checker does not yet support this expression.
// Warning 7650: (215-219): Assertion checker does not yet support this expression.
// Warning 8364: (215-217): Assertion checker does not yet implement type struct C.S storage ref
// Warning 8364: (215-222): Assertion checker does not yet implement type struct C.T storage ref
// Warning 8364: (215-227): Assertion checker does not yet implement type struct C.S storage ref

2
test/libsolidity/smtCheckerTests/types/type_expression_array_2d.sol
View File

@ -9,5 +9,3 @@ function f() public pure { int[][]; }
// Warning 6133: (41-48): Statement has no effect.
// Warning 8364: (41-46): Assertion checker does not yet implement type type(int256[] memory)
// Warning 8364: (41-48): Assertion checker does not yet implement type type(int256[] memory[] memory)
// Warning 8364: (41-46): Assertion checker does not yet implement type type(int256[] memory)
// Warning 8364: (41-48): Assertion checker does not yet implement type type(int256[] memory[] memory)

3
test/libsolidity/smtCheckerTests/types/type_expression_array_3d.sol
View File

@ -10,6 +10,3 @@ function f() public pure { int[][][]; }
// Warning 8364: (41-46): Assertion checker does not yet implement type type(int256[] memory)
// Warning 8364: (41-48): Assertion checker does not yet implement type type(int256[] memory[] memory)
// Warning 8364: (41-50): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory)
// Warning 8364: (41-46): Assertion checker does not yet implement type type(int256[] memory)
// Warning 8364: (41-48): Assertion checker does not yet implement type type(int256[] memory[] memory)
// Warning 8364: (41-50): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory)

3
test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_2d.sol
View File

@ -10,6 +10,3 @@ function f() public pure { (int[][]); }
// Warning 8364: (42-47): Assertion checker does not yet implement type type(int256[] memory)
// Warning 8364: (42-49): Assertion checker does not yet implement type type(int256[] memory[] memory)
// Warning 8364: (41-50): Assertion checker does not yet implement type type(int256[] memory[] memory)
// Warning 8364: (42-47): Assertion checker does not yet implement type type(int256[] memory)
// Warning 8364: (42-49): Assertion checker does not yet implement type type(int256[] memory[] memory)
// Warning 8364: (41-50): Assertion checker does not yet implement type type(int256[] memory[] memory)

4
test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_3d.sol
View File

@ -11,7 +11,3 @@ function f() public pure { (int[][][]); }
// Warning 8364: (42-49): Assertion checker does not yet implement type type(int256[] memory[] memory)
// Warning 8364: (42-51): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory)
// Warning 8364: (41-52): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory)
// Warning 8364: (42-47): Assertion checker does not yet implement type type(int256[] memory)
// Warning 8364: (42-49): Assertion checker does not yet implement type type(int256[] memory[] memory)
// Warning 8364: (42-51): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory)
// Warning 8364: (41-52): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory)

3
test/libsolidity/smtCheckerTests/types/type_meta_unsupported.sol
View File

@ -17,6 +17,3 @@ contract C {
// Warning 6328: (59-98): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (102-142): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (146-185): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 7507: (72-84): Assertion checker does not yet support this expression.
// Warning 7507: (109-129): Assertion checker does not yet support this expression.
// Warning 7507: (153-172): Assertion checker does not yet support this expression.