diff --git a/Changelog.md b/Changelog.md index 3546a754f..09ef7db60 100644 --- a/Changelog.md +++ b/Changelog.md @@ -9,6 +9,7 @@ Compiler Features: * Yul EVM Code Transform: Also pop unused argument slots for functions without return variables (under the same restrictions as for functions with return variables). * Yul Optimizer: Move function arguments and return variables to memory with the experimental Stack Limit Evader (which is not enabled by default). * Commandline Interface: option ``--pretty-json`` works also with ``--standard--json``. + * SMTChecker: Unproved targets are hidden by default, and the SMTChecker only states how many unproved targets there are. They can be listed using the command line option ``--model-checker-show-unproved`` or the JSON option ``settings.modelChecker.showUnproved``. Bugfixes: diff --git a/docs/smtchecker.rst b/docs/smtchecker.rst index 685f5e9fc..e2b61cf35 100644 --- a/docs/smtchecker.rst +++ b/docs/smtchecker.rst @@ -474,6 +474,14 @@ A common subset of targets might be, for example: There is no precise heuristic on how and when to split verification targets, but it can be useful especially when dealing with large contracts. +Unproved Targets +================ + +If there are any unproved targets, the SMTChecker issues one warning stating +how many unproved targets there are. If the user wishes to see all the specific +unproved targets, the CLI option ``--model-checker-show-unproved true`` and +the JSON option ``settings.modelChecker.showUnproved = true`` can be used. + Verified Contracts ================== diff --git a/docs/using-the-compiler.rst b/docs/using-the-compiler.rst index 9ae6b15c9..381f150cd 100644 --- a/docs/using-the-compiler.rst +++ b/docs/using-the-compiler.rst @@ -402,6 +402,8 @@ Input Description }, // Choose which model checker engine to use: all (default), bmc, chc, none. "engine": "chc", + // Choose whether to output all unproved targets. The default is `false`. + "showUnproved": true, // Choose which targets should be checked: constantCondition, // underflow, overflow, divByZero, balance, assert, popEmptyArray, outOfBounds. // If the option is not given all targets are checked by default. diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index eee9988ed..2676dffaa 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -60,7 +60,7 @@ BMC::BMC( #endif } -void BMC::analyze(SourceUnit const& _source, map> _solvedTargets) +void BMC::analyze(SourceUnit const& _source, map, smt::EncodingContext::IdCompare> _solvedTargets) { if (m_interface->solvers() == 0) { @@ -84,8 +84,21 @@ void BMC::analyze(SourceUnit const& _source, map 0 && !m_settings.showUnproved) + m_errorReporter.warning( + 2788_error, + {}, + "BMC: " + + to_string(m_unprovedAmt) + + " 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." + ); } // If this check is true, Z3 and CVC4 are not available @@ -961,8 +974,12 @@ void BMC::checkCondition( case smtutil::CheckResult::UNSATISFIABLE: break; case smtutil::CheckResult::UNKNOWN: - m_errorReporter.warning(_errorMightHappen, _location, "BMC: " + _description + " might happen here.", secondaryLocation); + { + ++m_unprovedAmt; + if (m_settings.showUnproved) + m_errorReporter.warning(_errorMightHappen, _location, "BMC: " + _description + " might happen here.", secondaryLocation); break; + } case smtutil::CheckResult::CONFLICTING: m_errorReporter.warning(1584_error, _location, "BMC: At least two SMT solvers provided conflicting answers. Results might not be sound."); break; diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index c1b89347c..a256dbf09 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -66,7 +66,7 @@ public: langutil::CharStreamProvider const& _charStreamProvider ); - void analyze(SourceUnit const& _sources, std::map> _solvedTargets); + void analyze(SourceUnit const& _sources, std::map, smt::EncodingContext::IdCompare> _solvedTargets); /// This is used if the SMT solver is not directly linked into this binary. /// @returns a list of inputs to the SMT solver that were not part of the argument to @@ -192,7 +192,10 @@ private: std::vector m_verificationTargets; /// Targets that were already proven. - std::map> m_solvedTargets; + std::map, smt::EncodingContext::IdCompare> m_solvedTargets; + + /// Number of verification conditions that could not be proved. + size_t m_unprovedAmt = 0; }; } diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 00657922d..7cc963956 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -933,6 +933,7 @@ void CHC::resetSourceAnalysis() { m_safeTargets.clear(); m_unsafeTargets.clear(); + m_unprovedTargets.clear(); m_functionTargetIds.clear(); m_verificationTargets.clear(); m_queryPlaceholders.clear(); @@ -1594,6 +1595,32 @@ void CHC::checkVerificationTargets() checkedErrorIds.insert(target.errorId); } + auto toReport = m_unsafeTargets; + if (m_settings.showUnproved) + for (auto const& [node, targets]: m_unprovedTargets) + for (auto const& [target, info]: targets) + toReport[node].emplace(target, info); + + for (auto const& [node, targets]: toReport) + for (auto const& [target, info]: targets) + m_errorReporter.warning( + info.error, + info.location, + info.message + ); + + if (!m_settings.showUnproved && !m_unprovedTargets.empty()) + m_errorReporter.warning( + 5840_error, + {}, + "CHC: " + + to_string(m_unprovedTargets.size()) + + " 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." + ); + // There can be targets in internal functions that are not reachable from the external interface. // These are safe by definition and are not even checked by the CHC engine, but this information // must still be reported safe by the BMC engine. @@ -1633,27 +1660,26 @@ void CHC::checkAndReportTarget( else if (result == CheckResult::SATISFIABLE) { solAssert(!_satMsg.empty(), ""); - m_unsafeTargets[_target.errorNode].insert(_target.type); auto cex = generateCounterexample(model, error().name); if (cex) - m_errorReporter.warning( + m_unsafeTargets[_target.errorNode][_target.type] = { _errorReporterId, location, "CHC: " + _satMsg + "\nCounterexample:\n" + *cex - ); + }; else - m_errorReporter.warning( + m_unsafeTargets[_target.errorNode][_target.type] = { _errorReporterId, location, "CHC: " + _satMsg - ); + }; } else if (!_unknownMsg.empty()) - m_errorReporter.warning( + m_unprovedTargets[_target.errorNode][_target.type] = { _errorReporterId, location, "CHC: " + _unknownMsg - ); + }; } /** diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 3aab9268d..f2e8f62a1 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -39,6 +39,8 @@ #include +#include + #include #include @@ -62,8 +64,14 @@ public: void analyze(SourceUnit const& _sources); - std::map> const& safeTargets() const { return m_safeTargets; } - std::map> const& unsafeTargets() const { return m_unsafeTargets; } + struct ReportTargetInfo + { + langutil::ErrorId error; + langutil::SourceLocation location; + std::string message; + }; + std::map, smt::EncodingContext::IdCompare> const& safeTargets() const { return m_safeTargets; } + std::map, smt::EncodingContext::IdCompare> const& unsafeTargets() const { return m_unsafeTargets; } /// This is used if the Horn solver is not directly linked into this binary. /// @returns a list of inputs to the Horn solver that were not part of the argument to @@ -347,10 +355,12 @@ private: /// Helper mapping unique IDs to actual verification targets. std::map m_verificationTargets; - /// Targets proven safe. - std::map> m_safeTargets; - /// Targets proven unsafe. - std::map> m_unsafeTargets; + /// Targets proved safe. + std::map, smt::EncodingContext::IdCompare> m_safeTargets; + /// Targets proved unsafe. + std::map, smt::EncodingContext::IdCompare> m_unsafeTargets; + /// Targets not proved. + std::map, smt::EncodingContext::IdCompare> m_unprovedTargets; //@} /// Control-flow. diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp index 1aac80248..9b304f8ea 100644 --- a/libsolidity/formal/ModelChecker.cpp +++ b/libsolidity/formal/ModelChecker.cpp @@ -120,8 +120,8 @@ void ModelChecker::analyze(SourceUnit const& _source) m_chc.analyze(_source); auto solvedTargets = m_chc.safeTargets(); - for (auto const& target: m_chc.unsafeTargets()) - solvedTargets[target.first] += target.second; + for (auto const& [node, targets]: m_chc.unsafeTargets()) + solvedTargets[node] += targets | ranges::views::keys; if (m_settings.engine.bmc) m_bmc.analyze(_source, solvedTargets); diff --git a/libsolidity/formal/ModelCheckerSettings.h b/libsolidity/formal/ModelCheckerSettings.h index edd8f0800..ff39ddc9f 100644 --- a/libsolidity/formal/ModelCheckerSettings.h +++ b/libsolidity/formal/ModelCheckerSettings.h @@ -113,6 +113,7 @@ struct ModelCheckerSettings { ModelCheckerContracts contracts = ModelCheckerContracts::Default(); ModelCheckerEngine engine = ModelCheckerEngine::None(); + bool showUnproved = false; smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::All(); ModelCheckerTargets targets = ModelCheckerTargets::Default(); std::optional timeout; @@ -123,6 +124,7 @@ struct ModelCheckerSettings return contracts == _other.contracts && engine == _other.engine && + showUnproved == _other.showUnproved && solvers == _other.solvers && targets == _other.targets && timeout == _other.timeout; diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp index 70ed10d27..0a12059d5 100644 --- a/libsolidity/interface/StandardCompiler.cpp +++ b/libsolidity/interface/StandardCompiler.cpp @@ -442,7 +442,7 @@ std::optional checkSettingsKeys(Json::Value const& _input) std::optional checkModelCheckerSettingsKeys(Json::Value const& _input) { - static set keys{"contracts", "engine", "solvers", "targets", "timeout"}; + static set keys{"contracts", "engine", "showUnproved", "solvers", "targets", "timeout"}; return checkKeys(_input, keys, "modelChecker"); } @@ -951,6 +951,14 @@ std::variant StandardCompiler: ret.modelCheckerSettings.engine = *engine; } + if (modelCheckerSettings.isMember("showUnproved")) + { + auto const& showUnproved = modelCheckerSettings["showUnproved"]; + if (!showUnproved.isBool()) + return formatFatalError("JSONError", "settings.modelChecker.showUnproved must be a Boolean value."); + ret.modelCheckerSettings.showUnproved = showUnproved.asBool(); + } + if (modelCheckerSettings.isMember("solvers")) { auto const& solversArray = modelCheckerSettings["solvers"]; diff --git a/solc/CommandLineParser.cpp b/solc/CommandLineParser.cpp index a01aa59f5..3654bbfc8 100644 --- a/solc/CommandLineParser.cpp +++ b/solc/CommandLineParser.cpp @@ -87,6 +87,7 @@ static string const g_strMetadataHash = "metadata-hash"; static string const g_strMetadataLiteral = "metadata-literal"; static string const g_strModelCheckerContracts = "model-checker-contracts"; static string const g_strModelCheckerEngine = "model-checker-engine"; +static string const g_strModelCheckerShowUnproved = "model-checker-show-unproved"; static string const g_strModelCheckerSolvers = "model-checker-solvers"; static string const g_strModelCheckerTargets = "model-checker-targets"; static string const g_strModelCheckerTimeout = "model-checker-timeout"; @@ -724,6 +725,11 @@ General Information)").c_str(), po::value()->value_name("all,bmc,chc,none")->default_value("none"), "Select model checker engine." ) + ( + g_strModelCheckerShowUnproved.c_str(), + po::value()->value_name("false,true")->default_value(false), + "Select whether to show all unproved targets." + ) ( g_strModelCheckerSolvers.c_str(), po::value()->value_name("all,cvc4,z3,smtlib2")->default_value("all"), @@ -1098,6 +1104,12 @@ General Information)").c_str(), m_options.modelChecker.settings.engine = *engine; } + if (m_args.count(g_strModelCheckerShowUnproved)) + { + bool showUnproved = m_args[g_strModelCheckerShowUnproved].as(); + m_options.modelChecker.settings.showUnproved = showUnproved; + } + if (m_args.count(g_strModelCheckerSolvers)) { string solversStr = m_args[g_strModelCheckerSolvers].as(); @@ -1129,6 +1141,7 @@ General Information)").c_str(), m_options.modelChecker.initialize = m_args.count(g_strModelCheckerContracts) || m_args.count(g_strModelCheckerEngine) || + m_args.count(g_strModelCheckerShowUnproved) || m_args.count(g_strModelCheckerSolvers) || m_args.count(g_strModelCheckerTargets) || m_args.count(g_strModelCheckerTimeout); diff --git a/test/cmdlineTests/model_checker_show_unproved_default_all_engines/args b/test/cmdlineTests/model_checker_show_unproved_default_all_engines/args new file mode 100644 index 000000000..5aeb1490e --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_default_all_engines/args @@ -0,0 +1 @@ +--model-checker-engine all diff --git a/test/cmdlineTests/model_checker_show_unproved_default_all_engines/err b/test/cmdlineTests/model_checker_show_unproved_default_all_engines/err new file mode 100644 index 000000000..45c38ef35 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_default_all_engines/err @@ -0,0 +1,3 @@ +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: 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. diff --git a/test/cmdlineTests/model_checker_show_unproved_default_all_engines/input.sol b/test/cmdlineTests/model_checker_show_unproved_default_all_engines/input.sol new file mode 100644 index 000000000..567c9cd2b --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_default_all_engines/input.sol @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } +} diff --git a/test/cmdlineTests/model_checker_show_unproved_default_bmc/args b/test/cmdlineTests/model_checker_show_unproved_default_bmc/args new file mode 100644 index 000000000..549f20236 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_default_bmc/args @@ -0,0 +1 @@ +--model-checker-engine bmc diff --git a/test/cmdlineTests/model_checker_show_unproved_default_bmc/err b/test/cmdlineTests/model_checker_show_unproved_default_bmc/err new file mode 100644 index 000000000..f8d0af2f4 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_default_bmc/err @@ -0,0 +1 @@ +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. diff --git a/test/cmdlineTests/model_checker_show_unproved_default_bmc/input.sol b/test/cmdlineTests/model_checker_show_unproved_default_bmc/input.sol new file mode 100644 index 000000000..567c9cd2b --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_default_bmc/input.sol @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } +} diff --git a/test/cmdlineTests/model_checker_show_unproved_default_chc/args b/test/cmdlineTests/model_checker_show_unproved_default_chc/args new file mode 100644 index 000000000..7458a47d3 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_default_chc/args @@ -0,0 +1 @@ +--model-checker-engine chc diff --git a/test/cmdlineTests/model_checker_show_unproved_default_chc/err b/test/cmdlineTests/model_checker_show_unproved_default_chc/err new file mode 100644 index 000000000..77083185f --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_default_chc/err @@ -0,0 +1 @@ +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. diff --git a/test/cmdlineTests/model_checker_show_unproved_default_chc/input.sol b/test/cmdlineTests/model_checker_show_unproved_default_chc/input.sol new file mode 100644 index 000000000..567c9cd2b --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_default_chc/input.sol @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } +} diff --git a/test/cmdlineTests/model_checker_show_unproved_false_all_engines/args b/test/cmdlineTests/model_checker_show_unproved_false_all_engines/args new file mode 100644 index 000000000..5f6883c76 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_false_all_engines/args @@ -0,0 +1 @@ +--model-checker-engine all --model-checker-show-unproved false diff --git a/test/cmdlineTests/model_checker_show_unproved_false_all_engines/err b/test/cmdlineTests/model_checker_show_unproved_false_all_engines/err new file mode 100644 index 000000000..45c38ef35 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_false_all_engines/err @@ -0,0 +1,3 @@ +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: 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. diff --git a/test/cmdlineTests/model_checker_show_unproved_false_all_engines/input.sol b/test/cmdlineTests/model_checker_show_unproved_false_all_engines/input.sol new file mode 100644 index 000000000..567c9cd2b --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_false_all_engines/input.sol @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } +} diff --git a/test/cmdlineTests/model_checker_show_unproved_false_bmc/args b/test/cmdlineTests/model_checker_show_unproved_false_bmc/args new file mode 100644 index 000000000..40fcde62b --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_false_bmc/args @@ -0,0 +1 @@ +--model-checker-engine bmc --model-checker-show-unproved false diff --git a/test/cmdlineTests/model_checker_show_unproved_false_bmc/err b/test/cmdlineTests/model_checker_show_unproved_false_bmc/err new file mode 100644 index 000000000..f8d0af2f4 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_false_bmc/err @@ -0,0 +1 @@ +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. diff --git a/test/cmdlineTests/model_checker_show_unproved_false_bmc/input.sol b/test/cmdlineTests/model_checker_show_unproved_false_bmc/input.sol new file mode 100644 index 000000000..567c9cd2b --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_false_bmc/input.sol @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } +} diff --git a/test/cmdlineTests/model_checker_show_unproved_false_chc/args b/test/cmdlineTests/model_checker_show_unproved_false_chc/args new file mode 100644 index 000000000..c14333f44 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_false_chc/args @@ -0,0 +1 @@ +--model-checker-engine chc --model-checker-show-unproved false diff --git a/test/cmdlineTests/model_checker_show_unproved_false_chc/err b/test/cmdlineTests/model_checker_show_unproved_false_chc/err new file mode 100644 index 000000000..77083185f --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_false_chc/err @@ -0,0 +1 @@ +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. diff --git a/test/cmdlineTests/model_checker_show_unproved_false_chc/input.sol b/test/cmdlineTests/model_checker_show_unproved_false_chc/input.sol new file mode 100644 index 000000000..567c9cd2b --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_false_chc/input.sol @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } +} diff --git a/test/cmdlineTests/model_checker_show_unproved_true_all_engines/args b/test/cmdlineTests/model_checker_show_unproved_true_all_engines/args new file mode 100644 index 000000000..4ccfd2e96 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_true_all_engines/args @@ -0,0 +1 @@ +--model-checker-engine all --model-checker-show-unproved true diff --git a/test/cmdlineTests/model_checker_show_unproved_true_all_engines/err b/test/cmdlineTests/model_checker_show_unproved_true_all_engines/err new file mode 100644 index 000000000..83864075d --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_true_all_engines/err @@ -0,0 +1,12 @@ +Warning: CHC: Assertion violation might happen here. + --> model_checker_show_unproved_true_all_engines/input.sol:10:9: + | +10 | assert(s.x > 0); + | ^^^^^^^^^^^^^^^ + +Warning: BMC: Assertion violation might happen here. + --> model_checker_show_unproved_true_all_engines/input.sol:10:9: + | +10 | assert(s.x > 0); + | ^^^^^^^^^^^^^^^ +Note: diff --git a/test/cmdlineTests/model_checker_show_unproved_true_all_engines/input.sol b/test/cmdlineTests/model_checker_show_unproved_true_all_engines/input.sol new file mode 100644 index 000000000..567c9cd2b --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_true_all_engines/input.sol @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } +} diff --git a/test/cmdlineTests/model_checker_show_unproved_true_bmc/args b/test/cmdlineTests/model_checker_show_unproved_true_bmc/args new file mode 100644 index 000000000..79cae9260 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_true_bmc/args @@ -0,0 +1 @@ +--model-checker-engine bmc --model-checker-show-unproved true diff --git a/test/cmdlineTests/model_checker_show_unproved_true_bmc/err b/test/cmdlineTests/model_checker_show_unproved_true_bmc/err new file mode 100644 index 000000000..84ada7873 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_true_bmc/err @@ -0,0 +1,6 @@ +Warning: BMC: Assertion violation might happen here. + --> model_checker_show_unproved_true_bmc/input.sol:10:9: + | +10 | assert(s.x > 0); + | ^^^^^^^^^^^^^^^ +Note: diff --git a/test/cmdlineTests/model_checker_show_unproved_true_bmc/input.sol b/test/cmdlineTests/model_checker_show_unproved_true_bmc/input.sol new file mode 100644 index 000000000..567c9cd2b --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_true_bmc/input.sol @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } +} diff --git a/test/cmdlineTests/model_checker_show_unproved_true_chc/args b/test/cmdlineTests/model_checker_show_unproved_true_chc/args new file mode 100644 index 000000000..f992f4d0c --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_true_chc/args @@ -0,0 +1 @@ +--model-checker-engine chc --model-checker-show-unproved true diff --git a/test/cmdlineTests/model_checker_show_unproved_true_chc/err b/test/cmdlineTests/model_checker_show_unproved_true_chc/err new file mode 100644 index 000000000..8274f4b46 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_true_chc/err @@ -0,0 +1,5 @@ +Warning: CHC: Assertion violation might happen here. + --> model_checker_show_unproved_true_chc/input.sol:10:9: + | +10 | assert(s.x > 0); + | ^^^^^^^^^^^^^^^ diff --git a/test/cmdlineTests/model_checker_show_unproved_true_chc/input.sol b/test/cmdlineTests/model_checker_show_unproved_true_chc/input.sol new file mode 100644 index 000000000..567c9cd2b --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_true_chc/input.sol @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } +} diff --git a/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/args b/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/args new file mode 100644 index 000000000..b20188349 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/args @@ -0,0 +1 @@ +--model-checker-engine all --model-checker-show-unproved aaa diff --git a/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/err b/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/err new file mode 100644 index 000000000..9ece92874 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/err @@ -0,0 +1 @@ +the argument ('aaa') for option '--model-checker-show-unproved' is invalid. Valid choices are 'on|off', 'yes|no', '1|0' and 'true|false' diff --git a/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/exit b/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/exit new file mode 100644 index 000000000..d00491fd7 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/exit @@ -0,0 +1 @@ +1 diff --git a/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/input.sol b/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/input.sol new file mode 100644 index 000000000..567c9cd2b --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/input.sol @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } +} diff --git a/test/cmdlineTests/model_checker_timeout_all/err b/test/cmdlineTests/model_checker_timeout_all/err index 6b2d3392a..45c38ef35 100644 --- a/test/cmdlineTests/model_checker_timeout_all/err +++ b/test/cmdlineTests/model_checker_timeout_all/err @@ -1,12 +1,3 @@ -Warning: CHC: Assertion violation might happen here. - --> model_checker_timeout_all/input.sol:9:3: - | -9 | assert(r % k == 0); - | ^^^^^^^^^^^^^^^^^^ +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: BMC: Assertion violation might happen here. - --> model_checker_timeout_all/input.sol:9:3: - | -9 | assert(r % k == 0); - | ^^^^^^^^^^^^^^^^^^ -Note: +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. diff --git a/test/cmdlineTests/model_checker_timeout_bmc/err b/test/cmdlineTests/model_checker_timeout_bmc/err index 9cce6ba0c..f8d0af2f4 100644 --- a/test/cmdlineTests/model_checker_timeout_bmc/err +++ b/test/cmdlineTests/model_checker_timeout_bmc/err @@ -1,6 +1 @@ -Warning: BMC: Assertion violation might happen here. - --> model_checker_timeout_bmc/input.sol:9:3: - | -9 | assert(r % k == 0); - | ^^^^^^^^^^^^^^^^^^ -Note: +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. diff --git a/test/cmdlineTests/model_checker_timeout_chc/err b/test/cmdlineTests/model_checker_timeout_chc/err index 187ef937c..77083185f 100644 --- a/test/cmdlineTests/model_checker_timeout_chc/err +++ b/test/cmdlineTests/model_checker_timeout_chc/err @@ -1,5 +1 @@ -Warning: CHC: Assertion violation might happen here. - --> model_checker_timeout_chc/input.sol:9:3: - | -9 | assert(r % k == 0); - | ^^^^^^^^^^^^^^^^^^ +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. diff --git a/test/cmdlineTests/standard_model_checker_show_unproved_default_all_engines/input.json b/test/cmdlineTests/standard_model_checker_show_unproved_default_all_engines/input.json new file mode 100644 index 000000000..18a8b21fc --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unproved_default_all_engines/input.json @@ -0,0 +1,26 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "all" + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unproved_default_all_engines/output.json b/test/cmdlineTests/standard_model_checker_show_unproved_default_all_engines/output.json new file mode 100644 index 000000000..cf4c00c61 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unproved_default_all_engines/output.json @@ -0,0 +1,90 @@ +{"auxiliaryInputRequested":{"smtlib2queries":{"0x119e9d636624c5af8dc0d97ee8d2905551bfe9eea88d60c6d3793cfdc576a76b":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int))))) +(declare-fun |s_7_0| () |struct test.S|) +(declare-fun |b_9_0| () Bool) +(declare-fun |s_7_1| () |struct test.S|) +(declare-fun |expr_15_0| () Bool) +(declare-fun |expr_15_1| () Bool) +(declare-fun |expr_16_0| () Int) +(declare-fun |expr_17_0| () Int) +(declare-fun |expr_18_0| () Int) +(declare-fun |expr_12_0| () |struct test.S|) +(declare-fun |expr_14_1| () Int) +(declare-fun |expr_19_1| () Int) +(declare-fun |expr_12_1| () |struct test.S|) +(declare-fun |expr_12_2| () |struct test.S|) +(declare-fun |expr_14_2| () Int) +(declare-fun |s_7_2| () |struct test.S|) +(declare-fun |expr_12_3| () |struct test.S|) +(declare-fun |expr_22_0| () |struct test.S|) +(declare-fun |expr_23_1| () Int) +(declare-fun |expr_24_0| () Int) +(declare-fun |expr_25_1| () Bool) + +(assert (and (and (and true true) (and (= expr_25_1 (> expr_23_1 expr_24_0)) (and (=> (and true true) true) (and (= expr_24_0 0) (and (=> (and true true) (and (>= expr_23_1 0) (<= expr_23_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_23_1 (|struct test.S_accessor_x| expr_22_0)) (and (= expr_22_0 s_7_2) (and (= expr_12_3 s_7_2) (and (ite (and true true) (= s_7_2 expr_12_2) (= s_7_2 s_7_1)) (and (=> (and true true) (and (>= expr_14_2 0) (<= expr_14_2 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_2 (|struct test.S_accessor_x| expr_12_2)) (and (= (|struct test.S_accessor_x| expr_12_2) expr_19_1) (and (= expr_12_1 s_7_1) (and (=> (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (bv2nat (bvor (ite (>= expr_14_1 0) ((_ int2bv 256) expr_14_1) (bvneg ((_ int2bv 256) (- expr_14_1)))) (ite (>= expr_18_0 0) ((_ int2bv 256) expr_18_0) (bvneg ((_ int2bv 256) (- expr_18_0))))))) (and (=> (and true true) (and (>= expr_14_1 0) (<= expr_14_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_1 (|struct test.S_accessor_x| expr_12_0)) (and (= expr_12_0 s_7_1) (and (=> (and true true) (and (>= expr_18_0 0) (<= expr_18_0 255))) (and (= expr_18_0 (ite expr_15_1 expr_16_0 expr_17_0)) (and (=> (and (and true true) (not expr_15_1)) true) (and (= expr_17_0 2) (and (=> (and (and true true) expr_15_1) true) (and (= expr_16_0 1) (and (= expr_15_1 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))) (not expr_25_1))) +(declare-const |EVALEXPR_0| Bool) +(assert (= |EVALEXPR_0| b_9_0)) +(check-sat) +(get-value (|EVALEXPR_0| )) +","0x4d368a1e0f051bee84d8e64e660d7d50d57486e66c037dcdb97b06447bbcfb8e":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int))))) +(declare-fun |s_7_0| () |struct test.S|) +(declare-fun |b_9_0| () Bool) +(declare-fun |s_7_1| () |struct test.S|) +(declare-fun |expr_15_0| () Bool) + +(assert (and (and (and true true) (and (= expr_15_0 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))) (not expr_15_0))) +(check-sat) +","0xab73091601c574bdace0ae9a7fc088a8f13ff47d4b78323c2df81da0281c9df4":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int))))) +(declare-fun |s_7_0| () |struct test.S|) +(declare-fun |b_9_0| () Bool) +(declare-fun |s_7_1| () |struct test.S|) +(declare-fun |expr_15_0| () Bool) + +(assert (and (and (and true true) (and (= expr_15_0 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))) expr_15_0)) +(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: 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":"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"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_show_unproved_false_all_engines/input.json b/test/cmdlineTests/standard_model_checker_show_unproved_false_all_engines/input.json new file mode 100644 index 000000000..d7396dd98 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unproved_false_all_engines/input.json @@ -0,0 +1,27 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "all", + "showUnproved": false + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unproved_false_all_engines/output.json b/test/cmdlineTests/standard_model_checker_show_unproved_false_all_engines/output.json new file mode 100644 index 000000000..cf4c00c61 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unproved_false_all_engines/output.json @@ -0,0 +1,90 @@ +{"auxiliaryInputRequested":{"smtlib2queries":{"0x119e9d636624c5af8dc0d97ee8d2905551bfe9eea88d60c6d3793cfdc576a76b":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int))))) +(declare-fun |s_7_0| () |struct test.S|) +(declare-fun |b_9_0| () Bool) +(declare-fun |s_7_1| () |struct test.S|) +(declare-fun |expr_15_0| () Bool) +(declare-fun |expr_15_1| () Bool) +(declare-fun |expr_16_0| () Int) +(declare-fun |expr_17_0| () Int) +(declare-fun |expr_18_0| () Int) +(declare-fun |expr_12_0| () |struct test.S|) +(declare-fun |expr_14_1| () Int) +(declare-fun |expr_19_1| () Int) +(declare-fun |expr_12_1| () |struct test.S|) +(declare-fun |expr_12_2| () |struct test.S|) +(declare-fun |expr_14_2| () Int) +(declare-fun |s_7_2| () |struct test.S|) +(declare-fun |expr_12_3| () |struct test.S|) +(declare-fun |expr_22_0| () |struct test.S|) +(declare-fun |expr_23_1| () Int) +(declare-fun |expr_24_0| () Int) +(declare-fun |expr_25_1| () Bool) + +(assert (and (and (and true true) (and (= expr_25_1 (> expr_23_1 expr_24_0)) (and (=> (and true true) true) (and (= expr_24_0 0) (and (=> (and true true) (and (>= expr_23_1 0) (<= expr_23_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_23_1 (|struct test.S_accessor_x| expr_22_0)) (and (= expr_22_0 s_7_2) (and (= expr_12_3 s_7_2) (and (ite (and true true) (= s_7_2 expr_12_2) (= s_7_2 s_7_1)) (and (=> (and true true) (and (>= expr_14_2 0) (<= expr_14_2 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_2 (|struct test.S_accessor_x| expr_12_2)) (and (= (|struct test.S_accessor_x| expr_12_2) expr_19_1) (and (= expr_12_1 s_7_1) (and (=> (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (bv2nat (bvor (ite (>= expr_14_1 0) ((_ int2bv 256) expr_14_1) (bvneg ((_ int2bv 256) (- expr_14_1)))) (ite (>= expr_18_0 0) ((_ int2bv 256) expr_18_0) (bvneg ((_ int2bv 256) (- expr_18_0))))))) (and (=> (and true true) (and (>= expr_14_1 0) (<= expr_14_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_1 (|struct test.S_accessor_x| expr_12_0)) (and (= expr_12_0 s_7_1) (and (=> (and true true) (and (>= expr_18_0 0) (<= expr_18_0 255))) (and (= expr_18_0 (ite expr_15_1 expr_16_0 expr_17_0)) (and (=> (and (and true true) (not expr_15_1)) true) (and (= expr_17_0 2) (and (=> (and (and true true) expr_15_1) true) (and (= expr_16_0 1) (and (= expr_15_1 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))) (not expr_25_1))) +(declare-const |EVALEXPR_0| Bool) +(assert (= |EVALEXPR_0| b_9_0)) +(check-sat) +(get-value (|EVALEXPR_0| )) +","0x4d368a1e0f051bee84d8e64e660d7d50d57486e66c037dcdb97b06447bbcfb8e":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int))))) +(declare-fun |s_7_0| () |struct test.S|) +(declare-fun |b_9_0| () Bool) +(declare-fun |s_7_1| () |struct test.S|) +(declare-fun |expr_15_0| () Bool) + +(assert (and (and (and true true) (and (= expr_15_0 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))) (not expr_15_0))) +(check-sat) +","0xab73091601c574bdace0ae9a7fc088a8f13ff47d4b78323c2df81da0281c9df4":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int))))) +(declare-fun |s_7_0| () |struct test.S|) +(declare-fun |b_9_0| () Bool) +(declare-fun |s_7_1| () |struct test.S|) +(declare-fun |expr_15_0| () Bool) + +(assert (and (and (and true true) (and (= expr_15_0 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))) expr_15_0)) +(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: 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":"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"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_show_unproved_false_bmc/input.json b/test/cmdlineTests/standard_model_checker_show_unproved_false_bmc/input.json new file mode 100644 index 000000000..c9ee3258e --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unproved_false_bmc/input.json @@ -0,0 +1,27 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "bmc", + "showUnproved": false + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unproved_false_bmc/output.json b/test/cmdlineTests/standard_model_checker_show_unproved_false_bmc/output.json new file mode 100644 index 000000000..6d9e16af8 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unproved_false_bmc/output.json @@ -0,0 +1,88 @@ +{"auxiliaryInputRequested":{"smtlib2queries":{"0x119e9d636624c5af8dc0d97ee8d2905551bfe9eea88d60c6d3793cfdc576a76b":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int))))) +(declare-fun |s_7_0| () |struct test.S|) +(declare-fun |b_9_0| () Bool) +(declare-fun |s_7_1| () |struct test.S|) +(declare-fun |expr_15_0| () Bool) +(declare-fun |expr_15_1| () Bool) +(declare-fun |expr_16_0| () Int) +(declare-fun |expr_17_0| () Int) +(declare-fun |expr_18_0| () Int) +(declare-fun |expr_12_0| () |struct test.S|) +(declare-fun |expr_14_1| () Int) +(declare-fun |expr_19_1| () Int) +(declare-fun |expr_12_1| () |struct test.S|) +(declare-fun |expr_12_2| () |struct test.S|) +(declare-fun |expr_14_2| () Int) +(declare-fun |s_7_2| () |struct test.S|) +(declare-fun |expr_12_3| () |struct test.S|) +(declare-fun |expr_22_0| () |struct test.S|) +(declare-fun |expr_23_1| () Int) +(declare-fun |expr_24_0| () Int) +(declare-fun |expr_25_1| () Bool) + +(assert (and (and (and true true) (and (= expr_25_1 (> expr_23_1 expr_24_0)) (and (=> (and true true) true) (and (= expr_24_0 0) (and (=> (and true true) (and (>= expr_23_1 0) (<= expr_23_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_23_1 (|struct test.S_accessor_x| expr_22_0)) (and (= expr_22_0 s_7_2) (and (= expr_12_3 s_7_2) (and (ite (and true true) (= s_7_2 expr_12_2) (= s_7_2 s_7_1)) (and (=> (and true true) (and (>= expr_14_2 0) (<= expr_14_2 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_2 (|struct test.S_accessor_x| expr_12_2)) (and (= (|struct test.S_accessor_x| expr_12_2) expr_19_1) (and (= expr_12_1 s_7_1) (and (=> (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (bv2nat (bvor (ite (>= expr_14_1 0) ((_ int2bv 256) expr_14_1) (bvneg ((_ int2bv 256) (- expr_14_1)))) (ite (>= expr_18_0 0) ((_ int2bv 256) expr_18_0) (bvneg ((_ int2bv 256) (- expr_18_0))))))) (and (=> (and true true) (and (>= expr_14_1 0) (<= expr_14_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_1 (|struct test.S_accessor_x| expr_12_0)) (and (= expr_12_0 s_7_1) (and (=> (and true true) (and (>= expr_18_0 0) (<= expr_18_0 255))) (and (= expr_18_0 (ite expr_15_1 expr_16_0 expr_17_0)) (and (=> (and (and true true) (not expr_15_1)) true) (and (= expr_17_0 2) (and (=> (and (and true true) expr_15_1) true) (and (= expr_16_0 1) (and (= expr_15_1 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))) (not expr_25_1))) +(declare-const |EVALEXPR_0| Bool) +(assert (= |EVALEXPR_0| b_9_0)) +(check-sat) +(get-value (|EVALEXPR_0| )) +","0x4d368a1e0f051bee84d8e64e660d7d50d57486e66c037dcdb97b06447bbcfb8e":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int))))) +(declare-fun |s_7_0| () |struct test.S|) +(declare-fun |b_9_0| () Bool) +(declare-fun |s_7_1| () |struct test.S|) +(declare-fun |expr_15_0| () Bool) + +(assert (and (and (and true true) (and (= expr_15_0 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))) (not expr_15_0))) +(check-sat) +","0xab73091601c574bdace0ae9a7fc088a8f13ff47d4b78323c2df81da0281c9df4":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int))))) +(declare-fun |s_7_0| () |struct test.S|) +(declare-fun |b_9_0| () Bool) +(declare-fun |s_7_1| () |struct test.S|) +(declare-fun |expr_15_0| () Bool) + +(assert (and (and (and true true) (and (= expr_15_0 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))) expr_15_0)) +(check-sat) +"}},"errors":[{"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"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_show_unproved_false_chc/input.json b/test/cmdlineTests/standard_model_checker_show_unproved_false_chc/input.json new file mode 100644 index 000000000..fe662e80c --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unproved_false_chc/input.json @@ -0,0 +1,27 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "chc", + "showUnproved": false + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unproved_false_chc/output.json b/test/cmdlineTests/standard_model_checker_show_unproved_false_chc/output.json new file mode 100644 index 000000000..5e66cb899 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unproved_false_chc/output.json @@ -0,0 +1,3 @@ +{"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: 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"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_show_unproved_true_all_engines/input.json b/test/cmdlineTests/standard_model_checker_show_unproved_true_all_engines/input.json new file mode 100644 index 000000000..3f9bb715e --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unproved_true_all_engines/input.json @@ -0,0 +1,27 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "all", + "showUnproved": true + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unproved_true_all_engines/output.json b/test/cmdlineTests/standard_model_checker_show_unproved_true_all_engines/output.json new file mode 100644 index 000000000..2e384c009 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unproved_true_all_engines/output.json @@ -0,0 +1,99 @@ +{"auxiliaryInputRequested":{"smtlib2queries":{"0x119e9d636624c5af8dc0d97ee8d2905551bfe9eea88d60c6d3793cfdc576a76b":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int))))) +(declare-fun |s_7_0| () |struct test.S|) +(declare-fun |b_9_0| () Bool) +(declare-fun |s_7_1| () |struct test.S|) +(declare-fun |expr_15_0| () Bool) +(declare-fun |expr_15_1| () Bool) +(declare-fun |expr_16_0| () Int) +(declare-fun |expr_17_0| () Int) +(declare-fun |expr_18_0| () Int) +(declare-fun |expr_12_0| () |struct test.S|) +(declare-fun |expr_14_1| () Int) +(declare-fun |expr_19_1| () Int) +(declare-fun |expr_12_1| () |struct test.S|) +(declare-fun |expr_12_2| () |struct test.S|) +(declare-fun |expr_14_2| () Int) +(declare-fun |s_7_2| () |struct test.S|) +(declare-fun |expr_12_3| () |struct test.S|) +(declare-fun |expr_22_0| () |struct test.S|) +(declare-fun |expr_23_1| () Int) +(declare-fun |expr_24_0| () Int) +(declare-fun |expr_25_1| () Bool) + +(assert (and (and (and true true) (and (= expr_25_1 (> expr_23_1 expr_24_0)) (and (=> (and true true) true) (and (= expr_24_0 0) (and (=> (and true true) (and (>= expr_23_1 0) (<= expr_23_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_23_1 (|struct test.S_accessor_x| expr_22_0)) (and (= expr_22_0 s_7_2) (and (= expr_12_3 s_7_2) (and (ite (and true true) (= s_7_2 expr_12_2) (= s_7_2 s_7_1)) (and (=> (and true true) (and (>= expr_14_2 0) (<= expr_14_2 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_2 (|struct test.S_accessor_x| expr_12_2)) (and (= (|struct test.S_accessor_x| expr_12_2) expr_19_1) (and (= expr_12_1 s_7_1) (and (=> (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (bv2nat (bvor (ite (>= expr_14_1 0) ((_ int2bv 256) expr_14_1) (bvneg ((_ int2bv 256) (- expr_14_1)))) (ite (>= expr_18_0 0) ((_ int2bv 256) expr_18_0) (bvneg ((_ int2bv 256) (- expr_18_0))))))) (and (=> (and true true) (and (>= expr_14_1 0) (<= expr_14_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_1 (|struct test.S_accessor_x| expr_12_0)) (and (= expr_12_0 s_7_1) (and (=> (and true true) (and (>= expr_18_0 0) (<= expr_18_0 255))) (and (= expr_18_0 (ite expr_15_1 expr_16_0 expr_17_0)) (and (=> (and (and true true) (not expr_15_1)) true) (and (= expr_17_0 2) (and (=> (and (and true true) expr_15_1) true) (and (= expr_16_0 1) (and (= expr_15_1 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))) (not expr_25_1))) +(declare-const |EVALEXPR_0| Bool) +(assert (= |EVALEXPR_0| b_9_0)) +(check-sat) +(get-value (|EVALEXPR_0| )) +","0x4d368a1e0f051bee84d8e64e660d7d50d57486e66c037dcdb97b06447bbcfb8e":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int))))) +(declare-fun |s_7_0| () |struct test.S|) +(declare-fun |b_9_0| () Bool) +(declare-fun |s_7_1| () |struct test.S|) +(declare-fun |expr_15_0| () Bool) + +(assert (and (and (and true true) (and (= expr_15_0 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))) (not expr_15_0))) +(check-sat) +","0xab73091601c574bdace0ae9a7fc088a8f13ff47d4b78323c2df81da0281c9df4":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int))))) +(declare-fun |s_7_0| () |struct test.S|) +(declare-fun |b_9_0| () Bool) +(declare-fun |s_7_1| () |struct test.S|) +(declare-fun |expr_15_0| () Bool) + +(assert (and (and (and true true) (and (= expr_15_0 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))) expr_15_0)) +(check-sat) +"}},"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation might happen here. + --> A:11:7: + | +11 | \t\t\t\t\t\tassert(s.x > 0); + | \t\t\t\t\t\t^^^^^^^^^^^^^^^ + +","message":"CHC: Assertion violation might happen here.","severity":"warning","sourceLocation":{"end":201,"file":"A","start":186},"type":"Warning"},{"component":"general","errorCode":"7812","formattedMessage":"Warning: BMC: Assertion violation might happen here. + --> A:11:7: + | +11 | \t\t\t\t\t\tassert(s.x > 0); + | \t\t\t\t\t\t^^^^^^^^^^^^^^^ +Note: + +","message":"BMC: Assertion violation might happen here.","secondarySourceLocations":[{"message":""}],"severity":"warning","sourceLocation":{"end":201,"file":"A","start":186},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_show_unproved_true_bmc/input.json b/test/cmdlineTests/standard_model_checker_show_unproved_true_bmc/input.json new file mode 100644 index 000000000..2f367ae80 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unproved_true_bmc/input.json @@ -0,0 +1,27 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "bmc", + "showUnproved": true + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unproved_true_bmc/output.json b/test/cmdlineTests/standard_model_checker_show_unproved_true_bmc/output.json new file mode 100644 index 000000000..d21389103 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unproved_true_bmc/output.json @@ -0,0 +1,93 @@ +{"auxiliaryInputRequested":{"smtlib2queries":{"0x119e9d636624c5af8dc0d97ee8d2905551bfe9eea88d60c6d3793cfdc576a76b":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int))))) +(declare-fun |s_7_0| () |struct test.S|) +(declare-fun |b_9_0| () Bool) +(declare-fun |s_7_1| () |struct test.S|) +(declare-fun |expr_15_0| () Bool) +(declare-fun |expr_15_1| () Bool) +(declare-fun |expr_16_0| () Int) +(declare-fun |expr_17_0| () Int) +(declare-fun |expr_18_0| () Int) +(declare-fun |expr_12_0| () |struct test.S|) +(declare-fun |expr_14_1| () Int) +(declare-fun |expr_19_1| () Int) +(declare-fun |expr_12_1| () |struct test.S|) +(declare-fun |expr_12_2| () |struct test.S|) +(declare-fun |expr_14_2| () Int) +(declare-fun |s_7_2| () |struct test.S|) +(declare-fun |expr_12_3| () |struct test.S|) +(declare-fun |expr_22_0| () |struct test.S|) +(declare-fun |expr_23_1| () Int) +(declare-fun |expr_24_0| () Int) +(declare-fun |expr_25_1| () Bool) + +(assert (and (and (and true true) (and (= expr_25_1 (> expr_23_1 expr_24_0)) (and (=> (and true true) true) (and (= expr_24_0 0) (and (=> (and true true) (and (>= expr_23_1 0) (<= expr_23_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_23_1 (|struct test.S_accessor_x| expr_22_0)) (and (= expr_22_0 s_7_2) (and (= expr_12_3 s_7_2) (and (ite (and true true) (= s_7_2 expr_12_2) (= s_7_2 s_7_1)) (and (=> (and true true) (and (>= expr_14_2 0) (<= expr_14_2 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_2 (|struct test.S_accessor_x| expr_12_2)) (and (= (|struct test.S_accessor_x| expr_12_2) expr_19_1) (and (= expr_12_1 s_7_1) (and (=> (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (bv2nat (bvor (ite (>= expr_14_1 0) ((_ int2bv 256) expr_14_1) (bvneg ((_ int2bv 256) (- expr_14_1)))) (ite (>= expr_18_0 0) ((_ int2bv 256) expr_18_0) (bvneg ((_ int2bv 256) (- expr_18_0))))))) (and (=> (and true true) (and (>= expr_14_1 0) (<= expr_14_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_1 (|struct test.S_accessor_x| expr_12_0)) (and (= expr_12_0 s_7_1) (and (=> (and true true) (and (>= expr_18_0 0) (<= expr_18_0 255))) (and (= expr_18_0 (ite expr_15_1 expr_16_0 expr_17_0)) (and (=> (and (and true true) (not expr_15_1)) true) (and (= expr_17_0 2) (and (=> (and (and true true) expr_15_1) true) (and (= expr_16_0 1) (and (= expr_15_1 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))) (not expr_25_1))) +(declare-const |EVALEXPR_0| Bool) +(assert (= |EVALEXPR_0| b_9_0)) +(check-sat) +(get-value (|EVALEXPR_0| )) +","0x4d368a1e0f051bee84d8e64e660d7d50d57486e66c037dcdb97b06447bbcfb8e":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int))))) +(declare-fun |s_7_0| () |struct test.S|) +(declare-fun |b_9_0| () Bool) +(declare-fun |s_7_1| () |struct test.S|) +(declare-fun |expr_15_0| () Bool) + +(assert (and (and (and true true) (and (= expr_15_0 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))) (not expr_15_0))) +(check-sat) +","0xab73091601c574bdace0ae9a7fc088a8f13ff47d4b78323c2df81da0281c9df4":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int))))) +(declare-fun |s_7_0| () |struct test.S|) +(declare-fun |b_9_0| () Bool) +(declare-fun |s_7_1| () |struct test.S|) +(declare-fun |expr_15_0| () Bool) + +(assert (and (and (and true true) (and (= expr_15_0 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))) expr_15_0)) +(check-sat) +"}},"errors":[{"component":"general","errorCode":"7812","formattedMessage":"Warning: BMC: Assertion violation might happen here. + --> A:11:7: + | +11 | \t\t\t\t\t\tassert(s.x > 0); + | \t\t\t\t\t\t^^^^^^^^^^^^^^^ +Note: + +","message":"BMC: Assertion violation might happen here.","secondarySourceLocations":[{"message":""}],"severity":"warning","sourceLocation":{"end":201,"file":"A","start":186},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_show_unproved_true_chc/input.json b/test/cmdlineTests/standard_model_checker_show_unproved_true_chc/input.json new file mode 100644 index 000000000..f81688b71 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unproved_true_chc/input.json @@ -0,0 +1,27 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "chc", + "showUnproved": true + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unproved_true_chc/output.json b/test/cmdlineTests/standard_model_checker_show_unproved_true_chc/output.json new file mode 100644 index 000000000..352b76d27 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unproved_true_chc/output.json @@ -0,0 +1,7 @@ +{"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation might happen here. + --> A:11:7: + | +11 | \t\t\t\t\t\tassert(s.x > 0); + | \t\t\t\t\t\t^^^^^^^^^^^^^^^ + +","message":"CHC: Assertion violation might happen here.","severity":"warning","sourceLocation":{"end":201,"file":"A","start":186},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_show_unproved_wrong/input.json b/test/cmdlineTests/standard_model_checker_show_unproved_wrong/input.json new file mode 100644 index 000000000..bdaec9b3e --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unproved_wrong/input.json @@ -0,0 +1,27 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "all", + "showUnproved": "aaa" + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unproved_wrong/output.json b/test/cmdlineTests/standard_model_checker_show_unproved_wrong/output.json new file mode 100644 index 000000000..394dbf925 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unproved_wrong/output.json @@ -0,0 +1 @@ +{"errors":[{"component":"general","formattedMessage":"settings.modelChecker.showUnproved must be a Boolean value.","message":"settings.modelChecker.showUnproved must be a Boolean value.","severity":"error","type":"JSONError"}]} diff --git a/test/cmdlineTests/standard_model_checker_timeout_all/output.json b/test/cmdlineTests/standard_model_checker_timeout_all/output.json index 15f7ad969..335a6f99e 100644 --- a/test/cmdlineTests/standard_model_checker_timeout_all/output.json +++ b/test/cmdlineTests/standard_model_checker_timeout_all/output.json @@ -254,17 +254,8 @@ (assert (= |EVALEXPR_3| r_33_1)) (check-sat) (get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| )) -"}},"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation might happen here. - --> A:6:85: - | -6 | require(k > 0); require(x % k == 0); require(y % k == 0); uint r = mulmod(x, y, k); assert(r % k == 0);}} - | ^^^^^^^^^^^^^^^^^^ +"}},"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: Assertion violation might happen here.","severity":"warning","sourceLocation":{"end":227,"file":"A","start":209},"type":"Warning"},{"component":"general","errorCode":"7812","formattedMessage":"Warning: BMC: Assertion violation might happen here. - --> A:6:85: - | -6 | require(k > 0); require(x % k == 0); require(y % k == 0); uint r = mulmod(x, y, k); assert(r % k == 0);}} - | ^^^^^^^^^^^^^^^^^^ -Note: +","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":"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: Assertion violation might happen here.","secondarySourceLocations":[{"message":""}],"severity":"warning","sourceLocation":{"end":227,"file":"A","start":209},"type":"Warning"}],"sources":{"A":{"id":0}}} +","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"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_timeout_bmc/output.json b/test/cmdlineTests/standard_model_checker_timeout_bmc/output.json index 0c3de2823..c1631811f 100644 --- a/test/cmdlineTests/standard_model_checker_timeout_bmc/output.json +++ b/test/cmdlineTests/standard_model_checker_timeout_bmc/output.json @@ -518,11 +518,6 @@ (assert (and (and (and true true) (and (= expr_21_1 (= expr_19_1 expr_20_0)) (and (=> (and true true) true) (and (= expr_20_0 0) (and (=> (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (ite (= expr_18_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_18_0 0) (< r_div_mod_0_0 expr_18_0))) (and (= (+ (* d_div_mod_0_0 expr_18_0) r_div_mod_0_0) expr_17_0) (and (=> (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 k_7_0) (and (=> (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_3_0) (and (=> (and true true) expr_13_1) (and (= expr_13_1 (> expr_11_0 expr_12_0)) (and (=> (and true true) true) (and (= expr_12_0 0) (and (=> (and true true) (and (>= expr_11_0 0) (<= expr_11_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_11_0 k_7_0) (and (and (>= k_7_0 0) (<= k_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_5_0 0) (<= y_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_3_0 0) (<= x_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_33_0 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3204897777)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 191)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 6)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 219)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 241)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))))))))))))))) (not expr_21_1))) (check-sat) -"}},"errors":[{"component":"general","errorCode":"7812","formattedMessage":"Warning: BMC: Assertion violation might happen here. - --> A:6:85: - | -6 | require(k > 0); require(x % k == 0); require(y % k == 0); uint r = mulmod(x, y, k); assert(r % k == 0);}} - | ^^^^^^^^^^^^^^^^^^ -Note: +"}},"errors":[{"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: Assertion violation might happen here.","secondarySourceLocations":[{"message":""}],"severity":"warning","sourceLocation":{"end":227,"file":"A","start":209},"type":"Warning"}],"sources":{"A":{"id":0}}} +","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"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_timeout_chc/output.json b/test/cmdlineTests/standard_model_checker_timeout_chc/output.json index 34de85f8f..5e66cb899 100644 --- a/test/cmdlineTests/standard_model_checker_timeout_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_timeout_chc/output.json @@ -1,7 +1,3 @@ -{"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation might happen here. - --> A:6:85: - | -6 | require(k > 0); require(x % k == 0); require(y % k == 0); uint r = mulmod(x, y, k); assert(r % k == 0);}} - | ^^^^^^^^^^^^^^^^^^ +{"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: Assertion violation might happen here.","severity":"warning","sourceLocation":{"end":227,"file":"A","start":209},"type":"Warning"}],"sources":{"A":{"id":0}}} +","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"}],"sources":{"A":{"id":0}}} diff --git a/test/libsolidity/SMTCheckerTest.cpp b/test/libsolidity/SMTCheckerTest.cpp index 961baab70..166aa2982 100644 --- a/test/libsolidity/SMTCheckerTest.cpp +++ b/test/libsolidity/SMTCheckerTest.cpp @@ -27,6 +27,14 @@ using namespace solidity::frontend::test; SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, EVMVersion{}) { + auto const& showUnproved = m_reader.stringSetting("SMTShowUnproved", "yes"); + if (showUnproved == "no") + m_modelCheckerSettings.showUnproved = false; + else if (showUnproved == "yes") + m_modelCheckerSettings.showUnproved = true; + else + BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT \"show unproved\" choice.")); + auto const& choice = m_reader.stringSetting("SMTSolvers", "any"); if (choice == "any") m_modelCheckerSettings.solvers = smtutil::SMTSolverChoice::All(); diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol index 0598311ad..2bbaa2e1c 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol @@ -22,14 +22,14 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (226-256): CHC: Assertion violation happens here. // Warning 1218: (310-340): CHC: Error trying to invoke SMT solver. -// Warning 6328: (310-340): CHC: Assertion violation might happen here. // Warning 1218: (483-513): CHC: Error trying to invoke SMT solver. -// Warning 6328: (483-513): CHC: Assertion violation might happen here. // Warning 1218: (568-598): CHC: Error trying to invoke SMT solver. -// Warning 6328: (568-598): CHC: Assertion violation might happen here. // Warning 1218: (654-684): CHC: Error trying to invoke SMT solver. +// Warning 6328: (226-256): CHC: Assertion violation happens here. +// Warning 6328: (310-340): CHC: Assertion violation might happen here. +// Warning 6328: (483-513): CHC: Assertion violation might happen here. +// Warning 6328: (568-598): CHC: Assertion violation might happen here. // Warning 6328: (654-684): CHC: Assertion violation might happen here. // Warning 4661: (310-340): BMC: Assertion violation happens here. // Warning 4661: (483-513): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal_no_unproved.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal_no_unproved.sol new file mode 100644 index 000000000..ffeef4896 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal_no_unproved.sol @@ -0,0 +1,35 @@ +contract C { + function abiencodePackedStringLiteral() public pure { + bytes memory b1 = abi.encodePacked(""); + bytes memory b2 = abi.encodePacked(""); + // should hold, but currently fails due to string literal abstraction + assert(b1.length == b2.length); + + bytes memory b3 = abi.encodePacked(bytes("")); + assert(b1.length == b3.length); // should fail + + bytes memory b4 = abi.encodePacked(bytes24("")); + // should hold, but currently fails due to string literal abstraction + assert(b1.length == b4.length); + + bytes memory b5 = abi.encodePacked(string("")); + assert(b1.length == b5.length); // should fail + + bytes memory b6 = abi.encode(""); + assert(b1.length == b6.length); // should fail + } +} +// ==== +// SMTEngine: all +// SMTShowUnproved: no +// ---- +// Warning 1218: (310-340): CHC: Error trying to invoke SMT solver. +// Warning 1218: (483-513): CHC: Error trying to invoke SMT solver. +// Warning 1218: (568-598): CHC: Error trying to invoke SMT solver. +// Warning 1218: (654-684): CHC: Error trying to invoke SMT solver. +// Warning 6328: (226-256): CHC: Assertion violation happens here. +// Warning 5840: CHC: 4 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 4661: (310-340): BMC: Assertion violation happens here. +// Warning 4661: (483-513): BMC: Assertion violation happens here. +// Warning 4661: (568-598): BMC: Assertion violation happens here. +// Warning 4661: (654-684): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol index 6eb3fff73..2a3ff2bb2 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol @@ -19,12 +19,12 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (208-238): CHC: Assertion violation happens here. // Warning 1218: (286-316): CHC: Error trying to invoke SMT solver. -// Warning 6328: (286-316): CHC: Assertion violation might happen here. // Warning 1218: (453-483): CHC: Error trying to invoke SMT solver. -// Warning 6328: (453-483): CHC: Assertion violation might happen here. // Warning 1218: (532-562): CHC: Error trying to invoke SMT solver. +// Warning 6328: (208-238): CHC: Assertion violation happens here. +// Warning 6328: (286-316): CHC: Assertion violation might happen here. +// Warning 6328: (453-483): CHC: Assertion violation might happen here. // Warning 6328: (532-562): CHC: Assertion violation might happen here. // Warning 4661: (286-316): BMC: Assertion violation happens here. // Warning 4661: (453-483): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol index 0365b9655..c9d9bb056 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol @@ -25,13 +25,13 @@ contract C { // ==== // SMTEngine: all // ---- +// Warning 1218: (691-721): CHC: Error trying to invoke SMT solver. +// Warning 1218: (959-989): CHC: Error trying to invoke SMT solver. +// Warning 1218: (1079-1109): CHC: Error trying to invoke SMT solver. // Warning 6328: (325-355): CHC: Assertion violation happens here. // Warning 6328: (578-608): CHC: Assertion violation happens here. -// Warning 1218: (691-721): CHC: Error trying to invoke SMT solver. // Warning 6328: (691-721): CHC: Assertion violation might happen here. -// Warning 1218: (959-989): CHC: Error trying to invoke SMT solver. // Warning 6328: (959-989): CHC: Assertion violation might happen here. -// Warning 1218: (1079-1109): CHC: Error trying to invoke SMT solver. // Warning 6328: (1079-1109): CHC: Assertion violation might happen here. // Warning 4661: (691-721): BMC: Assertion violation happens here. // Warning 4661: (959-989): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol index b94977030..740411bf3 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol @@ -25,13 +25,13 @@ contract C { // ==== // SMTEngine: all // ---- +// Warning 1218: (692-722): CHC: Error trying to invoke SMT solver. +// Warning 1218: (960-990): CHC: Error trying to invoke SMT solver. +// Warning 1218: (1080-1110): CHC: Error trying to invoke SMT solver. // Warning 6328: (326-356): CHC: Assertion violation happens here. // Warning 6328: (579-609): CHC: Assertion violation happens here. -// Warning 1218: (692-722): CHC: Error trying to invoke SMT solver. // Warning 6328: (692-722): CHC: Assertion violation might happen here. -// Warning 1218: (960-990): CHC: Error trying to invoke SMT solver. // Warning 6328: (960-990): CHC: Assertion violation might happen here. -// Warning 1218: (1080-1110): CHC: Error trying to invoke SMT solver. // Warning 6328: (1080-1110): CHC: Assertion violation might happen here. // Warning 4661: (692-722): BMC: Assertion violation happens here. // Warning 4661: (960-990): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol index 3360feb02..ca1b6b40a 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol @@ -14,8 +14,8 @@ contract C { // SMTEngine: all // ---- // Warning 1218: (333-371): CHC: Error trying to invoke SMT solver. -// Warning 6328: (333-371): CHC: Assertion violation might happen here. // Warning 1218: (390-428): CHC: Error trying to invoke SMT solver. +// Warning 6328: (333-371): CHC: Assertion violation might happen here. // Warning 6328: (390-428): CHC: Assertion violation might happen here. // Warning 4661: (333-371): BMC: Assertion violation happens here. // Warning 4661: (390-428): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol index e824c57d1..839d00835 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol @@ -22,14 +22,14 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (252-282): CHC: Assertion violation happens here. // Warning 1218: (347-377): CHC: Error trying to invoke SMT solver. -// Warning 6328: (347-377): CHC: Assertion violation might happen here. // Warning 1218: (531-561): CHC: Error trying to invoke SMT solver. -// Warning 6328: (531-561): CHC: Assertion violation might happen here. // Warning 1218: (627-657): CHC: Error trying to invoke SMT solver. -// Warning 6328: (627-657): CHC: Assertion violation might happen here. // Warning 1218: (746-776): CHC: Error trying to invoke SMT solver. +// Warning 6328: (252-282): CHC: Assertion violation happens here. +// Warning 6328: (347-377): CHC: Assertion violation might happen here. +// Warning 6328: (531-561): CHC: Assertion violation might happen here. +// Warning 6328: (627-657): CHC: Assertion violation might happen here. // Warning 6328: (746-776): CHC: Assertion violation might happen here. // Warning 4661: (347-377): BMC: Assertion violation happens here. // Warning 4661: (531-561): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol index 7530ea6c5..fd15ea27d 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol @@ -25,13 +25,13 @@ contract C { // ==== // SMTEngine: all // ---- +// Warning 1218: (702-732): CHC: Error trying to invoke SMT solver. +// Warning 1218: (971-1001): CHC: Error trying to invoke SMT solver. +// Warning 1218: (1086-1116): CHC: Error trying to invoke SMT solver. // Warning 6328: (334-364): CHC: Assertion violation happens here. // Warning 6328: (588-618): CHC: Assertion violation happens here. -// Warning 1218: (702-732): CHC: Error trying to invoke SMT solver. // Warning 6328: (702-732): CHC: Assertion violation might happen here. -// Warning 1218: (971-1001): CHC: Error trying to invoke SMT solver. // Warning 6328: (971-1001): CHC: Assertion violation might happen here. -// Warning 1218: (1086-1116): CHC: Error trying to invoke SMT solver. // Warning 6328: (1086-1116): CHC: Assertion violation might happen here. // Warning 4661: (702-732): BMC: Assertion violation happens here. // Warning 4661: (971-1001): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol index f9da7be6b..cdb87233e 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol @@ -25,13 +25,13 @@ contract C { // ==== // SMTEngine: all // ---- +// Warning 1218: (703-733): CHC: Error trying to invoke SMT solver. +// Warning 1218: (972-1002): CHC: Error trying to invoke SMT solver. +// Warning 1218: (1087-1117): CHC: Error trying to invoke SMT solver. // Warning 6328: (335-365): CHC: Assertion violation happens here. // Warning 6328: (589-619): CHC: Assertion violation happens here. -// Warning 1218: (703-733): CHC: Error trying to invoke SMT solver. // Warning 6328: (703-733): CHC: Assertion violation might happen here. -// Warning 1218: (972-1002): CHC: Error trying to invoke SMT solver. // Warning 6328: (972-1002): CHC: Assertion violation might happen here. -// Warning 1218: (1087-1117): CHC: Error trying to invoke SMT solver. // Warning 6328: (1087-1117): CHC: Assertion violation might happen here. // Warning 4661: (703-733): BMC: Assertion violation happens here. // Warning 4661: (972-1002): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol index a76f91f81..dbf423741 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol @@ -14,8 +14,8 @@ contract C { // SMTEngine: all // ---- // Warning 1218: (337-375): CHC: Error trying to invoke SMT solver. -// Warning 6328: (337-375): CHC: Assertion violation might happen here. // Warning 1218: (394-432): CHC: Error trying to invoke SMT solver. +// Warning 6328: (337-375): CHC: Assertion violation might happen here. // Warning 6328: (394-432): CHC: Assertion violation might happen here. // Warning 4661: (337-375): BMC: Assertion violation happens here. // Warning 4661: (394-432): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol index 666fa23ba..2e64229bc 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol @@ -22,14 +22,14 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (261-291): CHC: Assertion violation happens here. // Warning 1218: (357-387): CHC: Error trying to invoke SMT solver. -// Warning 6328: (357-387): CHC: Assertion violation might happen here. // Warning 1218: (542-572): CHC: Error trying to invoke SMT solver. -// Warning 6328: (542-572): CHC: Assertion violation might happen here. // Warning 1218: (639-669): CHC: Error trying to invoke SMT solver. -// Warning 6328: (639-669): CHC: Assertion violation might happen here. // Warning 1218: (753-783): CHC: Error trying to invoke SMT solver. +// Warning 6328: (261-291): CHC: Assertion violation happens here. +// Warning 6328: (357-387): CHC: Assertion violation might happen here. +// Warning 6328: (542-572): CHC: Assertion violation might happen here. +// Warning 6328: (639-669): CHC: Assertion violation might happen here. // Warning 6328: (753-783): CHC: Assertion violation might happen here. // Warning 4661: (357-387): BMC: Assertion violation happens here. // Warning 4661: (542-572): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/compound_bitwise_or_uint_3.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/compound_bitwise_or_uint_3.sol new file mode 100644 index 000000000..02d538d7d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/bmc_coverage/compound_bitwise_or_uint_3.sol @@ -0,0 +1,15 @@ +contract C { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } +} +// ==== +// SMTEngine: bmc +// SMTShowUnproved: no +// ---- +// Warning 2788: 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. diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol index 865ec694b..fd3b55a8c 100644 --- a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol +++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol @@ -46,12 +46,12 @@ contract C { // SMTEngine: all // ---- // Warning 1218: (693-712): CHC: Error trying to invoke SMT solver. -// Warning 6328: (693-712): CHC: Assertion violation might happen here. // Warning 1218: (716-735): CHC: Error trying to invoke SMT solver. -// Warning 6328: (716-735): CHC: Assertion violation might happen here. // Warning 1218: (739-758): CHC: Error trying to invoke SMT solver. -// Warning 6328: (739-758): CHC: Assertion violation might happen here. // Warning 1218: (762-781): CHC: Error trying to invoke SMT solver. +// Warning 6328: (693-712): CHC: Assertion violation might happen here. +// Warning 6328: (716-735): CHC: Assertion violation might happen here. +// Warning 6328: (739-758): CHC: Assertion violation might happen here. // Warning 6328: (762-781): CHC: Assertion violation might happen here. // Warning 4661: (693-712): BMC: Assertion violation happens here. // Warning 4661: (716-735): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol b/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol index 3c1777d85..22a4551c8 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol @@ -20,6 +20,5 @@ contract C { // SMTIgnoreCex: yes // ---- // Warning 4984: (113-116): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. -// Warning 4984: (113-116): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 6328: (156-170): CHC: Assertion violation happens here. // Warning 2661: (113-116): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol index 7c9ba2d5c..2437d9829 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol @@ -27,7 +27,6 @@ contract C { // SMTEngine: all // ---- // Warning 1218: (302-333): CHC: Error trying to invoke SMT solver. -// Warning 6328: (302-333): CHC: Assertion violation might happen here. // 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. diff --git a/test/libsolidity/smtCheckerTests/file_level/recursion.sol b/test/libsolidity/smtCheckerTests/file_level/recursion.sol index f461861e9..34a26d326 100644 --- a/test/libsolidity/smtCheckerTests/file_level/recursion.sol +++ b/test/libsolidity/smtCheckerTests/file_level/recursion.sol @@ -25,4 +25,3 @@ contract C { } // ==== // SMTEngine: all -// ---- diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol index 067ac0218..84fdaf87d 100644 --- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol @@ -21,5 +21,5 @@ contract A is B { // SMTEngine: all // SMTIgnoreCex: yes // ---- -// Warning 6328: (200-218): CHC: Assertion violation happens here. // Warning 4984: (171-176): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 6328: (200-218): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol index 165740218..b7cacc0f6 100644 --- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol @@ -19,5 +19,5 @@ contract A is B { // ==== // SMTEngine: all // ---- -// Warning 4984: (175-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\nTransaction trace:\nA.constructor(115792089237316195423570985008687907853269984665640564039457584007913129639935) // Warning 4984: (166-171): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639934\n\nTransaction trace:\nA.constructor(115792089237316195423570985008687907853269984665640564039457584007913129639934) +// Warning 4984: (175-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\nTransaction trace:\nA.constructor(115792089237316195423570985008687907853269984665640564039457584007913129639935) diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol index 98da0a2a6..6a2b07919 100644 --- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol @@ -29,6 +29,6 @@ contract A is B2, B1 { // SMTEngine: all // SMTIgnoreCex: yes // ---- -// Warning 4984: (209-214): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 4984: (193-198): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 4984: (209-214): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 6328: (302-318): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol b/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol index 414809209..8fd9bf9a2 100644 --- a/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol +++ b/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol @@ -14,5 +14,5 @@ contract C { // SMTEngine: all // SMTIgnoreCex: yes // ---- -// Warning 6328: (129-143): CHC: Assertion violation happens here. // Warning 4984: (82-87): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 6328: (129-143): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol index cf31fa9e5..1fe537aad 100644 --- a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol @@ -21,8 +21,8 @@ contract C{ // SMTEngine: all // ---- // Warning 5667: (37-43): Unused function parameter. Remove or comment out the variable name to silence this warning. +// Warning 6328: (49-63): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0) // Warning 6328: (105-119): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f() // Warning 6328: (137-151): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n C.g() -- internal call // Warning 6328: (187-201): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n C.g() -- internal call // Warning 6328: (212-226): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n C.g() -- internal call -// Warning 6328: (49-63): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0) diff --git a/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol index 2e934a0f2..f03e1b4eb 100644 --- a/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol @@ -21,6 +21,6 @@ contract C{ // SMTEngine: all // ---- // Warning 5667: (37-43): Unused function parameter. Remove or comment out the variable name to silence this warning. +// Warning 6328: (49-63): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0) // Warning 6328: (105-119): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f() // Warning 6328: (151-165): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n C.g() -- internal call\n C.g() -- internal call -// Warning 6328: (49-63): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0) diff --git a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol index 83f8e609c..f97bae5cd 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol @@ -28,5 +28,5 @@ contract C is B { // ==== // SMTEngine: all // ---- -// Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()\n A.v() -- internal call // Warning 6328: (62-76): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nB.f()\n A.f() -- internal call\n C.v() -- internal call +// Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()\n A.v() -- internal call diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol index f3a6393fa..f02e416a4 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol @@ -23,6 +23,6 @@ contract A is B { // SMTEngine: all // SMTIgnoreCex: yes // ---- -// Warning 6328: (243-261): CHC: Assertion violation happens here. // Warning 4984: (125-130): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 4984: (184-189): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 6328: (243-261): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol index d20358525..e223ad5f7 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol @@ -23,6 +23,6 @@ contract A is B { // SMTEngine: all // SMTIgnoreCex: yes // ---- -// Warning 6328: (241-259): CHC: Assertion violation happens here. // Warning 4984: (125-131): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 4984: (185-190): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 6328: (241-259): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol index 940ff64b3..c7c63f00f 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol @@ -25,5 +25,5 @@ contract D is B, C { // ==== // SMTEngine: all // ---- -// Warning 6328: (223-237): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nD.constructor() // Warning 6328: (134-148): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nD.constructor() +// Warning 6328: (223-237): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nD.constructor() diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol index 88fe7f51f..02a66575a 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol @@ -24,5 +24,5 @@ contract LoopFor2 { // ---- // Warning 2072: (202-217): Unused local variable. // Warning 6368: (354-358): CHC: Out of bounds access happens here. -// Warning 6368: (378-382): CHC: Out of bounds access happens here. // Warning 6368: (371-375): CHC: Out of bounds access happens here. +// Warning 6368: (378-382): CHC: Out of bounds access happens here. diff --git a/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol b/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol index dc4fc9ef1..2a2f16c47 100644 --- a/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol +++ b/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol @@ -35,4 +35,3 @@ contract C { } // ==== // SMTEngine: chc -// ---- diff --git a/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol index e617e274e..d7a309405 100644 --- a/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol +++ b/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol @@ -7,5 +7,5 @@ contract C { // SMTEngine: all // SMTIgnoreCex: yes // ---- -// Warning 4281: (77-82): CHC: Division by zero happens here. // Warning 4984: (77-82): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here. +// Warning 4281: (77-82): CHC: Division by zero happens here. diff --git a/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_2.sol b/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_2.sol index f1bcf66b6..efc59fcfc 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_2.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_2.sol @@ -14,5 +14,5 @@ contract C is A { // ==== // SMTEngine: all // ---- -// Warning 6328: (240-254): CHC: Assertion violation happens here.\nCounterexample:\nv = 1, x = 1\n\nTransaction trace:\nC.constructor(){ value: 1 } // Warning 6328: (60-74): CHC: Assertion violation happens here.\nCounterexample:\nv = 0, x = 1\n\nTransaction trace:\nC.constructor(){ value: 1 } +// Warning 6328: (240-254): CHC: Assertion violation happens here.\nCounterexample:\nv = 1, x = 1\n\nTransaction trace:\nC.constructor(){ value: 1 } diff --git a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_function_call.sol b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_function_call.sol index 10fd28ee3..7ce444357 100644 --- a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_function_call.sol +++ b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_function_call.sol @@ -11,5 +11,5 @@ contract B { // SMTEngine: all // SMTIgnoreCex: yes // ---- -// Warning 6328: (130-152): CHC: Assertion violation happens here. // Warning 6328: (104-126): CHC: Assertion violation happens here. +// Warning 6328: (130-152): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_branches_3d_show_unproved.sol b/test/libsolidity/smtCheckerTests/types/array_branches_3d_show_unproved.sol new file mode 100644 index 000000000..6ec629c9f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_branches_3d_show_unproved.sol @@ -0,0 +1,25 @@ +contract C +{ + uint[][][] c; + constructor() { + c.push(); + c[0].push(); + c[0][0].push(); + } + function f(bool b) public { + c[0][0][0] = 0; + if (b) + c[0][0][0] = 1; + assert(c[0][0][0] < 2); + } +} +// ==== +// SMTEngine: all +// SMTShowUnproved: yes +// ---- +// Warning 6368: (124-131): CHC: Out of bounds access might happen here. +// Warning 6368: (124-134): CHC: Out of bounds access might happen here. +// Warning 6368: (152-159): CHC: Out of bounds access might happen here. +// Warning 6368: (152-162): CHC: Out of bounds access might happen here. +// Warning 6368: (177-184): CHC: Out of bounds access might happen here. +// Warning 6368: (177-187): CHC: Out of bounds access might happen here. diff --git a/test/solc/CommandLineParser.cpp b/test/solc/CommandLineParser.cpp index 02444ce5d..bb427232c 100644 --- a/test/solc/CommandLineParser.cpp +++ b/test/solc/CommandLineParser.cpp @@ -82,6 +82,7 @@ BOOST_AUTO_TEST_CASE(no_options) expectedOptions.modelChecker.settings = { ModelCheckerContracts::Default(), ModelCheckerEngine::None(), + false, smtutil::SMTSolverChoice::All(), ModelCheckerTargets::Default(), nullopt, @@ -151,6 +152,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options) "--yul-optimizations=agf", "--model-checker-contracts=contract1.yul:A,contract2.yul:B", "--model-checker-engine=bmc", + "--model-checker-show-unproved=true", "--model-checker-solvers=z3,smtlib2", "--model-checker-targets=underflow,divByZero", "--model-checker-timeout=5", @@ -209,6 +211,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options) expectedOptions.modelChecker.settings = { {{{"contract1.yul", {"A"}}, {"contract2.yul", {"B"}}}}, {true, false}, + true, {false, true, true}, {{VerificationTargetType::Underflow, VerificationTargetType::DivByZero}}, 5, @@ -279,6 +282,7 @@ BOOST_AUTO_TEST_CASE(assembly_mode_options) "contract1.yul:A," "contract2.yul:B", "--model-checker-engine=bmc", // Ignored in assembly mode + "--model-checker-show-unproved=true", // Ignored in assembly mode "--model-checker-solvers=z3,smtlib2", // Ignored in assembly mode "--model-checker-targets=" // Ignored in assembly mode "underflow," @@ -377,6 +381,7 @@ BOOST_AUTO_TEST_CASE(standard_json_mode_options) "contract1.yul:A," "contract2.yul:B", "--model-checker-engine=bmc", // Ignored in Standard JSON mode + "--model-checker-show-unproved=true", // Ignored in Standard JSON mode "--model-checker-solvers=z3,smtlib2", // Ignored in Standard JSON mode "--model-checker-targets=" // Ignored in Standard JSON mode "underflow," diff --git a/test/tools/fuzzer_common.cpp b/test/tools/fuzzer_common.cpp index ef85288b0..65749a009 100644 --- a/test/tools/fuzzer_common.cpp +++ b/test/tools/fuzzer_common.cpp @@ -20,6 +20,7 @@ #include #include +#include #include @@ -104,6 +105,7 @@ void FuzzerUtil::testCompiler( compiler.setModelCheckerSettings({ frontend::ModelCheckerContracts::Default(), frontend::ModelCheckerEngine::All(), + /*showUnproved=*/false, smtutil::SMTSolverChoice::All(), frontend::ModelCheckerTargets::Default(), /*timeout=*/1