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

Merge pull request #11850 from ethereum/smt_remove_redundant_warnings

Browse Source 
[SMTChecker] Remove redundant unsupported warnings
This commit is contained in:
Leonardo 2021-08-27 17:07:24 +02:00 committed by GitHub
commit ab6b430c1f
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
76 changed files with 142 additions and 432 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
liblangutil/CMakeLists.txt
View File

@ -25,6 +25,7 @@ set(sources
Token.cpp
Token.h
UndefMacros.h
UniqueErrorReporter.h
)
add_library(langutil ${sources})

1
liblangutil/Exceptions.h
View File

@ -105,6 +105,7 @@ struct ErrorId
unsigned long long error = 0;
bool operator==(ErrorId const& _rhs) const { return error == _rhs.error; }
bool operator!=(ErrorId const& _rhs) const { return !(*this == _rhs); }
bool operator<(ErrorId const& _rhs) const { return error < _rhs.error; }
};
constexpr ErrorId operator"" _error(unsigned long long _error) { return ErrorId{ _error }; }

94
liblangutil/UniqueErrorReporter.h Normal file
View File

@ -0,0 +1,94 @@
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#pragma once
#include <liblangutil/ErrorReporter.h>
#include <liblangutil/Exceptions.h>
namespace solidity::langutil
{
/*
* Wrapper for ErrorReporter that removes duplicates.
* Two errors are considered the same if their error ID and location are the same.
*/
class UniqueErrorReporter
{
public:
UniqueErrorReporter(): m_errorReporter(m_uniqueErrors) {}
void warning(ErrorId _error, SourceLocation const& _location, std::string const& _description)
{
if (!seen(_error, _location, _description))
{
m_errorReporter.warning(_error, _location, _description);
markAsSeen(_error, _location, _description);
}
}
void warning(
ErrorId _error,
SourceLocation const& _location,
std::string const& _description,
SecondarySourceLocation const& _secondaryLocation
)
{
if (!seen(_error, _location, _description))
{
m_errorReporter.warning(_error, _location, _description, _secondaryLocation);
markAsSeen(_error, _location, _description);
}
}
void warning(ErrorId _error, std::string const& _description)
{
if (!seen(_error, {}, _description))
{
m_errorReporter.warning(_error, _description);
markAsSeen(_error, {}, _description);
}
}
bool seen(ErrorId _error, SourceLocation const& _location, std::string const& _description) const
{
if (m_seenErrors.count({_error, _location}))
{
solAssert(m_seenErrors.at({_error, _location}) == _description, "");
return true;
}
return false;
}
void markAsSeen(ErrorId _error, SourceLocation const& _location, std::string const& _description)
{
solAssert(!seen(_error, _location, _description), "");
m_seenErrors[{_error, _location}] = _description;
}
ErrorList const& errors() const { return m_errorReporter.errors(); }
void clear() { m_errorReporter.clear(); }
private:
ErrorReporter m_errorReporter;
ErrorList m_uniqueErrors;
std::map<std::pair<ErrorId, SourceLocation>, std::string> m_seenErrors;
};
}

15
libsolidity/formal/BMC.cpp
View File

@ -37,15 +37,14 @@ using namespace solidity::frontend;
BMC::BMC(
smt::EncodingContext& _context,
ErrorReporter& _errorReporter,
UniqueErrorReporter& _errorReporter,
map<h256, string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
ModelCheckerSettings const& _settings,
CharStreamProvider const& _charStreamProvider
):
SMTEncoder(_context, _settings, _charStreamProvider),
m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout)),
m_outerErrorReporter(_errorReporter)
SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider),
m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout))
{
#if defined (HAVE_Z3) || defined (HAVE_CVC4)
if (m_settings.solvers.cvc4 || m_settings.solvers.z3)
@ -67,7 +66,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
if (!m_noSolverWarning)
{
m_noSolverWarning = true;
m_outerErrorReporter.warning(
m_errorReporter.warning(
7710_error,
SourceLocation(),
"BMC analysis was not possible since no SMT solver was found and enabled."
@ -113,7 +112,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
if (!m_noSolverWarning)
{
m_noSolverWarning = true;
m_outerErrorReporter.warning(
m_errorReporter.warning(
8084_error,
SourceLocation(),
"BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available."
@ -124,10 +123,6 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
);
}
}
else
m_outerErrorReporter.append(m_errorReporter.errors());
m_errorReporter.clear();
}
bool BMC::shouldInlineFunctionCall(

7
libsolidity/formal/BMC.h
View File

@ -36,7 +36,7 @@
#include <libsolidity/interface/ReadFile.h>
#include <libsmtutil/SolverInterface.h>
#include <liblangutil/ErrorReporter.h>
#include <liblangutil/UniqueErrorReporter.h>
#include <set>
#include <string>
@ -59,7 +59,7 @@ class BMC: public SMTEncoder
public:
BMC(
smt::EncodingContext& _context,
langutil::ErrorReporter& _errorReporter,
langutil::UniqueErrorReporter& _errorReporter,
std::map<h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
ModelCheckerSettings const& _settings,
@ -186,9 +186,6 @@ private:
bool m_loopExecutionHappened = false;
bool m_externalFunctionCallHappened = false;
/// ErrorReporter that comes from CompilerStack.
langutil::ErrorReporter& m_outerErrorReporter;
std::vector<BMCVerificationTarget> m_verificationTargets;
/// Targets that were already proven.

13
libsolidity/formal/CHC.cpp
View File

@ -53,14 +53,13 @@ using namespace solidity::frontend::smt;
CHC::CHC(
EncodingContext& _context,
ErrorReporter& _errorReporter,
UniqueErrorReporter& _errorReporter,
[[maybe_unused]] map<util::h256, string> const& _smtlib2Responses,
[[maybe_unused]] ReadCallback::Callback const& _smtCallback,
ModelCheckerSettings const& _settings,
CharStreamProvider const& _charStreamProvider
):
SMTEncoder(_context, _settings, _charStreamProvider),
m_outerErrorReporter(_errorReporter)
SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider)
{
bool usesZ3 = m_settings.solvers.z3;
#ifdef HAVE_Z3
@ -79,7 +78,7 @@ void CHC::analyze(SourceUnit const& _source)
if (!m_noSolverWarning)
{
m_noSolverWarning = true;
m_outerErrorReporter.warning(
m_errorReporter.warning(
7649_error,
SourceLocation(),
"CHC analysis was not possible since no Horn solver was enabled."
@ -111,7 +110,7 @@ void CHC::analyze(SourceUnit const& _source)
if (!ranSolver && !m_noSolverWarning)
{
m_noSolverWarning = true;
m_outerErrorReporter.warning(
m_errorReporter.warning(
3996_error,
SourceLocation(),
#ifdef HAVE_Z3_DLOPEN
@ -122,10 +121,6 @@ void CHC::analyze(SourceUnit const& _source)
#endif
);
}
else
m_outerErrorReporter.append(m_errorReporter.errors());
m_errorReporter.clear();
}
vector<string> CHC::unhandledQueries() const

6
libsolidity/formal/CHC.h
View File

@ -40,6 +40,7 @@
#include <libsmtutil/CHCSolverInterface.h>
#include <liblangutil/SourceLocation.h>
#include <liblangutil/UniqueErrorReporter.h>
#include <boost/algorithm/string/join.hpp>
@ -55,7 +56,7 @@ class CHC: public SMTEncoder
public:
CHC(
smt::EncodingContext& _context,
langutil::ErrorReporter& _errorReporter,
langutil::UniqueErrorReporter& _errorReporter,
std::map<util::h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
ModelCheckerSettings const& _settings,
@ -415,9 +416,6 @@ private:
/// CHC solver.
std::unique_ptr<smtutil::CHCSolverInterface> m_interface;
/// ErrorReporter that comes from CompilerStack.
langutil::ErrorReporter& m_outerErrorReporter;
};
}

13
libsolidity/formal/ModelChecker.cpp
View File

@ -40,8 +40,8 @@ ModelChecker::ModelChecker(
m_errorReporter(_errorReporter),
m_settings(move(_settings)),
m_context(),
m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider),
m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider)
m_bmc(m_context, m_uniqueErrorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider),
m_chc(m_context, m_uniqueErrorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider)
{
}
@ -68,7 +68,7 @@ void ModelChecker::checkRequestedSourcesAndContracts(vector<shared_ptr<SourceUni
{
if (!exist.count(sourceName))
{
m_errorReporter.warning(
m_uniqueErrorReporter.warning(
9134_error,
SourceLocation(),
"Requested source \"" + sourceName + "\" does not exist."
@ -79,7 +79,7 @@ void ModelChecker::checkRequestedSourcesAndContracts(vector<shared_ptr<SourceUni
// Requested contracts in source `s`.
for (auto const& contract: m_settings.contracts.contracts.at(sourceName))
if (!source.count(contract))
m_errorReporter.warning(
m_uniqueErrorReporter.warning(
7400_error,
SourceLocation(),
"Requested contract \"" + contract + "\" does not exist in source \"" + sourceName + "\"."
@ -104,7 +104,7 @@ void ModelChecker::analyze(SourceUnit const& _source)
break;
}
solAssert(smtPragma, "");
m_errorReporter.warning(
m_uniqueErrorReporter.warning(
5523_error,
smtPragma->location(),
"The SMTChecker pragma has been deprecated and will be removed in the future. "
@ -125,6 +125,9 @@ void ModelChecker::analyze(SourceUnit const& _source)
if (m_settings.engine.bmc)
m_bmc.analyze(_source, solvedTargets);
m_errorReporter.append(m_uniqueErrorReporter.errors());
m_uniqueErrorReporter.clear();
}
vector<string> ModelChecker::unhandledQueries()

10
libsolidity/formal/ModelChecker.h
View File

@ -31,7 +31,9 @@
#include <libsolidity/interface/ReadFile.h>
#include <libsmtutil/SolverInterface.h>
#include <liblangutil/ErrorReporter.h>
#include <liblangutil/UniqueErrorReporter.h>
namespace solidity::langutil
{
@ -73,8 +75,16 @@ public:
static smtutil::SMTSolverChoice availableSolvers();
private:
/// Error reporter from CompilerStack.
/// We need to append m_uniqueErrorReporter
/// to this one when the analysis is done.
langutil::ErrorReporter& m_errorReporter;
/// Used by ModelChecker, SMTEncoder, BMC and CHC to avoid duplicates.
/// This is local to ModelChecker, so needs to be appended
/// to m_errorReporter at the end of the analysis.
langutil::UniqueErrorReporter m_uniqueErrorReporter;
ModelCheckerSettings m_settings;
/// Stores the context of the encoding.

3
libsolidity/formal/SMTEncoder.cpp
View File

@ -46,9 +46,10 @@ using namespace solidity::frontend;
SMTEncoder::SMTEncoder(
smt::EncodingContext& _context,
ModelCheckerSettings const& _settings,
UniqueErrorReporter& _errorReporter,
langutil::CharStreamProvider const& _charStreamProvider
):
m_errorReporter(m_smtErrors),
m_errorReporter(_errorReporter),
m_context(_context),
m_settings(_settings),
m_charStreamProvider(_charStreamProvider)

9
libsolidity/formal/SMTEncoder.h
View File

@ -32,7 +32,7 @@
#include <libsolidity/ast/AST.h>
#include <libsolidity/ast/ASTVisitor.h>
#include <libsolidity/interface/ReadFile.h>
#include <liblangutil/ErrorReporter.h>
#include <liblangutil/UniqueErrorReporter.h>
#include <string>
#include <unordered_map>
@ -55,6 +55,7 @@ public:
SMTEncoder(
smt::EncodingContext& _context,
ModelCheckerSettings const& _settings,
langutil::UniqueErrorReporter& _errorReporter,
langutil::CharStreamProvider const& _charStreamProvider
);
@ -420,11 +421,7 @@ protected:
/// or unchecked arithmetic.
bool m_checked = true;
/// Local SMTEncoder ErrorReporter.
/// This is necessary to show the "No SMT solver available"
/// warning before the others in case it's needed.
langutil::ErrorReporter m_errorReporter;
langutil::ErrorList m_smtErrors;
langutil::UniqueErrorReporter& m_errorReporter;
/// Stores the current function/modifier call/invocation path.
std::vector<CallStackEntry> m_callStack;

4
test/cmdlineTests/model_checker_solvers_smtlib2/err
View File

@ -1,3 +1,7 @@
Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.
Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.

40
test/cmdlineTests/standard_model_checker_contracts_multi_source/output.json
View File

@ -41,46 +41,6 @@ A.constructor()
A.f(0)","severity":"warning","sourceLocation":{"end":231,"file":"Source","start":218},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
Counterexample:
y = 0
Transaction trace:
A.constructor()
B.g(0)
--> Source:5:7:
|
5 | \t\t\t\t\t\tassert(y > 0);
| \t\t\t\t\t\t^^^^^^^^^^^^^
","message":"CHC: Assertion violation happens here.
Counterexample:
y = 0
Transaction trace:
A.constructor()
B.g(0)","severity":"warning","sourceLocation":{"end":137,"file":"Source","start":124},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
Counterexample:
x = 0
Transaction trace:
A.constructor()
A.f(0)
--> Source:10:7:
|
10 | \t\t\t\t\t\tassert(x > 0);
| \t\t\t\t\t\t^^^^^^^^^^^^^
","message":"CHC: Assertion violation happens here.
Counterexample:
x = 0
Transaction trace:
A.constructor()
A.f(0)","severity":"warning","sourceLocation":{"end":231,"file":"Source","start":218},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
Counterexample:
z = 0
Transaction trace:

8
test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json
View File

@ -145,8 +145,12 @@
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
(=> error_target_3_0 false)))
(check-sat)"}},"errors":[{"component":"general","errorCode":"3996","formattedMessage":"Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.
(check-sat)"}},"errors":[{"component":"general","errorCode":"5840","formattedMessage":"Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
","message":"CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"8084","formattedMessage":"Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.
","message":"CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"3996","formattedMessage":"Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.
","message":"CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"2788","formattedMessage":"Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
","message":"BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"8084","formattedMessage":"Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.
","message":"BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}}

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.