cerc-io/solidity
11
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #10374 from blishko/smtchecker-type-identifiers

Browse Source 
[SMTChecker] Do not report warning when encountered a Type identifier.
This commit is contained in:
Leonardo
2020-11-23 15:54:06 -01:00
committed by GitHub
parent f313668ef1 66125b79d6
commit 243ac16cea
10 changed files with 2 additions and 23 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+2 -5
View File
@@ -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<TypeType const*>(_identifier.annotation().type);
typetype && typetype->actualType()->category() == Type::Category::Struct
)
// Ignore type identifiers
else if (dynamic_cast<TypeType const*>(_identifier.annotation().type))
return;
// Ignore the builtin abi, it is handled in FunctionCall.
// TODO: ignore MagicType in general (abi, block, msg, tx, type)
test/libsolidity/smtCheckerTests/functions/functions_library_1.sol
-2
View File
@@ -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)
test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol
-2
View File
@@ -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)
test/libsolidity/smtCheckerTests/functions/library_after_contract.sol
-2
View File
@@ -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)
test/libsolidity/smtCheckerTests/functions/library_constant.sol
-2
View File
@@ -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)
test/libsolidity/smtCheckerTests/imports/import_library.sol
-2
View File
@@ -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)
test/libsolidity/smtCheckerTests/operators/function_call_named_arguments.sol
-2
View File
@@ -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)
test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol
-2
View File
@@ -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)
test/libsolidity/smtCheckerTests/typecast/same_size.sol
-2
View File
@@ -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)
test/libsolidity/smtCheckerTests/typecast/upcast.sol
-2
View File
@@ -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)