diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 87f5ad1b8..4be4fbd90 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -79,6 +79,24 @@ void CHC::analyze(SourceUnit const& _source) source->accept(*this); checkVerificationTargets(); + + bool ranSolver = true; +#ifndef HAVE_Z3 + ranSolver = dynamic_cast(m_interface.get())->unhandledQueries().empty(); +#endif + if (!ranSolver && !m_noSolverWarning) + { + m_noSolverWarning = true; + m_outerErrorReporter.warning( + 3996_error, + SourceLocation(), + "CHC analysis was not possible since no integrated z3 SMT solver was found." + ); + } + else + m_outerErrorReporter.append(m_errorReporter.errors()); + + m_errorReporter.clear(); } vector CHC::unhandledQueries() const @@ -1076,10 +1094,10 @@ pair CHC::query(smtutil::Expression c case CheckResult::UNKNOWN: break; case CheckResult::CONFLICTING: - m_outerErrorReporter.warning(1988_error, _location, "CHC: At least two SMT solvers provided conflicting answers. Results might not be sound."); + m_errorReporter.warning(1988_error, _location, "CHC: At least two SMT solvers provided conflicting answers. Results might not be sound."); break; case CheckResult::ERROR: - m_outerErrorReporter.warning(1218_error, _location, "CHC: Error trying to invoke SMT solver."); + m_errorReporter.warning(1218_error, _location, "CHC: Error trying to invoke SMT solver."); break; } return {result, cex}; @@ -1233,21 +1251,21 @@ void CHC::checkAndReportTarget( m_unsafeTargets[_target.errorNode].insert(_target.type); auto cex = generateCounterexample(model, error().name); if (cex) - m_outerErrorReporter.warning( + m_errorReporter.warning( _errorReporterId, location, "CHC: " + _satMsg, SecondarySourceLocation().append("Counterexample:\n" + *cex, SourceLocation{}) ); else - m_outerErrorReporter.warning( + m_errorReporter.warning( _errorReporterId, location, "CHC: " + _satMsg ); } else if (!_unknownMsg.empty()) - m_outerErrorReporter.warning( + m_errorReporter.warning( _errorReporterId, location, "CHC: " + _unknownMsg diff --git a/scripts/error_codes.py b/scripts/error_codes.py index ad0374a76..1520b5f4e 100755 --- a/scripts/error_codes.py +++ b/scripts/error_codes.py @@ -223,7 +223,7 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False): "1123", "1133", "1218", "1220", "1584", "1823", "1950", "1988", "2418", "2461", "2512", "2592", "2657", "2800", "2842", "2856", "3046", "3263", "3356", "3441", "3682", "3876", - "3893", "4010", "4281", "4802", "4805", "4828", + "3893", "3996", "4010", "4281", "4802", "4805", "4828", "4904", "4990", "5052", "5073", "5170", "5188", "5272", "5347", "5473", "5622", "6041", "6052", "6084", "6272", "6708", "6792", "6931", "7110", "7128", "7186", "7589", "7593", "7653", "7812", "7885", "8065", "8084", "8140", diff --git a/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol b/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol index fb0f69ddc..187bf87f7 100644 --- a/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol +++ b/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol @@ -36,3 +36,5 @@ library MerkleProof { // ---- // Warning 4588: (988-1032): Assertion checker does not yet implement this type of function call. // Warning 4588: (1175-1219): Assertion checker does not yet implement this type of function call. +// Warning 4588: (988-1032): Assertion checker does not yet implement this type of function call. +// Warning 4588: (1175-1219): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol index c29762706..a31ae955a 100644 --- a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol +++ b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol @@ -84,4 +84,5 @@ contract InternalCall { // Warning 2018: (1212-1274): Function state mutability can be restricted to pure // Warning 2018: (1280-1342): Function state mutability can be restricted to pure // Warning 4588: (771-814): Assertion checker does not yet implement this type of function call. +// Warning 4588: (771-814): Assertion checker does not yet implement this type of function call. // Warning 5729: (1403-1408): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol b/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol index 6f73d845d..f5af0f820 100644 --- a/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol +++ b/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol @@ -11,3 +11,5 @@ contract C { // Warning 2072: (133-143): Unused local variable. // Warning 8364: (146-147): Assertion checker does not yet implement type type(struct C.A storage pointer) // Warning 4639: (146-163): Assertion checker does not yet implement this expression. +// Warning 8364: (146-147): Assertion checker does not yet implement type type(struct C.A storage pointer) +// Warning 4639: (146-163): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/control_flow/try_catch_1.sol b/test/libsolidity/smtCheckerTests/control_flow/try_catch_1.sol index 78cb9264a..921aeea7b 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/try_catch_1.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/try_catch_1.sol @@ -11,3 +11,5 @@ contract C { // Warning 6321: (75-79): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. // Warning 7645: (98-121): Assertion checker does not support try/catch clauses. // Warning 7645: (124-159): Assertion checker does not support try/catch clauses. +// Warning 7645: (98-121): Assertion checker does not support try/catch clauses. +// Warning 7645: (124-159): Assertion checker does not support try/catch clauses. diff --git a/test/libsolidity/smtCheckerTests/control_flow/try_catch_2.sol b/test/libsolidity/smtCheckerTests/control_flow/try_catch_2.sol index dfe2a4428..ed1971b4a 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/try_catch_2.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/try_catch_2.sol @@ -12,3 +12,5 @@ contract C { // ---- // Warning 7645: (83-85): Assertion checker does not support try/catch clauses. // Warning 7645: (88-122): Assertion checker does not support try/catch clauses. +// Warning 7645: (83-85): Assertion checker does not support try/catch clauses. +// Warning 7645: (88-122): Assertion checker does not support try/catch clauses. diff --git a/test/libsolidity/smtCheckerTests/function_selector/function_types_sig.sol b/test/libsolidity/smtCheckerTests/function_selector/function_types_sig.sol index b49c3ac51..2aa2ba857 100644 --- a/test/libsolidity/smtCheckerTests/function_selector/function_types_sig.sol +++ b/test/libsolidity/smtCheckerTests/function_selector/function_types_sig.sol @@ -24,6 +24,8 @@ contract C { } } // ---- +// Warning 6031: (261-267): Internal error: Expression undefined for SMT solver. +// Warning 7650: (284-296): Assertion checker does not yet support this expression. // Warning 6328: (470-495): CHC: Assertion violation happens here. // Warning 6328: (540-565): CHC: Assertion violation happens here. // Warning 6031: (261-267): Internal error: Expression undefined for SMT solver. diff --git a/test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol b/test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol index 2cf037ea5..fb72bd18e 100644 --- a/test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol +++ b/test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol @@ -7,3 +7,5 @@ contract C { // ---- // Warning 4588: (162-176): Assertion checker does not yet implement this type of function call. // Warning 4588: (178-203): Assertion checker does not yet implement this type of function call. +// Warning 4588: (162-176): Assertion checker does not yet implement this type of function call. +// Warning 4588: (178-203): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_library_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_library_1.sol index 04a666219..85597b727 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_library_1.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_library_1.sol @@ -18,3 +18,4 @@ contract C } // ---- // Warning 8364: (228-229): Assertion checker does not yet implement type type(library L) +// Warning 8364: (228-229): Assertion checker does not yet implement type type(library L) diff --git a/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol index c139a2386..fe671423b 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol @@ -17,5 +17,6 @@ contract C } } // ---- +// Warning 8364: (228-229): Assertion checker does not yet implement type type(library L) // Warning 6328: (245-261): CHC: Assertion violation happens here. // Warning 8364: (228-229): Assertion checker does not yet implement type type(library L) diff --git a/test/libsolidity/smtCheckerTests/functions/library_after_contract.sol b/test/libsolidity/smtCheckerTests/functions/library_after_contract.sol index c621041dd..8eb622caf 100644 --- a/test/libsolidity/smtCheckerTests/functions/library_after_contract.sol +++ b/test/libsolidity/smtCheckerTests/functions/library_after_contract.sol @@ -16,3 +16,4 @@ library L { // ---- // Warning 2018: (131-190): Function state mutability can be restricted to pure // Warning 8364: (86-87): Assertion checker does not yet implement type type(library L) +// Warning 8364: (86-87): Assertion checker does not yet implement type type(library L) diff --git a/test/libsolidity/smtCheckerTests/functions/library_constant.sol b/test/libsolidity/smtCheckerTests/functions/library_constant.sol index 301f0a6be..77c14a79c 100644 --- a/test/libsolidity/smtCheckerTests/functions/library_constant.sol +++ b/test/libsolidity/smtCheckerTests/functions/library_constant.sol @@ -19,6 +19,7 @@ contract C { } } // ---- +// Warning 8364: (300-302): Assertion checker does not yet implement type type(library l1) // Warning 6328: (136-155): CHC: Assertion violation happens here. // Warning 4984: (229-234): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 4984: (327-332): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/imports/import_library.sol b/test/libsolidity/smtCheckerTests/imports/import_library.sol index 852eec4f5..188995fee 100644 --- a/test/libsolidity/smtCheckerTests/imports/import_library.sol +++ b/test/libsolidity/smtCheckerTests/imports/import_library.sol @@ -15,5 +15,6 @@ library L { } } // ---- +// Warning 8364: (c:104-105): Assertion checker does not yet implement type type(library L) // Warning 6328: (c:113-126): CHC: Assertion violation happens here. // Warning 8364: (c:104-105): Assertion checker does not yet implement type type(library L) diff --git a/test/libsolidity/smtCheckerTests/inline_assembly/empty.sol b/test/libsolidity/smtCheckerTests/inline_assembly/empty.sol index 607c27bc3..0996e82ba 100644 --- a/test/libsolidity/smtCheckerTests/inline_assembly/empty.sol +++ b/test/libsolidity/smtCheckerTests/inline_assembly/empty.sol @@ -9,3 +9,4 @@ contract C } // ---- // Warning 7737: (76-90): Assertion checker does not support inline assembly. +// Warning 7737: (76-90): Assertion checker does not support inline assembly. diff --git a/test/libsolidity/smtCheckerTests/inline_assembly/local_var.sol b/test/libsolidity/smtCheckerTests/inline_assembly/local_var.sol index d452ca474..a1e3cfff3 100644 --- a/test/libsolidity/smtCheckerTests/inline_assembly/local_var.sol +++ b/test/libsolidity/smtCheckerTests/inline_assembly/local_var.sol @@ -11,3 +11,4 @@ contract C } // ---- // Warning 7737: (97-121): Assertion checker does not support inline assembly. +// Warning 7737: (97-121): Assertion checker does not support inline assembly. diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol index 26d17231e..7249b9e99 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol @@ -12,3 +12,7 @@ contract C { // Warning 8364: (231-237): Assertion checker does not yet implement type type(uint256[] memory) // Warning 8364: (231-240): Assertion checker does not yet implement type type(uint256[] memory[2] memory) // Warning 4588: (202-242): Assertion checker does not yet implement this type of function call. +// Warning 8364: (221-222): Assertion checker does not yet implement type type(struct C.S storage pointer) +// Warning 8364: (231-237): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (231-240): Assertion checker does not yet implement type type(uint256[] memory[2] memory) +// Warning 4588: (202-242): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2_value_types.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2_value_types.sol index 8fa353ec9..8dccd12dc 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2_value_types.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2_value_types.sol @@ -12,6 +12,8 @@ contract C { // ---- // Warning 2072: (122-129): Unused local variable. // Warning 2072: (178-185): Unused local variable. +// Warning 4588: (133-164): Assertion checker does not yet implement this type of function call. +// Warning 4588: (189-220): Assertion checker does not yet implement this type of function call. // Warning 6328: (300-316): CHC: Assertion violation happens here. // Warning 4588: (133-164): Assertion checker does not yet implement this type of function call. // Warning 4588: (189-220): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol index 4ba6b7211..d5ba5789f 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol @@ -13,6 +13,10 @@ contract C { // Warning 2072: (97-101): Unused local variable. // Warning 2072: (156-166): Unused local variable. // Warning 2072: (168-172): Unused local variable. +// Warning 8364: (139-140): Assertion checker does not yet implement type type(contract C) +// Warning 4588: (105-142): Assertion checker does not yet implement this type of function call. +// Warning 8364: (210-211): Assertion checker does not yet implement type type(contract C) +// Warning 4588: (176-213): Assertion checker does not yet implement this type of function call. // Warning 6328: (293-309): CHC: Assertion violation happens here. // Warning 6328: (313-329): CHC: Assertion violation happens here. // Warning 8364: (139-140): Assertion checker does not yet implement type type(contract C) diff --git a/test/libsolidity/smtCheckerTests/special/abi_encode_slice.sol b/test/libsolidity/smtCheckerTests/special/abi_encode_slice.sol index 927ecf631..b56c7780a 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_encode_slice.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_encode_slice.sol @@ -6,3 +6,4 @@ contract C { } // ---- // Warning 4588: (126-154): Assertion checker does not yet implement this type of function call. +// Warning 4588: (126-154): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol b/test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol index f14156bde..a9ece12e5 100644 --- a/test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol +++ b/test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol @@ -11,3 +11,4 @@ contract C } // ---- // Warning 8364: (132-133): Assertion checker does not yet implement type type(enum C.D) +// Warning 8364: (132-133): Assertion checker does not yet implement type type(enum C.D) diff --git a/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol b/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol index 4680d5367..f462ae78a 100644 --- a/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol +++ b/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol @@ -12,6 +12,9 @@ contract C { } // ---- // Warning 2519: (128-159): This declaration shadows an existing declaration. +// Warning 6031: (214-218): Internal error: Expression undefined for SMT solver. +// Warning 6031: (222-226): Internal error: Expression undefined for SMT solver. +// Warning 7229: (238-244): Assertion checker does not yet implement the type function (uint256) returns (uint256) for comparisons // Warning 6328: (207-227): CHC: Assertion violation happens here. // Warning 6328: (231-245): CHC: Assertion violation happens here. // Warning 5729: (214-218): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/typecast/same_size.sol b/test/libsolidity/smtCheckerTests/typecast/same_size.sol index 4d5bed1a1..c4edd7244 100644 --- a/test/libsolidity/smtCheckerTests/typecast/same_size.sol +++ b/test/libsolidity/smtCheckerTests/typecast/same_size.sol @@ -72,3 +72,4 @@ contract C { } // ---- // Warning 8364: (1304-1305): Assertion checker does not yet implement type type(enum E) +// Warning 8364: (1304-1305): Assertion checker does not yet implement type type(enum E) diff --git a/test/libsolidity/smtCheckerTests/typecast/upcast.sol b/test/libsolidity/smtCheckerTests/typecast/upcast.sol index 8ad35a7d5..df9d6e2be 100644 --- a/test/libsolidity/smtCheckerTests/typecast/upcast.sol +++ b/test/libsolidity/smtCheckerTests/typecast/upcast.sol @@ -68,3 +68,4 @@ contract C { } // ---- // Warning 8364: (1144-1145): Assertion checker does not yet implement type type(contract D) +// Warning 8364: (1144-1145): Assertion checker does not yet implement type type(contract D) diff --git a/test/libsolidity/smtCheckerTests/types/function_type_external_address.sol b/test/libsolidity/smtCheckerTests/types/function_type_external_address.sol index 286ee451b..07bcce0a8 100644 --- a/test/libsolidity/smtCheckerTests/types/function_type_external_address.sol +++ b/test/libsolidity/smtCheckerTests/types/function_type_external_address.sol @@ -7,3 +7,4 @@ contract C { } // ---- // Warning 7650: (128-137): Assertion checker does not yet support this expression. +// Warning 7650: (128-137): Assertion checker does not yet support this expression. diff --git a/test/libsolidity/smtCheckerTests/types/function_type_members.sol b/test/libsolidity/smtCheckerTests/types/function_type_members.sol index 7b9a0f44d..b5f825b2b 100644 --- a/test/libsolidity/smtCheckerTests/types/function_type_members.sol +++ b/test/libsolidity/smtCheckerTests/types/function_type_members.sol @@ -7,3 +7,4 @@ contract C { } // ---- // Warning 7650: (108-118): Assertion checker does not yet support this expression. +// Warning 7650: (108-118): Assertion checker does not yet support this expression. diff --git a/test/libsolidity/smtCheckerTests/types/function_type_nested.sol b/test/libsolidity/smtCheckerTests/types/function_type_nested.sol index 2b6a0e538..8d61acf6e 100644 --- a/test/libsolidity/smtCheckerTests/types/function_type_nested.sol +++ b/test/libsolidity/smtCheckerTests/types/function_type_nested.sol @@ -12,6 +12,10 @@ contract C { } } // ---- +// Warning 8115: (152-197): Assertion checker does not yet support the type of this variable. +// Warning 8364: (212-214): Assertion checker does not yet implement type function (function (uint256)) +// Warning 6031: (255-257): Internal error: Expression undefined for SMT solver. +// Warning 8364: (255-257): Assertion checker does not yet implement type function (function (uint256)) // Warning 5729: (123-128): Assertion checker does not yet implement this type of function call. // Warning 8115: (152-197): Assertion checker does not yet support the type of this variable. // Warning 8364: (212-214): Assertion checker does not yet implement type function (function (uint256)) diff --git a/test/libsolidity/smtCheckerTests/types/function_type_nested_return.sol b/test/libsolidity/smtCheckerTests/types/function_type_nested_return.sol index 65f321656..ec4dff520 100644 --- a/test/libsolidity/smtCheckerTests/types/function_type_nested_return.sol +++ b/test/libsolidity/smtCheckerTests/types/function_type_nested_return.sol @@ -15,6 +15,11 @@ contract C { } } // ---- +// Warning 8115: (224-269): Assertion checker does not yet support the type of this variable. +// Warning 8364: (284-286): Assertion checker does not yet implement type function (function (uint256)) +// Warning 1695: (287-288): Assertion checker does not yet support this global variable. +// Warning 6031: (327-329): Internal error: Expression undefined for SMT solver. +// Warning 8364: (327-329): Assertion checker does not yet implement type function (function (uint256)) // Warning 5729: (195-200): Assertion checker does not yet implement this type of function call. // Warning 8115: (224-269): Assertion checker does not yet support the type of this variable. // Warning 8364: (284-286): Assertion checker does not yet implement type function (function (uint256)) diff --git a/test/libsolidity/smtCheckerTests/types/mapping_struct_assignment.sol b/test/libsolidity/smtCheckerTests/types/mapping_struct_assignment.sol index fa2c2d10d..33c3ded48 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_struct_assignment.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_struct_assignment.sol @@ -11,6 +11,8 @@ contract C } } // ---- +// Warning 8364: (159-160): Assertion checker does not yet implement type type(struct C.S storage pointer) +// Warning 4639: (159-163): Assertion checker does not yet implement this expression. // Warning 6838: (140-144): BMC: Condition is always false. // Warning 8364: (159-160): Assertion checker does not yet implement type type(struct C.S storage pointer) // Warning 4639: (159-163): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/types/no_effect_statements.sol b/test/libsolidity/smtCheckerTests/types/no_effect_statements.sol index 742a2fe67..a5f78824c 100644 --- a/test/libsolidity/smtCheckerTests/types/no_effect_statements.sol +++ b/test/libsolidity/smtCheckerTests/types/no_effect_statements.sol @@ -22,3 +22,9 @@ contract test { // Warning 8364: (140-141): Assertion checker does not yet implement type type(struct test.s storage pointer) // Warning 8364: (140-144): Assertion checker does not yet implement type type(struct test.s memory[7] memory) // Warning 8364: (156-163): Assertion checker does not yet implement type type(uint256[7] memory) +// Warning 8364: (125-126): Assertion checker does not yet implement type type(struct test.s storage pointer) +// Warning 8364: (130-131): Assertion checker does not yet implement type type(struct test.s storage pointer) +// Warning 4639: (130-136): Assertion checker does not yet implement this expression. +// Warning 8364: (140-141): Assertion checker does not yet implement type type(struct test.s storage pointer) +// Warning 8364: (140-144): Assertion checker does not yet implement type type(struct test.s memory[7] memory) +// Warning 8364: (156-163): Assertion checker does not yet implement type type(uint256[7] memory) diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_1.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_1.sol index a9fe81ba1..86190683c 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_1.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_1.sol @@ -13,6 +13,16 @@ contract C { } } // ---- +// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable. +// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable. +// Warning 7650: (131-135): Assertion checker does not yet support this expression. +// Warning 8364: (131-133): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (139-143): Assertion checker does not yet support this expression. +// Warning 8364: (139-141): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (155-159): Assertion checker does not yet support this expression. +// Warning 8364: (155-157): Assertion checker does not yet implement type struct C.S storage ref +// 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 6328: (124-144): CHC: Assertion violation happens here. // Warning 6328: (148-182): CHC: Assertion violation happens here. // Warning 8115: (81-85): Assertion checker does not yet support the type of this variable. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_2.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_2.sol index 56b117415..28265eef5 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_2.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_2.sol @@ -22,6 +22,48 @@ contract C { } } // ---- +// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable. +// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable. +// Warning 7650: (131-135): Assertion checker does not yet support this expression. +// Warning 8364: (131-133): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (139-143): Assertion checker does not yet support this expression. +// Warning 8364: (139-141): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (155-159): Assertion checker does not yet support this expression. +// Warning 8364: (155-157): Assertion checker does not yet implement type struct C.S storage ref +// 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 7650: (193-202): Assertion checker does not yet support this expression. +// Warning 7650: (193-197): Assertion checker does not yet support this expression. +// Warning 8364: (193-195): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (193-200): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (206-215): Assertion checker does not yet support this expression. +// Warning 7650: (206-210): Assertion checker does not yet support this expression. +// Warning 8364: (206-208): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (206-213): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (246-250): Assertion checker does not yet support this expression. +// Warning 8364: (246-248): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (246-250): Assertion checker does not support recursive structs. +// Warning 7650: (259-263): Assertion checker does not yet support this expression. +// Warning 8364: (259-261): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (259-263): Assertion checker does not support recursive structs. +// Warning 7650: (272-276): Assertion checker does not yet support this expression. +// Warning 8364: (272-274): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (272-283): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (272-276): Assertion checker does not support recursive structs. +// 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-298): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (287-291): Assertion checker does not support recursive structs. +// Warning 7650: (302-311): Assertion checker does not yet support this expression. +// Warning 7650: (302-306): Assertion checker does not yet support this expression. +// Warning 8364: (302-304): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (302-309): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (302-311): Assertion checker does not support recursive structs. +// Warning 7650: (320-329): Assertion checker does not yet support this expression. +// Warning 7650: (320-324): Assertion checker does not yet support this expression. +// Warning 8364: (320-322): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (320-327): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (320-329): Assertion checker does not support recursive structs. // Warning 6328: (124-144): CHC: Assertion violation happens here. // Warning 6328: (148-182): CHC: Assertion violation happens here. // Warning 6328: (186-216): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_3.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_3.sol index cbb608dec..6971aaa40 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_3.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_3.sol @@ -28,6 +28,94 @@ contract C { } } // ---- +// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable. +// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable. +// Warning 7650: (131-135): Assertion checker does not yet support this expression. +// Warning 8364: (131-133): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (139-143): Assertion checker does not yet support this expression. +// Warning 8364: (139-141): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (155-159): Assertion checker does not yet support this expression. +// Warning 8364: (155-157): Assertion checker does not yet implement type struct C.S storage ref +// 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 7650: (193-202): Assertion checker does not yet support this expression. +// Warning 7650: (193-197): Assertion checker does not yet support this expression. +// Warning 8364: (193-195): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (193-200): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (206-215): Assertion checker does not yet support this expression. +// Warning 7650: (206-210): Assertion checker does not yet support this expression. +// Warning 8364: (206-208): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (206-213): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (227-236): Assertion checker does not yet support this expression. +// 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 ref +// Warning 8364: (227-234): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (247-256): Assertion checker does not yet support this expression. +// Warning 7650: (247-251): Assertion checker does not yet support this expression. +// Warning 8364: (247-249): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (247-254): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (275-289): Assertion checker does not yet support this expression. +// Warning 7650: (275-284): Assertion checker does not yet support this expression. +// Warning 7650: (275-279): Assertion checker does not yet support this expression. +// Warning 8364: (275-277): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (275-282): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (275-287): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (293-307): Assertion checker does not yet support this expression. +// Warning 7650: (293-302): Assertion checker does not yet support this expression. +// Warning 7650: (293-297): Assertion checker does not yet support this expression. +// Warning 8364: (293-295): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (293-300): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (293-305): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (338-342): Assertion checker does not yet support this expression. +// Warning 8364: (338-340): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (338-342): Assertion checker does not support recursive structs. +// Warning 7650: (351-355): Assertion checker does not yet support this expression. +// Warning 8364: (351-353): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (351-355): Assertion checker does not support recursive structs. +// Warning 7650: (364-368): Assertion checker does not yet support this expression. +// Warning 8364: (364-366): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (364-375): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (364-368): Assertion checker does not support recursive structs. +// Warning 7650: (379-383): Assertion checker does not yet support this expression. +// Warning 8364: (379-381): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (379-390): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (379-383): Assertion checker does not support recursive structs. +// Warning 7650: (394-403): Assertion checker does not yet support this expression. +// Warning 7650: (394-398): Assertion checker does not yet support this expression. +// Warning 8364: (394-396): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (394-401): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (394-403): Assertion checker does not support recursive structs. +// Warning 7650: (412-421): Assertion checker does not yet support this expression. +// Warning 7650: (412-416): Assertion checker does not yet support this expression. +// Warning 8364: (412-414): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (412-419): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (412-421): Assertion checker does not support recursive structs. +// Warning 7650: (430-439): Assertion checker does not yet support this expression. +// Warning 7650: (430-434): Assertion checker does not yet support this expression. +// Warning 8364: (430-432): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (430-437): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (430-446): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (430-439): Assertion checker does not support recursive structs. +// Warning 7650: (450-459): Assertion checker does not yet support this expression. +// Warning 7650: (450-454): Assertion checker does not yet support this expression. +// Warning 8364: (450-452): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (450-457): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (450-466): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (450-459): Assertion checker does not support recursive structs. +// Warning 7650: (470-484): Assertion checker does not yet support this expression. +// Warning 7650: (470-479): Assertion checker does not yet support this expression. +// Warning 7650: (470-474): Assertion checker does not yet support this expression. +// Warning 8364: (470-472): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (470-477): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (470-482): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (470-484): Assertion checker does not support recursive structs. +// Warning 7650: (493-507): Assertion checker does not yet support this expression. +// Warning 7650: (493-502): Assertion checker does not yet support this expression. +// Warning 7650: (493-497): Assertion checker does not yet support this expression. +// Warning 8364: (493-495): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (493-500): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (493-505): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (493-507): Assertion checker does not support recursive structs. // Warning 6328: (124-144): CHC: Assertion violation happens here. // Warning 6328: (148-182): CHC: Assertion violation happens here. // Warning 6328: (186-216): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_4.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_4.sol index 18ec01049..cef0fa89c 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_4.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_4.sol @@ -18,6 +18,39 @@ contract C { } } // ---- +// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable. +// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable. +// Warning 8115: (135-147): Assertion checker does not yet support the type of this variable. +// Warning 8115: (166-178): Assertion checker does not yet support the type of this variable. +// Warning 8364: (155-157): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (160-162): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (150-162): Assertion checker does not yet implement type struct C.S storage pointer +// Warning 8364: (186-188): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (191-193): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (181-193): Assertion checker does not yet implement type struct C.S storage pointer +// Warning 7650: (204-208): Assertion checker does not yet support this expression. +// Warning 8364: (204-206): Assertion checker does not yet implement type struct C.S storage pointer +// Warning 7650: (212-216): Assertion checker does not yet support this expression. +// Warning 8364: (212-214): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (220-224): Assertion checker does not yet support this expression. +// Warning 8364: (220-222): Assertion checker does not yet implement type struct C.S storage pointer +// Warning 7650: (228-232): Assertion checker does not yet support this expression. +// Warning 8364: (228-230): 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 7650: (252-256): Assertion checker does not yet support this expression. +// Warning 8364: (252-254): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (260-264): Assertion checker does not yet support this expression. +// Warning 8364: (260-262): Assertion checker does not yet implement type struct C.S storage pointer +// Warning 7650: (268-272): Assertion checker does not yet support this expression. +// Warning 8364: (268-270): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (277-281): Assertion checker does not yet support this expression. +// Warning 8364: (277-279): Assertion checker does not yet implement type struct C.S storage pointer +// Warning 4375: (277-281): Assertion checker does not support recursive structs. +// Warning 7650: (366-370): Assertion checker does not yet support this expression. +// Warning 8364: (366-368): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (380-384): Assertion checker does not yet support this expression. +// Warning 8364: (380-382): Assertion checker does not yet implement type struct C.S storage ref // Warning 6328: (197-233): CHC: Assertion violation happens here. // Warning 6328: (237-273): CHC: Assertion violation happens here. // Warning 6328: (359-391): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_5.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_5.sol index e86747344..a8e621e4a 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_5.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_5.sol @@ -16,6 +16,16 @@ contract C { } } // ---- +// Warning 8364: (126-135): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (153-166): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (170-181): Assertion checker does not yet support this expression. +// Warning 8364: (170-179): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (170-188): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (170-181): Assertion checker does not support recursive structs. +// Warning 7650: (199-210): Assertion checker does not yet support this expression. +// Warning 8364: (199-208): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (221-228): Assertion checker does not yet support this expression. +// Warning 8364: (221-226): Assertion checker does not yet implement type struct C.S storage ref // Warning 6328: (192-236): CHC: Assertion violation happens here. // Warning 8364: (126-135): Assertion checker does not yet implement type struct C.S storage ref // Warning 8364: (153-166): Assertion checker does not yet implement type struct C.S storage ref diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_6.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_6.sol index 3999a4394..e4aab975c 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_6.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_6.sol @@ -21,6 +21,37 @@ contract C { } } // ---- +// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable. +// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable. +// 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: (152-156): Assertion checker does not yet support this expression. +// Warning 8364: (152-154): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (152-156): Assertion checker does not support recursive structs. +// 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 4375: (167-171): Assertion checker does not support recursive structs. +// Warning 7650: (175-179): Assertion checker does not yet support this expression. +// Warning 8364: (175-177): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (175-179): Assertion checker does not support recursive structs. +// Warning 7650: (192-196): Assertion checker does not yet support this expression. +// Warning 8364: (192-194): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (200-204): Assertion checker does not yet support this expression. +// Warning 8364: (200-202): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (220-224): Assertion checker does not yet support this expression. +// Warning 8364: (220-222): Assertion checker does not yet implement type struct C.S storage ref +// 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 8364: (258-260): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (271-275): Assertion checker does not yet support this expression. +// Warning 8364: (271-273): Assertion checker does not yet implement type struct C.S storage ref // Warning 4984: (200-208): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 6328: (185-209): CHC: Assertion violation happens here. // Warning 6328: (213-247): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_indirect_1.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_indirect_1.sol index 4bb810ec9..ecab74c2a 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_indirect_1.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_indirect_1.sol @@ -17,6 +17,16 @@ contract C { } } // ---- +// Warning 8115: (115-119): Assertion checker does not yet support the type of this variable. +// Warning 8115: (122-126): Assertion checker does not yet support the type of this variable. +// Warning 7650: (165-169): Assertion checker does not yet support this expression. +// Warning 8364: (165-167): Assertion checker does not yet implement type struct C.S storage ref +// 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 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: (204-208): Assertion checker does not yet support this expression. +// Warning 8364: (204-206): Assertion checker does not yet implement type struct C.S storage ref // Warning 6328: (158-178): CHC: Assertion violation happens here. // Warning 6328: (182-216): CHC: Assertion violation happens here. // Warning 8115: (115-119): Assertion checker does not yet support the type of this variable. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_indirect_2.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_indirect_2.sol index ceb704bdd..49de04be5 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_indirect_2.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_indirect_2.sol @@ -20,6 +20,40 @@ contract C { } } // ---- +// Warning 8115: (115-119): Assertion checker does not yet support the type of this variable. +// Warning 8115: (122-126): Assertion checker does not yet support the type of this variable. +// Warning 7650: (153-157): Assertion checker does not yet support this expression. +// Warning 8364: (153-155): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (153-164): Assertion checker does not yet implement type struct C.T storage ref +// Warning 4375: (153-157): Assertion checker does not support recursive structs. +// Warning 7650: (168-172): Assertion checker does not yet support this expression. +// Warning 8364: (168-170): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (168-179): Assertion checker does not yet implement type struct C.T storage ref +// Warning 4375: (168-172): Assertion checker does not support recursive structs. +// Warning 7650: (183-192): Assertion checker does not yet support this expression. +// Warning 7650: (183-187): Assertion checker does not yet support this expression. +// Warning 8364: (183-185): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (183-190): Assertion checker does not yet implement type struct C.T storage ref +// Warning 8364: (183-199): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (183-192): Assertion checker does not support recursive structs. +// Warning 7650: (203-212): Assertion checker does not yet support this expression. +// Warning 7650: (203-207): Assertion checker does not yet support this expression. +// Warning 8364: (203-205): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (203-210): Assertion checker does not yet implement type struct C.T storage ref +// Warning 8364: (203-219): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (203-212): Assertion checker does not support recursive structs. +// Warning 7650: (230-244): Assertion checker does not yet support this expression. +// Warning 7650: (230-239): Assertion checker does not yet support this expression. +// Warning 7650: (230-234): Assertion checker does not yet support this expression. +// Warning 8364: (230-232): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (230-237): Assertion checker does not yet implement type struct C.T storage ref +// Warning 8364: (230-242): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (248-262): Assertion checker does not yet support this expression. +// Warning 7650: (248-257): Assertion checker does not yet support this expression. +// Warning 7650: (248-252): Assertion checker does not yet support this expression. +// Warning 8364: (248-250): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (248-255): Assertion checker does not yet implement type struct C.T storage ref +// Warning 8364: (248-260): Assertion checker does not yet implement type struct C.S storage ref // Warning 6328: (223-263): CHC: Assertion violation happens here. // Warning 8115: (115-119): Assertion checker does not yet support the type of this variable. // Warning 8115: (122-126): Assertion checker does not yet support the type of this variable. diff --git a/test/libsolidity/smtCheckerTests/types/struct_1.sol b/test/libsolidity/smtCheckerTests/types/struct_1.sol index 99dc2b149..d8152d6e0 100644 --- a/test/libsolidity/smtCheckerTests/types/struct_1.sol +++ b/test/libsolidity/smtCheckerTests/types/struct_1.sol @@ -19,3 +19,7 @@ contract C // Warning 4639: (149-153): Assertion checker does not yet implement this expression. // Warning 8364: (173-174): Assertion checker does not yet implement type type(struct C.S storage pointer) // Warning 4639: (173-177): Assertion checker does not yet implement this expression. +// Warning 8364: (149-150): Assertion checker does not yet implement type type(struct C.S storage pointer) +// Warning 4639: (149-153): Assertion checker does not yet implement this expression. +// Warning 8364: (173-174): Assertion checker does not yet implement type type(struct C.S storage pointer) +// Warning 4639: (173-177): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol b/test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol index 3ed532ccb..3d3336eb1 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol @@ -16,4 +16,6 @@ contract C { // ---- // Warning 8364: (137-138): Assertion checker does not yet implement type type(struct C.S storage pointer) // Warning 4639: (137-141): Assertion checker does not yet implement this expression. +// Warning 8364: (137-138): Assertion checker does not yet implement type type(struct C.S storage pointer) +// Warning 4639: (137-141): Assertion checker does not yet implement this expression. // Warning 4639: (137-141): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/types/type_expression_array_2d.sol b/test/libsolidity/smtCheckerTests/types/type_expression_array_2d.sol index d98fc7b5c..22f6c9c07 100644 --- a/test/libsolidity/smtCheckerTests/types/type_expression_array_2d.sol +++ b/test/libsolidity/smtCheckerTests/types/type_expression_array_2d.sol @@ -8,3 +8,5 @@ function f() public pure { int[][]; } // Warning 6133: (73-80): Statement has no effect. // Warning 8364: (73-78): Assertion checker does not yet implement type type(int256[] memory) // Warning 8364: (73-80): Assertion checker does not yet implement type type(int256[] memory[] memory) +// Warning 8364: (73-78): Assertion checker does not yet implement type type(int256[] memory) +// Warning 8364: (73-80): Assertion checker does not yet implement type type(int256[] memory[] memory) diff --git a/test/libsolidity/smtCheckerTests/types/type_expression_array_3d.sol b/test/libsolidity/smtCheckerTests/types/type_expression_array_3d.sol index 1bd311897..51869fb3f 100644 --- a/test/libsolidity/smtCheckerTests/types/type_expression_array_3d.sol +++ b/test/libsolidity/smtCheckerTests/types/type_expression_array_3d.sol @@ -9,3 +9,6 @@ function f() public pure { int[][][]; } // Warning 8364: (73-78): Assertion checker does not yet implement type type(int256[] memory) // Warning 8364: (73-80): Assertion checker does not yet implement type type(int256[] memory[] memory) // Warning 8364: (73-82): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory) +// Warning 8364: (73-78): Assertion checker does not yet implement type type(int256[] memory) +// Warning 8364: (73-80): Assertion checker does not yet implement type type(int256[] memory[] memory) +// Warning 8364: (73-82): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory) diff --git a/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_2d.sol b/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_2d.sol index b653f8415..b34dd2a56 100644 --- a/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_2d.sol +++ b/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_2d.sol @@ -9,3 +9,6 @@ function f() public pure { (int[][]); } // Warning 8364: (74-79): Assertion checker does not yet implement type type(int256[] memory) // Warning 8364: (74-81): Assertion checker does not yet implement type type(int256[] memory[] memory) // Warning 8364: (73-82): Assertion checker does not yet implement type type(int256[] memory[] memory) +// Warning 8364: (74-79): Assertion checker does not yet implement type type(int256[] memory) +// Warning 8364: (74-81): Assertion checker does not yet implement type type(int256[] memory[] memory) +// Warning 8364: (73-82): Assertion checker does not yet implement type type(int256[] memory[] memory) diff --git a/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_3d.sol b/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_3d.sol index 524b59ace..dfa4a4661 100644 --- a/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_3d.sol +++ b/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_3d.sol @@ -10,3 +10,7 @@ function f() public pure { (int[][][]); } // Warning 8364: (74-81): Assertion checker does not yet implement type type(int256[] memory[] memory) // Warning 8364: (74-83): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory) // Warning 8364: (73-84): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory) +// Warning 8364: (74-79): Assertion checker does not yet implement type type(int256[] memory) +// Warning 8364: (74-81): Assertion checker does not yet implement type type(int256[] memory[] memory) +// Warning 8364: (74-83): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory) +// Warning 8364: (73-84): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory) diff --git a/test/libsolidity/smtCheckerTests/types/type_meta_unsupported.sol b/test/libsolidity/smtCheckerTests/types/type_meta_unsupported.sol index e9319b2d1..71b2c01ed 100644 --- a/test/libsolidity/smtCheckerTests/types/type_meta_unsupported.sol +++ b/test/libsolidity/smtCheckerTests/types/type_meta_unsupported.sol @@ -11,6 +11,9 @@ contract C { } } // ---- +// Warning 7507: (105-117): Assertion checker does not yet support this expression. +// Warning 7507: (142-162): Assertion checker does not yet support this expression. +// Warning 7507: (186-205): Assertion checker does not yet support this expression. // Warning 6328: (92-131): CHC: Assertion violation happens here. // Warning 6328: (135-175): CHC: Assertion violation happens here. // Warning 6328: (179-218): CHC: Assertion violation happens here.