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

Merge pull request #11705 from ethereum/smt_show_unproved

Browse Source 
[SMTChecker] Bundle unproved messages by default
This commit is contained in:
Leonardo 2021-08-04 15:21:43 +02:00 committed by GitHub
commit e18dec871f
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
99 changed files with 1108 additions and 117 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -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:

8
docs/smtchecker.rst
View File

@ -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
==================

2
docs/using-the-compiler.rst
View File

@ -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.

21
libsolidity/formal/BMC.cpp
View File

@ -60,7 +60,7 @@ BMC::BMC(
#endif
}
void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<VerificationTargetType>> _solvedTargets)
void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<VerificationTargetType>, smt::EncodingContext::IdCompare> _solvedTargets)
{
if (m_interface->solvers() == 0)
{
@ -84,8 +84,21 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
m_context.setAssertionAccumulation(true);
m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
createFreeConstants(sourceDependencies(_source));
m_unprovedAmt = 0;
_source.accept(*this);
if (m_unprovedAmt > 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;

7
libsolidity/formal/BMC.h
View File

@ -66,7 +66,7 @@ public:
langutil::CharStreamProvider const& _charStreamProvider
);
void analyze(SourceUnit const& _sources, std::map<ASTNode const*, std::set<VerificationTargetType>> _solvedTargets);
void analyze(SourceUnit const& _sources, std::map<ASTNode const*, std::set<VerificationTargetType>, 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<BMCVerificationTarget> m_verificationTargets;
/// Targets that were already proven.
std::map<ASTNode const*, std::set<VerificationTargetType>> m_solvedTargets;
std::map<ASTNode const*, std::set<VerificationTargetType>, smt::EncodingContext::IdCompare> m_solvedTargets;
/// Number of verification conditions that could not be proved.
size_t m_unprovedAmt = 0;
};
}

40
libsolidity/formal/CHC.cpp
View File

@ -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
);
};
}
/**

22
libsolidity/formal/CHC.h
View File

@ -39,6 +39,8 @@
#include <libsmtutil/CHCSolverInterface.h>
#include <liblangutil/SourceLocation.h>
#include <boost/algorithm/string/join.hpp>
#include <map>
@ -62,8 +64,14 @@ public:
void analyze(SourceUnit const& _sources);
std::map<ASTNode const*, std::set<VerificationTargetType>> const& safeTargets() const { return m_safeTargets; }
std::map<ASTNode const*, std::set<VerificationTargetType>> const& unsafeTargets() const { return m_unsafeTargets; }
struct ReportTargetInfo
{
langutil::ErrorId error;
langutil::SourceLocation location;
std::string message;
};
std::map<ASTNode const*, std::set<VerificationTargetType>, smt::EncodingContext::IdCompare> const& safeTargets() const { return m_safeTargets; }
std::map<ASTNode const*, std::map<VerificationTargetType, ReportTargetInfo>, 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<unsigned, CHCVerificationTarget> m_verificationTargets;
/// Targets proven safe.
std::map<ASTNode const*, std::set<VerificationTargetType>> m_safeTargets;
/// Targets proven unsafe.
std::map<ASTNode const*, std::set<VerificationTargetType>> m_unsafeTargets;
/// Targets proved safe.
std::map<ASTNode const*, std::set<VerificationTargetType>, smt::EncodingContext::IdCompare> m_safeTargets;
/// Targets proved unsafe.
std::map<ASTNode const*, std::map<VerificationTargetType, ReportTargetInfo>, smt::EncodingContext::IdCompare> m_unsafeTargets;
/// Targets not proved.
std::map<ASTNode const*, std::map<VerificationTargetType, ReportTargetInfo>, smt::EncodingContext::IdCompare> m_unprovedTargets;
//@}
/// Control-flow.

4
libsolidity/formal/ModelChecker.cpp
View File

@ -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);

2
libsolidity/formal/ModelCheckerSettings.h
View File

@ -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<unsigned> 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;

10
libsolidity/interface/StandardCompiler.cpp
View File

@ -442,7 +442,7 @@ std::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
std::optional<Json::Value> checkModelCheckerSettingsKeys(Json::Value const& _input)
{
static set<string> keys{"contracts", "engine", "solvers", "targets", "timeout"};
static set<string> keys{"contracts", "engine", "showUnproved", "solvers", "targets", "timeout"};
return checkKeys(_input, keys, "modelChecker");
}
@ -951,6 +951,14 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> 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"];

13
solc/CommandLineParser.cpp
View File

@ -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<string>()->value_name("all,bmc,chc,none")->default_value("none"),
"Select model checker engine."
)
(
g_strModelCheckerShowUnproved.c_str(),
po::value<bool>()->value_name("false,true")->default_value(false),
"Select whether to show all unproved targets."
)
(
g_strModelCheckerSolvers.c_str(),
po::value<string>()->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<bool>();
m_options.modelChecker.settings.showUnproved = showUnproved;
}
if (m_args.count(g_strModelCheckerSolvers))
{
string solversStr = m_args[g_strModelCheckerSolvers].as<string>();
@ -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);

1
test/cmdlineTests/model_checker_show_unproved_default_all_engines/args Normal file
View File

@ -0,0 +1 @@
--model-checker-engine all

3
test/cmdlineTests/model_checker_show_unproved_default_all_engines/err Normal file
View File

@ -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.

12
test/cmdlineTests/model_checker_show_unproved_default_all_engines/input.sol Normal file
View File

@ -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);
}
}

1
test/cmdlineTests/model_checker_show_unproved_default_bmc/args Normal file
View File

@ -0,0 +1 @@
--model-checker-engine bmc

1
test/cmdlineTests/model_checker_show_unproved_default_bmc/err Normal file
View File

@ -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.

12
test/cmdlineTests/model_checker_show_unproved_default_bmc/input.sol Normal file
View File

@ -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);
}
}

1
test/cmdlineTests/model_checker_show_unproved_default_chc/args Normal file
View File

@ -0,0 +1 @@
--model-checker-engine chc

1
test/cmdlineTests/model_checker_show_unproved_default_chc/err Normal file
View File

@ -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.

12
test/cmdlineTests/model_checker_show_unproved_default_chc/input.sol Normal file
View File

@ -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);
}
}

1
test/cmdlineTests/model_checker_show_unproved_false_all_engines/args Normal file
View File

@ -0,0 +1 @@
--model-checker-engine all --model-checker-show-unproved false

3
test/cmdlineTests/model_checker_show_unproved_false_all_engines/err Normal file
View File

@ -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.

12
test/cmdlineTests/model_checker_show_unproved_false_all_engines/input.sol Normal file
View File

@ -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);
}
}

1
test/cmdlineTests/model_checker_show_unproved_false_bmc/args Normal file
View File

@ -0,0 +1 @@
--model-checker-engine bmc --model-checker-show-unproved false

1
test/cmdlineTests/model_checker_show_unproved_false_bmc/err Normal file
View File

@ -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.

12
test/cmdlineTests/model_checker_show_unproved_false_bmc/input.sol Normal file
View File

@ -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);
}
}

1
test/cmdlineTests/model_checker_show_unproved_false_chc/args Normal file
View File

@ -0,0 +1 @@
--model-checker-engine chc --model-checker-show-unproved false

1
test/cmdlineTests/model_checker_show_unproved_false_chc/err Normal file
View File

@ -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.

12
test/cmdlineTests/model_checker_show_unproved_false_chc/input.sol Normal file
View File

@ -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);
}
}

1
test/cmdlineTests/model_checker_show_unproved_true_all_engines/args Normal file
View File

@ -0,0 +1 @@
--model-checker-engine all --model-checker-show-unproved true

12
test/cmdlineTests/model_checker_show_unproved_true_all_engines/err Normal file
View File

@ -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:

12
test/cmdlineTests/model_checker_show_unproved_true_all_engines/input.sol Normal file
View File

@ -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);
}
}

1
test/cmdlineTests/model_checker_show_unproved_true_bmc/args Normal file
View File

@ -0,0 +1 @@
--model-checker-engine bmc --model-checker-show-unproved true

6
test/cmdlineTests/model_checker_show_unproved_true_bmc/err Normal file
View File

@ -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:

12
test/cmdlineTests/model_checker_show_unproved_true_bmc/input.sol Normal file
View File

@ -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);
}
}

1
test/cmdlineTests/model_checker_show_unproved_true_chc/args Normal file
View File

@ -0,0 +1 @@
--model-checker-engine chc --model-checker-show-unproved true

5
test/cmdlineTests/model_checker_show_unproved_true_chc/err Normal file
View File

@ -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);
| ^^^^^^^^^^^^^^^

12
test/cmdlineTests/model_checker_show_unproved_true_chc/input.sol Normal file
View File

@ -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);
}
}

1
test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/args Normal file
View File

@ -0,0 +1 @@
--model-checker-engine all --model-checker-show-unproved aaa

1
test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/err Normal file
View File

@ -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'

1
test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/exit Normal file
View File

@ -0,0 +1 @@
1

12
test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/input.sol Normal file
View File

@ -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);
}
}

13
test/cmdlineTests/model_checker_timeout_all/err
View File

@ -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.

7
test/cmdlineTests/model_checker_timeout_bmc/err
View File

@ -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.

6
test/cmdlineTests/model_checker_timeout_chc/err
View File

@ -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.

26
test/cmdlineTests/standard_model_checker_show_unproved_default_all_engines/input.json Normal file
View File

@ -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"
}
}
}

90
test/cmdlineTests/standard_model_checker_show_unproved_default_all_engines/output.json Normal file
View File

@ -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}}}

27
test/cmdlineTests/standard_model_checker_show_unproved_false_all_engines/input.json Normal file
View File

@ -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
}
}
}

90
test/cmdlineTests/standard_model_checker_show_unproved_false_all_engines/output.json Normal file
View File

@ -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}}}

27
test/cmdlineTests/standard_model_checker_show_unproved_false_bmc/input.json Normal file
View File

@ -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
}
}
}

88
test/cmdlineTests/standard_model_checker_show_unproved_false_bmc/output.json Normal file
View File

@ -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}}}

27
test/cmdlineTests/standard_model_checker_show_unproved_false_chc/input.json Normal file
View File

@ -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
}
}
}

3
test/cmdlineTests/standard_model_checker_show_unproved_false_chc/output.json Normal file
View File

@ -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}}}

27
test/cmdlineTests/standard_model_checker_show_unproved_true_all_engines/input.json Normal file
View File

@ -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
}
}
}

99
test/cmdlineTests/standard_model_checker_show_unproved_true_all_engines/output.json Normal file
View File

@ -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}}}

27
test/cmdlineTests/standard_model_checker_show_unproved_true_bmc/input.json Normal file
View File

@ -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
}
}
}

93
test/cmdlineTests/standard_model_checker_show_unproved_true_bmc/output.json Normal file
View File

@ -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}}}

27
test/cmdlineTests/standard_model_checker_show_unproved_true_chc/input.json Normal file
View File

@ -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
}
}
}

7
test/cmdlineTests/standard_model_checker_show_unproved_true_chc/output.json Normal file
View File

@ -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}}}

27
test/cmdlineTests/standard_model_checker_show_unproved_wrong/input.json Normal file
View File

@ -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"
}
}
}

1
test/cmdlineTests/standard_model_checker_show_unproved_wrong/output.json Normal file
View File

@ -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"}]}

15
test/cmdlineTests/standard_model_checker_timeout_all/output.json
View File

@ -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}}}

9
test/cmdlineTests/standard_model_checker_timeout_bmc/output.json
View File

@ -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}}}

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

@ -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}}}

8
test/libsolidity/SMTCheckerTest.cpp
View File

@ -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();

8
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol
View File

@ -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.

35
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal_no_unproved.sol Normal file
View File

@ -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.

6
test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol
View File

@ -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.

6
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol
View File

@ -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.

6
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol
View File

@ -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.

8
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol
View File

@ -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.

6
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol
View File

@ -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.

6
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol
View File

@ -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.

8
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol
View File

@ -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.

15
test/libsolidity/smtCheckerTests/bmc_coverage/compound_bitwise_or_uint_3.sol Normal file
View File

@ -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.

6
test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol
View File

@ -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.

1
test/libsolidity/smtCheckerTests/external_calls/external_inc.sol
View File

@ -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.

1
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol
View File

@ -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.

1
test/libsolidity/smtCheckerTests/file_level/recursion.sol
View File

@ -25,4 +25,3 @@ contract C {
}
// ====
// SMTEngine: all
// ----

2
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol
View File

@ -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)

2
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol
View File

@ -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)

2
test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol
View File

@ -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)

2
test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol
View File

@ -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

2
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol
View File

@ -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()

2
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol
View File

@ -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.

1
test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol
View File

@ -35,4 +35,3 @@ contract C {
}
// ====
// SMTEngine: chc
// ----

2
test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/special/msg_value_inheritance_2.sol
View File

@ -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 }

2
test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_function_call.sol
View File

@ -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.

25
test/libsolidity/smtCheckerTests/types/array_branches_3d_show_unproved.sol Normal file
View File

@ -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.

5
test/solc/CommandLineParser.cpp
View File

@ -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,"

2
test/tools/fuzzer_common.cpp
View File

@ -20,6 +20,7 @@
#include <libsolidity/interface/OptimiserSettings.h>
#include <libsolidity/interface/CompilerStack.h>
#include <libsolidity/formal/ModelCheckerSettings.h>
#include <libsolutil/JSON.h>
@ -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