From 66125b79d6ffaabaac09add24f11baf2673814f1 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Mon, 23 Nov 2020 15:41:57 +0100 Subject: [PATCH] [SMTChecker] Do not report warning when encountered a Type identifier. The operations are supported now. --- libsolidity/formal/SMTEncoder.cpp | 7 ++----- .../smtCheckerTests/functions/functions_library_1.sol | 2 -- .../smtCheckerTests/functions/functions_library_1_fail.sol | 2 -- .../smtCheckerTests/functions/library_after_contract.sol | 2 -- .../smtCheckerTests/functions/library_constant.sol | 2 -- .../libsolidity/smtCheckerTests/imports/import_library.sol | 2 -- .../operators/function_call_named_arguments.sol | 2 -- .../smtCheckerTests/typecast/enum_from_uint.sol | 2 -- test/libsolidity/smtCheckerTests/typecast/same_size.sol | 2 -- test/libsolidity/smtCheckerTests/typecast/upcast.sol | 2 -- 10 files changed, 2 insertions(+), 23 deletions(-) diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 9a5cce9b3..bbbe1b00d 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -857,11 +857,8 @@ void SMTEncoder::endVisit(Identifier const& _identifier) defineExpr(_identifier, m_context.state().thisAddress()); m_uninterpretedTerms.insert(&_identifier); } - // Ignore struct type identifiers in struct constructor calls - else if ( - auto typetype = dynamic_cast(_identifier.annotation().type); - typetype && typetype->actualType()->category() == Type::Category::Struct - ) + // Ignore type identifiers + else if (dynamic_cast(_identifier.annotation().type)) return; // Ignore the builtin abi, it is handled in FunctionCall. // TODO: ignore MagicType in general (abi, block, msg, tx, type) diff --git a/test/libsolidity/smtCheckerTests/functions/functions_library_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_library_1.sol index 85597b727..ff33b2877 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_library_1.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_library_1.sol @@ -17,5 +17,3 @@ 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 fe671423b..32c18abc6 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol @@ -17,6 +17,4 @@ 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 8eb622caf..0d3efa6f6 100644 --- a/test/libsolidity/smtCheckerTests/functions/library_after_contract.sol +++ b/test/libsolidity/smtCheckerTests/functions/library_after_contract.sol @@ -15,5 +15,3 @@ 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 77c14a79c..e01d32e48 100644 --- a/test/libsolidity/smtCheckerTests/functions/library_constant.sol +++ b/test/libsolidity/smtCheckerTests/functions/library_constant.sol @@ -19,8 +19,6 @@ 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. -// Warning 8364: (300-302): Assertion checker does not yet implement type type(library l1) diff --git a/test/libsolidity/smtCheckerTests/imports/import_library.sol b/test/libsolidity/smtCheckerTests/imports/import_library.sol index 188995fee..a4b2925da 100644 --- a/test/libsolidity/smtCheckerTests/imports/import_library.sol +++ b/test/libsolidity/smtCheckerTests/imports/import_library.sol @@ -15,6 +15,4 @@ 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/operators/function_call_named_arguments.sol b/test/libsolidity/smtCheckerTests/operators/function_call_named_arguments.sol index 5fe62e3ce..d47efe9e3 100644 --- a/test/libsolidity/smtCheckerTests/operators/function_call_named_arguments.sol +++ b/test/libsolidity/smtCheckerTests/operators/function_call_named_arguments.sol @@ -29,6 +29,4 @@ contract C { } } // ---- -// Warning 8364: (360-361): Assertion checker does not yet implement type type(library L) // Warning 6328: (507-521): CHC: Assertion violation happens here. -// Warning 8364: (360-361): Assertion checker does not yet implement type type(library L) diff --git a/test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol b/test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol index a9ece12e5..3ec8c585d 100644 --- a/test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol +++ b/test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol @@ -10,5 +10,3 @@ 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/same_size.sol b/test/libsolidity/smtCheckerTests/typecast/same_size.sol index c4edd7244..940845236 100644 --- a/test/libsolidity/smtCheckerTests/typecast/same_size.sol +++ b/test/libsolidity/smtCheckerTests/typecast/same_size.sol @@ -71,5 +71,3 @@ 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 df9d6e2be..dc5b2f6e0 100644 --- a/test/libsolidity/smtCheckerTests/typecast/upcast.sol +++ b/test/libsolidity/smtCheckerTests/typecast/upcast.sol @@ -67,5 +67,3 @@ 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)