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 #11202 from ethereum/smt_remove_pragma

Browse Source 
[SMTChecker] Deprecate pragma SMTChecker
This commit is contained in:
Leonardo 2021-04-08 21:43:31 +02:00 committed by GitHub
commit 124db22f04
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1166 changed files with 5340 additions and 5267 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -10,6 +10,7 @@ Compiler Features:
* Analysis: Properly detect circular references to the bytecode of other contracts across all function calls.
* Commandline Interface: Model checker option ``--model-checker-targets`` also accepts ``outOfBounds``.
* Low-Level Inliner: Inline ordinary jumps to small blocks and jumps to small blocks that terminate.
* SMTChecker: Deprecate ``pragma experimental SMTChecker;`` and set default model checker engine to ``none``.
* SMTChecker: Report local variables in CHC counterexamples.
* SMTChecker: Report out of bounds index access for arrays and fixed bytes.
* Standard JSON: Model checker option ``settings.modelChecker.targets`` also accepts ``outOfBounds``.

41
docs/smtchecker.rst
View File

@ -39,8 +39,17 @@ The potential warnings that the SMTChecker reports are:
- ``<failing property> happens here.``. This means that the SMTChecker proved that a certain property fails. A counterexample may be given, however in complex situations it may also not show a counterexample. This result may also be a false positive in certain cases, when the SMT encoding adds abstractions for Solidity code that is either hard or impossible to express.
- ``<failing property> might happen here``. This means that the solver could not prove either case within the given timeout. Since the result is unknown, the SMTChecker reports the potential failure for soundness. This may be solved by increasing the query timeout, but the problem might also simply be too hard for the engine to solve.
It is currently an experimental feature, therefore in order to use it you need
to enable it via :ref:`a pragma directive<smt_checker>`.
To enable the SMTChecker, you must select :ref:`which engine should run<smtchecker_engines>`,
where the default is no engine. Selecting the engine enables the SMTChecker on all files.
.. note::
Prior to Solidity 0.8.4, the default way to enable the SMTChecker was via
``pragma experimental SMTChecker;`` and only the contracts containing the
pragma would be analyzed. That pragma has been deprecated, and although it
still enables the SMTChecker for backwards compatibility, it will be removed
in Solidity 0.9.0. Note also that now using the pragma even in a single file
enables the SMTChecker for all files.
.. note::
The lack of warnings for a verification target represents an undisputed
@ -62,9 +71,8 @@ Overflow
.. code-block:: Solidity
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
pragma experimental SMTChecker;
// This may report a warning if no SMT solver is available.
contract Overflow {
uint immutable x;
@ -110,9 +118,8 @@ the SMTChecker proves that no overflow is reachable (by not reporting warnings):
.. code-block:: Solidity
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
pragma experimental SMTChecker;
// This may report a warning if no SMT solver is available.
contract Overflow {
uint immutable x;
@ -149,9 +156,8 @@ definition to see what results come out!
.. code-block:: Solidity
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
pragma experimental SMTChecker;
// This may report a warning if no SMT solver is available.
contract Monotonic {
function f(uint _x) internal pure returns (uint) {
@ -172,9 +178,8 @@ equal every element in the array.
.. code-block:: Solidity
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
pragma experimental SMTChecker;
// This may report a warning if no SMT solver is available.
contract Max {
function max(uint[] memory _a) public pure returns (uint) {
@ -206,9 +211,8 @@ For example, changing the code to
.. code-block:: Solidity
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
pragma experimental SMTChecker;
// This may report a warning if no SMT solver is available.
contract Max {
function max(uint[] memory _a) public pure returns (uint) {
@ -259,10 +263,8 @@ below.
.. code-block:: Solidity
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
pragma experimental SMTChecker;
// This may report a warning if no SMT solver is available.
contract Robot {
int x = 0;
@ -361,9 +363,8 @@ anything, including reenter the caller contract.
.. code-block:: Solidity
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
pragma experimental SMTChecker;
// This may report a warning if no SMT solver is available.
interface Unknown {
function run() external;
@ -469,6 +470,8 @@ 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.
.. _smtchecker_engines:
Model Checking Engines
======================
@ -624,8 +627,6 @@ not mean loss of proving power.
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
pragma experimental SMTChecker;
// This may report a warning if no SMT solver is available.
contract Recover
{
@ -673,8 +674,6 @@ types.
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
pragma experimental SMTChecker;
// This will report a warning
contract Aliasing
{

2
libsolidity/formal/BMC.cpp
View File

@ -61,8 +61,6 @@ BMC::BMC(
void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<VerificationTargetType>> _solvedTargets)
{
solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), "");
/// This is currently used to abort analysis of SourceUnits
/// containing file level functions or constants.
if (SMTEncoder::analyze(_source))

6
libsolidity/formal/CHC.cpp
View File

@ -76,8 +76,6 @@ CHC::CHC(
void CHC::analyze(SourceUnit const& _source)
{
solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), "");
/// This is currently used to abort analysis of SourceUnits
/// containing file level functions or constants.
if (SMTEncoder::analyze(_source))
@ -1430,10 +1428,6 @@ void CHC::verificationTargetEncountered(
return;
solAssert(m_currentContract || m_currentFunction, "");
SourceUnit const* source = m_currentContract ? sourceUnitContaining(*m_currentContract) : sourceUnitContaining(*m_currentFunction);
solAssert(source, "");
if (!source->annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
return;
bool scopeIsFunction = m_currentFunction && !m_currentFunction->isConstructor();
auto errorId = newErrorId();

39
libsolidity/formal/ModelChecker.cpp
View File

@ -21,6 +21,8 @@
#include <libsmtutil/Z3Interface.h>
#endif
#include <range/v3/algorithm/any_of.hpp>
using namespace std;
using namespace solidity;
using namespace solidity::util;
@ -34,6 +36,7 @@ ModelChecker::ModelChecker(
ReadCallback::Callback const& _smtCallback,
smtutil::SMTSolverChoice _enabledSolvers
):
m_errorReporter(_errorReporter),
m_settings(_settings),
m_context(),
m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, m_settings),
@ -41,9 +44,43 @@ ModelChecker::ModelChecker(
{
}
// TODO This should be removed for 0.9.0.
void ModelChecker::enableAllEnginesIfPragmaPresent(vector<shared_ptr<SourceUnit>> const& _sources)
{
bool hasPragma = ranges::any_of(_sources, [](auto _source) {
return _source && _source->annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker);
});
if (hasPragma)
m_settings.engine = ModelCheckerEngine::All();
}
void ModelChecker::analyze(SourceUnit const& _source)
{
if (!_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
// TODO This should be removed for 0.9.0.
if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
{
PragmaDirective const* smtPragma = nullptr;
for (auto node: _source.nodes())
if (auto pragma = dynamic_pointer_cast<PragmaDirective>(node))
if (
pragma->literals().size() >= 2 &&
pragma->literals().at(1) == "SMTChecker"
)
{
smtPragma = pragma.get();
break;
}
solAssert(smtPragma, "");
m_errorReporter.warning(
5523_error,
smtPragma->location(),
"The SMTChecker pragma has been deprecated and will be removed in the future. "
"Please use the \"model checker engine\" compiler setting to activate the SMTChecker instead. "
"If the pragma is enabled, all engines will be used."
);
}
if (m_settings.engine.none())
return;
if (m_settings.engine.chc)

5
libsolidity/formal/ModelChecker.h
View File

@ -55,6 +55,9 @@ public:
smtutil::SMTSolverChoice _enabledSolvers = smtutil::SMTSolverChoice::All()
);
// TODO This should be removed for 0.9.0.
void enableAllEnginesIfPragmaPresent(std::vector<std::shared_ptr<SourceUnit>> const& _sources);
void analyze(SourceUnit const& _sources);
/// This is used if the SMT solver is not directly linked into this binary.
@ -66,6 +69,8 @@ public:
static smtutil::SMTSolverChoice availableSolvers();
private:
langutil::ErrorReporter& m_errorReporter;
ModelCheckerSettings m_settings;
/// Stores the context of the encoding.

2
libsolidity/formal/ModelCheckerSettings.h
View File

@ -69,7 +69,7 @@ struct ModelCheckerTargets
struct ModelCheckerSettings
{
ModelCheckerEngine engine = ModelCheckerEngine::All();
ModelCheckerEngine engine = ModelCheckerEngine::None();
ModelCheckerTargets targets = ModelCheckerTargets::All();
std::optional<unsigned> timeout;
};

1
libsolidity/interface/CompilerStack.cpp
View File

@ -547,6 +547,7 @@ bool CompilerStack::analyze()
if (noErrors)
{
ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_modelCheckerSettings, m_readFile, m_enabledSMTSolvers);
modelChecker.enableAllEnginesIfPragmaPresent(applyMap(m_sourceOrder, [](Source const* _source) { return _source->ast; }));
for (Source const* source: m_sourceOrder)
if (source->ast)
modelChecker.analyze(*source->ast);

2
solc/CommandLineInterface.cpp
View File

@ -1055,7 +1055,7 @@ General Information)").c_str(),
smtCheckerOptions.add_options()
(
g_strModelCheckerEngine.c_str(),
po::value<string>()->value_name("all,bmc,chc,none")->default_value("all"),
po::value<string>()->value_name("all,bmc,chc,none")->default_value("none"),
"Select model checker engine."
)
(

4
test/cmdlineTests/model_checker_engine_all/err
View File

@ -6,7 +6,7 @@ x = 0
Transaction trace:
test.constructor()
test.f(0)
--> model_checker_engine_all/input.sol:6:3:
--> model_checker_engine_all/input.sol:5:3:
|
6 | assert(x > 0);
5 | assert(x > 0);
| ^^^^^^^^^^^^^

1
test/cmdlineTests/model_checker_engine_all/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
function f(uint x) public pure {
assert(x > 0);

4
test/cmdlineTests/model_checker_engine_bmc/err
View File

@ -1,7 +1,7 @@
Warning: BMC: Assertion violation happens here.
--> model_checker_engine_bmc/input.sol:6:3:
--> model_checker_engine_bmc/input.sol:5:3:
|
6 | assert(x > 0);
5 | assert(x > 0);
| ^^^^^^^^^^^^^
Note: Counterexample:
x = 0

1
test/cmdlineTests/model_checker_engine_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
function f(uint x) public pure {
assert(x > 0);

4
test/cmdlineTests/model_checker_engine_chc/err
View File

@ -6,7 +6,7 @@ x = 0
Transaction trace:
test.constructor()
test.f(0)
--> model_checker_engine_chc/input.sol:6:3:
--> model_checker_engine_chc/input.sol:5:3:
|
6 | assert(x > 0);
5 | assert(x > 0);
| ^^^^^^^^^^^^^

1
test/cmdlineTests/model_checker_engine_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
function f(uint x) public pure {
assert(x > 0);

1
test/cmdlineTests/model_checker_engine_none/input.sol
View File

@ -1,7 +1,6 @@
// Removed to yield a warning, otherwise CI test fails with the expectation
// "no output requested"
//pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
function f(uint x) public pure {
assert(x > 0);

2
test/cmdlineTests/model_checker_targets_all/args
View File

@ -1 +1 @@
--model-checker-targets all
--model-checker-engine all --model-checker-targets all

36
test/cmdlineTests/model_checker_targets_all/err
View File

@ -8,9 +8,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 0)
--> model_checker_targets_all/input.sol:8:3:
--> model_checker_targets_all/input.sol:7:3:
|
8 | --x;
7 | --x;
| ^^^
Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
@ -23,9 +23,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 2)
--> model_checker_targets_all/input.sol:9:3:
--> model_checker_targets_all/input.sol:8:3:
|
9 | x + type(uint).max;
8 | x + type(uint).max;
| ^^^^^^^^^^^^^^^^^^
Warning: CHC: Division by zero happens here.
@ -38,10 +38,10 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all/input.sol:10:3:
|
10 | 2 / x;
| ^^^^^
--> model_checker_targets_all/input.sol:9:3:
|
9 | 2 / x;
| ^^^^^
Warning: CHC: Assertion violation happens here.
Counterexample:
@ -53,9 +53,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all/input.sol:12:3:
--> model_checker_targets_all/input.sol:11:3:
|
12 | assert(x > 0);
11 | assert(x > 0);
| ^^^^^^^^^^^^^
Warning: CHC: Empty array "pop" happens here.
@ -68,9 +68,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all/input.sol:13:3:
--> model_checker_targets_all/input.sol:12:3:
|
13 | arr.pop();
12 | arr.pop();
| ^^^^^^^^^
Warning: CHC: Out of bounds access happens here.
@ -83,22 +83,22 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all/input.sol:14:3:
--> model_checker_targets_all/input.sol:13:3:
|
14 | arr[x];
13 | arr[x];
| ^^^^^^
Warning: BMC: Condition is always true.
--> model_checker_targets_all/input.sol:7:11:
--> model_checker_targets_all/input.sol:6:11:
|
7 | require(x >= 0);
6 | require(x >= 0);
| ^^^^^^
Note: Callstack:
Warning: BMC: Insufficient funds happens here.
--> model_checker_targets_all/input.sol:11:3:
--> model_checker_targets_all/input.sol:10:3:
|
11 | a.transfer(x);
10 | a.transfer(x);
| ^^^^^^^^^^^^^
Note: Counterexample:
a = 0

1
test/cmdlineTests/model_checker_targets_all/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

28
test/cmdlineTests/model_checker_targets_all_bmc/err
View File

@ -1,14 +1,14 @@
Warning: BMC: Condition is always true.
--> model_checker_targets_all_bmc/input.sol:7:11:
--> model_checker_targets_all_bmc/input.sol:6:11:
|
7 | require(x >= 0);
6 | require(x >= 0);
| ^^^^^^
Note: Callstack:
Warning: BMC: Underflow (resulting value less than 0) happens here.
--> model_checker_targets_all_bmc/input.sol:8:3:
--> model_checker_targets_all_bmc/input.sol:7:3:
|
8 | --x;
7 | --x;
| ^^^
Note: Counterexample:
<result> = (- 1)
@ -19,9 +19,9 @@ Note: Callstack:
Note:
Warning: BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
--> model_checker_targets_all_bmc/input.sol:9:3:
--> model_checker_targets_all_bmc/input.sol:8:3:
|
9 | x + type(uint).max;
8 | x + type(uint).max;
| ^^^^^^^^^^^^^^^^^^
Note: Counterexample:
<result> = 2**256
@ -32,10 +32,10 @@ Note: Callstack:
Note:
Warning: BMC: Division by zero happens here.
--> model_checker_targets_all_bmc/input.sol:10:3:
|
10 | 2 / x;
| ^^^^^
--> model_checker_targets_all_bmc/input.sol:9:3:
|
9 | 2 / x;
| ^^^^^
Note: Counterexample:
<result> = 0
a = 0
@ -45,9 +45,9 @@ Note: Callstack:
Note:
Warning: BMC: Insufficient funds happens here.
--> model_checker_targets_all_bmc/input.sol:11:3:
--> model_checker_targets_all_bmc/input.sol:10:3:
|
11 | a.transfer(x);
10 | a.transfer(x);
| ^^^^^^^^^^^^^
Note: Counterexample:
a = 0
@ -57,9 +57,9 @@ Note: Callstack:
Note:
Warning: BMC: Assertion violation happens here.
--> model_checker_targets_all_bmc/input.sol:12:3:
--> model_checker_targets_all_bmc/input.sol:11:3:
|
12 | assert(x > 0);
11 | assert(x > 0);
| ^^^^^^^^^^^^^
Note: Counterexample:
a = 0

1
test/cmdlineTests/model_checker_targets_all_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

28
test/cmdlineTests/model_checker_targets_all_chc/err
View File

@ -8,9 +8,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 0)
--> model_checker_targets_all_chc/input.sol:8:3:
--> model_checker_targets_all_chc/input.sol:7:3:
|
8 | --x;
7 | --x;
| ^^^
Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
@ -23,9 +23,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 2)
--> model_checker_targets_all_chc/input.sol:9:3:
--> model_checker_targets_all_chc/input.sol:8:3:
|
9 | x + type(uint).max;
8 | x + type(uint).max;
| ^^^^^^^^^^^^^^^^^^
Warning: CHC: Division by zero happens here.
@ -38,10 +38,10 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all_chc/input.sol:10:3:
|
10 | 2 / x;
| ^^^^^
--> model_checker_targets_all_chc/input.sol:9:3:
|
9 | 2 / x;
| ^^^^^
Warning: CHC: Assertion violation happens here.
Counterexample:
@ -53,9 +53,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all_chc/input.sol:12:3:
--> model_checker_targets_all_chc/input.sol:11:3:
|
12 | assert(x > 0);
11 | assert(x > 0);
| ^^^^^^^^^^^^^
Warning: CHC: Empty array "pop" happens here.
@ -68,9 +68,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all_chc/input.sol:13:3:
--> model_checker_targets_all_chc/input.sol:12:3:
|
13 | arr.pop();
12 | arr.pop();
| ^^^^^^^^^
Warning: CHC: Out of bounds access happens here.
@ -83,7 +83,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all_chc/input.sol:14:3:
--> model_checker_targets_all_chc/input.sol:13:3:
|
14 | arr[x];
13 | arr[x];
| ^^^^^^

1
test/cmdlineTests/model_checker_targets_all_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

4
test/cmdlineTests/model_checker_targets_assert_bmc/err
View File

@ -1,7 +1,7 @@
Warning: BMC: Assertion violation happens here.
--> model_checker_targets_assert_bmc/input.sol:12:3:
--> model_checker_targets_assert_bmc/input.sol:11:3:
|
12 | assert(x > 0);
11 | assert(x > 0);
| ^^^^^^^^^^^^^
Note: Counterexample:
a = 0

1
test/cmdlineTests/model_checker_targets_assert_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

4
test/cmdlineTests/model_checker_targets_assert_chc/err
View File

@ -8,7 +8,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_assert_chc/input.sol:12:3:
--> model_checker_targets_assert_chc/input.sol:11:3:
|
12 | assert(x > 0);
11 | assert(x > 0);
| ^^^^^^^^^^^^^

1
test/cmdlineTests/model_checker_targets_assert_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

4
test/cmdlineTests/model_checker_targets_balance_bmc/err
View File

@ -1,7 +1,7 @@
Warning: BMC: Insufficient funds happens here.
--> model_checker_targets_balance_bmc/input.sol:11:3:
--> model_checker_targets_balance_bmc/input.sol:10:3:
|
11 | a.transfer(x);
10 | a.transfer(x);
| ^^^^^^^^^^^^^
Note: Counterexample:
a = 0

1
test/cmdlineTests/model_checker_targets_balance_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

1
test/cmdlineTests/model_checker_targets_balance_chc/input.sol
View File

@ -1,5 +1,4 @@
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

4
test/cmdlineTests/model_checker_targets_constant_condition_bmc/err
View File

@ -1,6 +1,6 @@
Warning: BMC: Condition is always true.
--> model_checker_targets_constant_condition_bmc/input.sol:7:11:
--> model_checker_targets_constant_condition_bmc/input.sol:6:11:
|
7 | require(x >= 0);
6 | require(x >= 0);
| ^^^^^^
Note: Callstack:

1
test/cmdlineTests/model_checker_targets_constant_condition_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

1
test/cmdlineTests/model_checker_targets_constant_condition_chc/input.sol
View File

@ -1,5 +1,4 @@
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

8
test/cmdlineTests/model_checker_targets_div_by_zero_bmc/err
View File

@ -1,8 +1,8 @@
Warning: BMC: Division by zero happens here.
--> model_checker_targets_div_by_zero_bmc/input.sol:10:3:
|
10 | 2 / x;
| ^^^^^
--> model_checker_targets_div_by_zero_bmc/input.sol:9:3:
|
9 | 2 / x;
| ^^^^^
Note: Counterexample:
<result> = 0
a = 0

1
test/cmdlineTests/model_checker_targets_div_by_zero_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

8
test/cmdlineTests/model_checker_targets_div_by_zero_chc/err
View File

@ -8,7 +8,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_div_by_zero_chc/input.sol:10:3:
|
10 | 2 / x;
| ^^^^^
--> model_checker_targets_div_by_zero_chc/input.sol:9:3:
|
9 | 2 / x;
| ^^^^^

1
test/cmdlineTests/model_checker_targets_div_by_zero_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

2
test/cmdlineTests/model_checker_targets_error/args
View File

@ -1 +1 @@
--model-checker-targets aaa,bbb
--model-checker-engine all --model-checker-targets aaa,bbb

1
test/cmdlineTests/model_checker_targets_error/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

1
test/cmdlineTests/model_checker_targets_out_of_bounds_bmc/input.sol
View File

@ -1,5 +1,4 @@
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

4
test/cmdlineTests/model_checker_targets_out_of_bounds_chc/err
View File

@ -8,7 +8,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_out_of_bounds_chc/input.sol:14:3:
--> model_checker_targets_out_of_bounds_chc/input.sol:13:3:
|
14 | arr[x];
13 | arr[x];
| ^^^^^^

1
test/cmdlineTests/model_checker_targets_out_of_bounds_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

4
test/cmdlineTests/model_checker_targets_overflow_bmc/err
View File

@ -1,7 +1,7 @@
Warning: BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
--> model_checker_targets_overflow_bmc/input.sol:9:3:
--> model_checker_targets_overflow_bmc/input.sol:8:3:
|
9 | x + type(uint).max;
8 | x + type(uint).max;
| ^^^^^^^^^^^^^^^^^^
Note: Counterexample:
<result> = 2**256

1
test/cmdlineTests/model_checker_targets_overflow_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

4
test/cmdlineTests/model_checker_targets_overflow_chc/err
View File

@ -8,7 +8,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 2)
--> model_checker_targets_overflow_chc/input.sol:9:3:
--> model_checker_targets_overflow_chc/input.sol:8:3:
|
9 | x + type(uint).max;
8 | x + type(uint).max;
| ^^^^^^^^^^^^^^^^^^

1
test/cmdlineTests/model_checker_targets_overflow_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

1
test/cmdlineTests/model_checker_targets_pop_empty_bmc/input.sol
View File

@ -1,5 +1,4 @@
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

4
test/cmdlineTests/model_checker_targets_pop_empty_chc/err
View File

@ -8,7 +8,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_pop_empty_chc/input.sol:13:3:
--> model_checker_targets_pop_empty_chc/input.sol:12:3:
|
13 | arr.pop();
12 | arr.pop();
| ^^^^^^^^^

1
test/cmdlineTests/model_checker_targets_pop_empty_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

4
test/cmdlineTests/model_checker_targets_underflow_bmc/err
View File

@ -1,7 +1,7 @@
Warning: BMC: Underflow (resulting value less than 0) happens here.
--> model_checker_targets_underflow_bmc/input.sol:8:3:
--> model_checker_targets_underflow_bmc/input.sol:7:3:
|
8 | --x;
7 | --x;
| ^^^
Note: Counterexample:
<result> = (- 1)

1
test/cmdlineTests/model_checker_targets_underflow_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

4
test/cmdlineTests/model_checker_targets_underflow_chc/err
View File

@ -8,7 +8,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 0)
--> model_checker_targets_underflow_chc/input.sol:8:3:
--> model_checker_targets_underflow_chc/input.sol:7:3:
|
8 | --x;
7 | --x;
| ^^^

1
test/cmdlineTests/model_checker_targets_underflow_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

12
test/cmdlineTests/model_checker_targets_underflow_overflow_assert_bmc/err
View File

@ -1,7 +1,7 @@
Warning: BMC: Underflow (resulting value less than 0) happens here.
--> model_checker_targets_underflow_overflow_assert_bmc/input.sol:8:3:
--> model_checker_targets_underflow_overflow_assert_bmc/input.sol:7:3:
|
8 | --x;
7 | --x;
| ^^^
Note: Counterexample:
<result> = (- 1)
@ -12,9 +12,9 @@ Note: Callstack:
Note:
Warning: BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
--> model_checker_targets_underflow_overflow_assert_bmc/input.sol:9:3:
--> model_checker_targets_underflow_overflow_assert_bmc/input.sol:8:3:
|
9 | x + type(uint).max;
8 | x + type(uint).max;
| ^^^^^^^^^^^^^^^^^^
Note: Counterexample:
<result> = 2**256
@ -25,9 +25,9 @@ Note: Callstack:
Note:
Warning: BMC: Assertion violation happens here.
--> model_checker_targets_underflow_overflow_assert_bmc/input.sol:12:3:
--> model_checker_targets_underflow_overflow_assert_bmc/input.sol:11:3:
|
12 | assert(x > 0);
11 | assert(x > 0);
| ^^^^^^^^^^^^^
Note: Counterexample:
a = 0

1
test/cmdlineTests/model_checker_targets_underflow_overflow_assert_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

12
test/cmdlineTests/model_checker_targets_underflow_overflow_assert_chc/err
View File

@ -8,9 +8,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 0)
--> model_checker_targets_underflow_overflow_assert_chc/input.sol:8:3:
--> model_checker_targets_underflow_overflow_assert_chc/input.sol:7:3:
|
8 | --x;
7 | --x;
| ^^^
Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
@ -23,9 +23,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 2)
--> model_checker_targets_underflow_overflow_assert_chc/input.sol:9:3:
--> model_checker_targets_underflow_overflow_assert_chc/input.sol:8:3:
|
9 | x + type(uint).max;
8 | x + type(uint).max;
| ^^^^^^^^^^^^^^^^^^
Warning: CHC: Assertion violation happens here.
@ -38,7 +38,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_underflow_overflow_assert_chc/input.sol:12:3:
--> model_checker_targets_underflow_overflow_assert_chc/input.sol:11:3:
|
12 | assert(x > 0);
11 | assert(x > 0);
| ^^^^^^^^^^^^^

1
test/cmdlineTests/model_checker_targets_underflow_overflow_assert_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

8
test/cmdlineTests/model_checker_targets_underflow_overflow_bmc/err
View File

@ -1,7 +1,7 @@
Warning: BMC: Underflow (resulting value less than 0) happens here.
--> model_checker_targets_underflow_overflow_bmc/input.sol:8:3:
--> model_checker_targets_underflow_overflow_bmc/input.sol:7:3:
|
8 | --x;
7 | --x;
| ^^^
Note: Counterexample:
<result> = (- 1)
@ -12,9 +12,9 @@ Note: Callstack:
Note:
Warning: BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
--> model_checker_targets_underflow_overflow_bmc/input.sol:9:3:
--> model_checker_targets_underflow_overflow_bmc/input.sol:8:3:
|
9 | x + type(uint).max;
8 | x + type(uint).max;
| ^^^^^^^^^^^^^^^^^^
Note: Counterexample:
<result> = 2**256

1
test/cmdlineTests/model_checker_targets_underflow_overflow_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

8
test/cmdlineTests/model_checker_targets_underflow_overflow_chc/err
View File

@ -8,9 +8,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 0)
--> model_checker_targets_underflow_overflow_chc/input.sol:8:3:
--> model_checker_targets_underflow_overflow_chc/input.sol:7:3:
|
8 | --x;
7 | --x;
| ^^^
Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
@ -23,7 +23,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 2)
--> model_checker_targets_underflow_overflow_chc/input.sol:9:3:
--> model_checker_targets_underflow_overflow_chc/input.sol:8:3:
|
9 | x + type(uint).max;
8 | x + type(uint).max;
| ^^^^^^^^^^^^^^^^^^

1
test/cmdlineTests/model_checker_targets_underflow_overflow_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

2
test/cmdlineTests/model_checker_timeout_all/args
View File

@ -1 +1 @@
--model-checker-timeout 1000
--model-checker-engine all --model-checker-timeout 1000

16
test/cmdlineTests/model_checker_timeout_all/err
View File

@ -1,12 +1,12 @@
Warning: CHC: Assertion violation might happen here.
--> model_checker_timeout_all/input.sol:10:3:
|
10 | assert(r % k == 0);
| ^^^^^^^^^^^^^^^^^^
--> model_checker_timeout_all/input.sol:9:3:
|
9 | assert(r % k == 0);
| ^^^^^^^^^^^^^^^^^^
Warning: BMC: Assertion violation might happen here.
--> model_checker_timeout_all/input.sol:10:3:
|
10 | assert(r % k == 0);
| ^^^^^^^^^^^^^^^^^^
--> model_checker_timeout_all/input.sol:9:3:
|
9 | assert(r % k == 0);
| ^^^^^^^^^^^^^^^^^^
Note:

1
test/cmdlineTests/model_checker_timeout_all/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
function f(uint x, uint y, uint k) public pure {
require(k > 0);

8
test/cmdlineTests/model_checker_timeout_bmc/err
View File

@ -1,6 +1,6 @@
Warning: BMC: Assertion violation might happen here.
--> model_checker_timeout_bmc/input.sol:10:3:
|
10 | assert(r % k == 0);
| ^^^^^^^^^^^^^^^^^^
--> model_checker_timeout_bmc/input.sol:9:3:
|
9 | assert(r % k == 0);
| ^^^^^^^^^^^^^^^^^^
Note:

1
test/cmdlineTests/model_checker_timeout_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
function f(uint x, uint y, uint k) public pure {
require(k > 0);

8
test/cmdlineTests/model_checker_timeout_chc/err
View File

@ -1,5 +1,5 @@
Warning: CHC: Assertion violation might happen here.
--> model_checker_timeout_chc/input.sol:10:3:
|
10 | assert(r % k == 0);
| ^^^^^^^^^^^^^^^^^^
--> model_checker_timeout_chc/input.sol:9:3:
|
9 | assert(r % k == 0);
| ^^^^^^^^^^^^^^^^^^

1
test/cmdlineTests/model_checker_timeout_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
function f(uint x, uint y, uint k) public pure {
require(k > 0);

2
test/cmdlineTests/standard_model_checker_engine_all/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }"
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { function f(uint x) public pure { assert(x > 0); } }"
}
},
"settings":

2
test/cmdlineTests/standard_model_checker_engine_all/output.json
View File

@ -18,4 +18,4 @@ x = 0
Transaction trace:
C.constructor()
C.f(0)","severity":"warning","sourceLocation":{"end":150,"file":"A","start":137},"type":"Warning"}],"sources":{"A":{"id":0}}}
C.f(0)","severity":"warning","sourceLocation":{"end":119,"file":"A","start":106},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_engine_bmc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }"
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { function f(uint x) public pure { assert(x > 0); } }"
}
},
"settings":

14
test/cmdlineTests/standard_model_checker_engine_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x890f1520a8ee68790fd3c13ddbc70536dc8afcff539c4da1a1766da6168e497e":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x944140895bd672003614580050e8349baeea7cced0d8b9447aefb6c4833b02a8":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -12,14 +12,14 @@
(declare-fun |crypto_0| () |crypto_type|)
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-fun |x_4_0| () Int)
(declare-fun |x_3_0| () Int)
(declare-fun |expr_7_0| () Int)
(declare-fun |expr_8_0| () Int)
(declare-fun |expr_9_0| () Int)
(declare-fun |expr_10_1| () Bool)
(declare-fun |expr_9_1| () Bool)
(assert (and (and (and true true) (and (= expr_10_1 (> expr_8_0 expr_9_0)) (and (implies (and true true) true) (and (= expr_9_0 0) (and (implies (and true true) (and (>= expr_8_0 0) (<= expr_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_8_0 x_4_0) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (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) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))) (not expr_10_1)))
(assert (and (and (and true true) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (implies (and true true) true) (and (= expr_8_0 0) (and (implies (and true true) (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_0) (and (and (>= x_3_0 0) (<= x_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (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) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))) (not expr_9_1)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| x_4_0))
(assert (= |EVALEXPR_0| x_3_0))
(check-sat)
(get-value (|EVALEXPR_0| ))
"}},"errors":[{"component":"general","errorCode":"4661","formattedMessage":"Warning: BMC: Assertion violation happens here.
@ -35,4 +35,4 @@ Note:
","message":"BMC: Assertion violation happens here.","secondarySourceLocations":[{"message":"Counterexample:
x = 0
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":150,"file":"A","start":137},"type":"Warning"}],"sources":{"A":{"id":0}}}
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":119,"file":"A","start":106},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_engine_chc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }"
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { function f(uint x) public pure { assert(x > 0); } }"
}
},
"settings":

2
test/cmdlineTests/standard_model_checker_engine_chc/output.json
View File

@ -18,4 +18,4 @@ x = 0
Transaction trace:
C.constructor()
C.f(0)","severity":"warning","sourceLocation":{"end":150,"file":"A","start":137},"type":"Warning"}],"sources":{"A":{"id":0}}}
C.f(0)","severity":"warning","sourceLocation":{"end":119,"file":"A","start":106},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_engine_none/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }"
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { function f(uint x) public pure { assert(x > 0); } }"
}
},
"settings":

3
test/cmdlineTests/standard_model_checker_targets_all/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);
@ -23,6 +23,7 @@
{
"modelChecker":
{
"engine": "all",
"targets": "all"
}
}

136
test/cmdlineTests/standard_model_checker_targets_all/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x858035fcfc2316b3f09ebac493170a22ae2971f0f65f8ca7e125fe7f4b88756d":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x9190f95880d71b6c4636672b262f07430b161f369cc56816ad265e4fa1ee1f3a":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -13,17 +13,17 @@
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(declare-fun |expr_14_1| () Bool)
(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 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) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) expr_15_1))
(assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 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) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) (not expr_14_1)))
(check-sat)
","0xc14e92836e07964eacd7231da77dea92406ac93d4e601c33d2300d5e067bdc1f":"(set-option :produce-models true)
","0xd32caa9b049de053b56e6d79b6b17e718634bff64ba913b2f28e5369947d4e3b":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -38,71 +38,71 @@
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 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) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) (not expr_15_1)))
(check-sat)
","0xeb141c7bf753748c7972af4a35e586d579a5e374e8f2aa2455ddbdf931e5582b":"(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 ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_1| () Int)
(declare-fun |x_9_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_17_0| () Int)
(declare-fun |expr_18_1| () Int)
(declare-fun |x_8_1| () Int)
(declare-fun |expr_20_0| () Int)
(declare-fun |expr_25_1| () Int)
(declare-fun |expr_26_1| () Int)
(declare-fun |expr_27_1| () Int)
(declare-fun |expr_28_0| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_0| () Int)
(declare-fun |d_div_mod_14_0| () Int)
(declare-fun |r_div_mod_14_0| () Int)
(declare-fun |expr_31_1| () Int)
(declare-fun |expr_33_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |expr_30_1| () Int)
(declare-fun |expr_32_0| () Int)
(declare-fun |expr_35_0| () Int)
(declare-fun |state_1| () |state_type|)
(declare-fun |state_2| () |state_type|)
(declare-fun |state_3| () |state_type|)
(declare-fun |expr_39_0| () Int)
(declare-fun |expr_40_0| () Int)
(declare-fun |expr_41_0| () Int)
(declare-fun |expr_42_1| () Bool)
(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_50_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_51_0| () Int)
(declare-fun |expr_52_1| () Int)
(declare-fun |expr_41_1| () Bool)
(declare-fun |expr_44_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_44_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_49_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_50_0| () Int)
(declare-fun |expr_51_1| () Int)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_36_0 0) (<= expr_36_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_0 x_9_1) (and (implies (and true true) (and (>= expr_33_0 0) (<= expr_33_0 1461501637330902918203684832716283019655932542975))) (and (= expr_33_0 a_7_0) (and (implies (and true true) (and (>= expr_31_1 0) (<= expr_31_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_31_1 (ite (= expr_30_0 0) 0 d_div_mod_14_0)) (and (and (<= 0 r_div_mod_14_0) (or (= expr_30_0 0) (< r_div_mod_14_0 expr_30_0))) (and (= (+ (* d_div_mod_14_0 expr_30_0) r_div_mod_14_0) expr_29_0) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- expr_18_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- expr_18_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 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) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_36_0)))
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_35_0 0) (<= expr_35_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_35_0 x_8_1) (and (implies (and true true) (and (>= expr_32_0 0) (<= expr_32_0 1461501637330902918203684832716283019655932542975))) (and (= expr_32_0 a_6_0) (and (implies (and true true) (and (>= expr_30_1 0) (<= expr_30_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_1 (ite (= expr_29_0 0) 0 d_div_mod_14_0)) (and (and (<= 0 r_div_mod_14_0) (or (= expr_29_0 0) (< r_div_mod_14_0 expr_29_0))) (and (= (+ (* d_div_mod_14_0 expr_29_0) r_div_mod_14_0) expr_28_0) (and (implies (and true true) (and (>= expr_29_0 0) (<= expr_29_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_29_0 x_8_1) (and (implies (and true true) true) (and (= expr_28_0 2) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (+ expr_20_0 expr_25_1)) (and (implies (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (implies (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (implies (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 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) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_35_0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_7_0))
(assert (= |EVALEXPR_0| a_6_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| x_9_1))
(assert (= |EVALEXPR_1| x_8_1))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| ))
","0xdb117433a9ec32d2f491750fb369a0d49c0afb6cad5f9ea3e1739ef8b87cdf4f":"(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 ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 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) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) expr_14_1))
(check-sat)
"}},"errors":[{"component":"general","errorCode":"3944","formattedMessage":"Warning: CHC: Underflow (resulting value less than 0) happens here.
Counterexample:
arr = []
@ -127,7 +127,7 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 0)","severity":"warning","sourceLocation":{"end":208,"file":"A","start":205},"type":"Warning"},{"component":"general","errorCode":"4984","formattedMessage":"Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
test.f(0, 0)","severity":"warning","sourceLocation":{"end":177,"file":"A","start":174},"type":"Warning"},{"component":"general","errorCode":"4984","formattedMessage":"Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
Counterexample:
arr = []
a = 0
@ -151,7 +151,7 @@ x = 1
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 2)","severity":"warning","sourceLocation":{"end":234,"file":"A","start":216},"type":"Warning"},{"component":"general","errorCode":"4281","formattedMessage":"Warning: CHC: Division by zero happens here.
test.f(0, 2)","severity":"warning","sourceLocation":{"end":203,"file":"A","start":185},"type":"Warning"},{"component":"general","errorCode":"4281","formattedMessage":"Warning: CHC: Division by zero happens here.
Counterexample:
arr = []
a = 0
@ -175,7 +175,7 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":247,"file":"A","start":242},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
test.f(0, 1)","severity":"warning","sourceLocation":{"end":216,"file":"A","start":211},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
Counterexample:
arr = []
a = 0
@ -199,7 +199,7 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":276},"type":"Warning"},{"component":"general","errorCode":"2529","formattedMessage":"Warning: CHC: Empty array \"pop\" happens here.
test.f(0, 1)","severity":"warning","sourceLocation":{"end":258,"file":"A","start":245},"type":"Warning"},{"component":"general","errorCode":"2529","formattedMessage":"Warning: CHC: Empty array \"pop\" happens here.
Counterexample:
arr = []
a = 0
@ -223,7 +223,7 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":306,"file":"A","start":297},"type":"Warning"},{"component":"general","errorCode":"6368","formattedMessage":"Warning: CHC: Out of bounds access happens here.
test.f(0, 1)","severity":"warning","sourceLocation":{"end":275,"file":"A","start":266},"type":"Warning"},{"component":"general","errorCode":"6368","formattedMessage":"Warning: CHC: Out of bounds access happens here.
Counterexample:
arr = []
a = 0
@ -247,14 +247,14 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":320,"file":"A","start":314},"type":"Warning"},{"component":"general","errorCode":"6838","formattedMessage":"Warning: BMC: Condition is always true.
test.f(0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":283},"type":"Warning"},{"component":"general","errorCode":"6838","formattedMessage":"Warning: BMC: Condition is always true.
--> A:7:15:
|
7 | \t\t\t\t\t\trequire(x >= 0);
| \t\t\t\t\t\t ^^^^^^
Note: Callstack:
","message":"BMC: Condition is always true.","secondarySourceLocations":[{"message":"Callstack:"}],"severity":"warning","sourceLocation":{"end":196,"file":"A","start":190},"type":"Warning"},{"component":"general","errorCode":"1236","formattedMessage":"Warning: BMC: Insufficient funds happens here.
","message":"BMC: Condition is always true.","secondarySourceLocations":[{"message":"Callstack:"}],"severity":"warning","sourceLocation":{"end":165,"file":"A","start":159},"type":"Warning"},{"component":"general","errorCode":"1236","formattedMessage":"Warning: BMC: Insufficient funds happens here.
--> A:11:7:
|
11 | \t\t\t\t\t\ta.transfer(x);
@ -269,4 +269,4 @@ Note:
","message":"BMC: Insufficient funds happens here.","secondarySourceLocations":[{"message":"Counterexample:
a = 0
x = 0
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":268,"file":"A","start":255},"type":"Warning"}],"sources":{"A":{"id":0}}}
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":237,"file":"A","start":224},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_targets_all_bmc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

388
test/cmdlineTests/standard_model_checker_targets_all_bmc/output.json
View File

File diff suppressed because one or more lines are too long

2
test/cmdlineTests/standard_model_checker_targets_all_chc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

12
test/cmdlineTests/standard_model_checker_targets_all_chc/output.json
View File

@ -22,7 +22,7 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 0)","severity":"warning","sourceLocation":{"end":208,"file":"A","start":205},"type":"Warning"},{"component":"general","errorCode":"4984","formattedMessage":"Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
test.f(0, 0)","severity":"warning","sourceLocation":{"end":177,"file":"A","start":174},"type":"Warning"},{"component":"general","errorCode":"4984","formattedMessage":"Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
Counterexample:
arr = []
a = 0
@ -46,7 +46,7 @@ x = 1
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 2)","severity":"warning","sourceLocation":{"end":234,"file":"A","start":216},"type":"Warning"},{"component":"general","errorCode":"4281","formattedMessage":"Warning: CHC: Division by zero happens here.
test.f(0, 2)","severity":"warning","sourceLocation":{"end":203,"file":"A","start":185},"type":"Warning"},{"component":"general","errorCode":"4281","formattedMessage":"Warning: CHC: Division by zero happens here.
Counterexample:
arr = []
a = 0
@ -70,7 +70,7 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":247,"file":"A","start":242},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
test.f(0, 1)","severity":"warning","sourceLocation":{"end":216,"file":"A","start":211},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
Counterexample:
arr = []
a = 0
@ -94,7 +94,7 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":276},"type":"Warning"},{"component":"general","errorCode":"2529","formattedMessage":"Warning: CHC: Empty array \"pop\" happens here.
test.f(0, 1)","severity":"warning","sourceLocation":{"end":258,"file":"A","start":245},"type":"Warning"},{"component":"general","errorCode":"2529","formattedMessage":"Warning: CHC: Empty array \"pop\" happens here.
Counterexample:
arr = []
a = 0
@ -118,7 +118,7 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":306,"file":"A","start":297},"type":"Warning"},{"component":"general","errorCode":"6368","formattedMessage":"Warning: CHC: Out of bounds access happens here.
test.f(0, 1)","severity":"warning","sourceLocation":{"end":275,"file":"A","start":266},"type":"Warning"},{"component":"general","errorCode":"6368","formattedMessage":"Warning: CHC: Out of bounds access happens here.
Counterexample:
arr = []
a = 0
@ -142,4 +142,4 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":320,"file":"A","start":314},"type":"Warning"}],"sources":{"A":{"id":0}}}
test.f(0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":283},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_targets_assert_bmc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

56
test/cmdlineTests/standard_model_checker_targets_assert_bmc/output.json
View File

File diff suppressed because one or more lines are too long

2
test/cmdlineTests/standard_model_checker_targets_assert_chc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

2
test/cmdlineTests/standard_model_checker_targets_assert_chc/output.json
View File

@ -22,4 +22,4 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":276},"type":"Warning"}],"sources":{"A":{"id":0}}}
test.f(0, 1)","severity":"warning","sourceLocation":{"end":258,"file":"A","start":245},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_targets_balance_bmc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

56
test/cmdlineTests/standard_model_checker_targets_balance_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0xecb8a634d43c6b3fa690c2fec3a4763042a115cb28580d86760b27cbb849cd95":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x3b3d90fa6754444a847a9b6f723e98fc3c8b428cb56d50a010bc2c435aa1bc10":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -13,44 +13,44 @@
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_1| () Int)
(declare-fun |x_9_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_17_0| () Int)
(declare-fun |expr_18_1| () Int)
(declare-fun |x_8_1| () Int)
(declare-fun |expr_20_0| () Int)
(declare-fun |expr_25_1| () Int)
(declare-fun |expr_26_1| () Int)
(declare-fun |expr_27_1| () Int)
(declare-fun |expr_28_0| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_31_1| () Int)
(declare-fun |expr_33_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |expr_30_1| () Int)
(declare-fun |expr_32_0| () Int)
(declare-fun |expr_35_0| () Int)
(declare-fun |state_1| () |state_type|)
(declare-fun |state_2| () |state_type|)
(declare-fun |state_3| () |state_type|)
(declare-fun |expr_39_0| () Int)
(declare-fun |expr_40_0| () Int)
(declare-fun |expr_41_0| () Int)
(declare-fun |expr_42_1| () Bool)
(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_50_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_51_0| () Int)
(declare-fun |expr_52_1| () Int)
(declare-fun |expr_41_1| () Bool)
(declare-fun |expr_44_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_44_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_49_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_50_0| () Int)
(declare-fun |expr_51_1| () Int)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_36_0 0) (<= expr_36_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_0 x_9_1) (and (implies (and true true) (and (>= expr_33_0 0) (<= expr_33_0 1461501637330902918203684832716283019655932542975))) (and (= expr_33_0 a_7_0) (and (implies (and true true) (and (>= expr_31_1 0) (<= expr_31_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_31_1 (ite (= expr_30_0 0) 0 d_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_30_0 0) (< r_div_mod_0_0 expr_30_0))) (and (= (+ (* d_div_mod_0_0 expr_30_0) r_div_mod_0_0) expr_29_0) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- expr_18_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- expr_18_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 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) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_36_0)))
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_35_0 0) (<= expr_35_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_35_0 x_8_1) (and (implies (and true true) (and (>= expr_32_0 0) (<= expr_32_0 1461501637330902918203684832716283019655932542975))) (and (= expr_32_0 a_6_0) (and (implies (and true true) (and (>= expr_30_1 0) (<= expr_30_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_1 (ite (= expr_29_0 0) 0 d_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_29_0 0) (< r_div_mod_0_0 expr_29_0))) (and (= (+ (* d_div_mod_0_0 expr_29_0) r_div_mod_0_0) expr_28_0) (and (implies (and true true) (and (>= expr_29_0 0) (<= expr_29_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_29_0 x_8_1) (and (implies (and true true) true) (and (= expr_28_0 2) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (+ expr_20_0 expr_25_1)) (and (implies (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (implies (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (implies (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 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) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_35_0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_7_0))
(assert (= |EVALEXPR_0| a_6_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| x_9_1))
(assert (= |EVALEXPR_1| x_8_1))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| ))
"}},"errors":[{"component":"general","errorCode":"1236","formattedMessage":"Warning: BMC: Insufficient funds happens here.
@ -68,4 +68,4 @@ Note:
","message":"BMC: Insufficient funds happens here.","secondarySourceLocations":[{"message":"Counterexample:
a = 0
x = 0
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":268,"file":"A","start":255},"type":"Warning"}],"sources":{"A":{"id":0}}}
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":237,"file":"A","start":224},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_targets_balance_chc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

2
test/cmdlineTests/standard_model_checker_targets_constantCondition_bmc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

34
test/cmdlineTests/standard_model_checker_targets_constantCondition_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x858035fcfc2316b3f09ebac493170a22ae2971f0f65f8ca7e125fe7f4b88756d":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x9190f95880d71b6c4636672b262f07430b161f369cc56816ad265e4fa1ee1f3a":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -13,17 +13,17 @@
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(declare-fun |expr_14_1| () Bool)
(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 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) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) expr_15_1))
(assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 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) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) (not expr_14_1)))
(check-sat)
","0xc14e92836e07964eacd7231da77dea92406ac93d4e601c33d2300d5e067bdc1f":"(set-option :produce-models true)
","0xdb117433a9ec32d2f491750fb369a0d49c0afb6cad5f9ea3e1739ef8b87cdf4f":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -38,15 +38,15 @@
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(declare-fun |expr_14_1| () Bool)
(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 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) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) (not expr_15_1)))
(assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 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) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) expr_14_1))
(check-sat)
"}},"errors":[{"component":"general","errorCode":"6838","formattedMessage":"Warning: BMC: Condition is always true.
--> A:7:15:
@ -55,4 +55,4 @@
| \t\t\t\t\t\t ^^^^^^
Note: Callstack:
","message":"BMC: Condition is always true.","secondarySourceLocations":[{"message":"Callstack:"}],"severity":"warning","sourceLocation":{"end":196,"file":"A","start":190},"type":"Warning"}],"sources":{"A":{"id":0}}}
","message":"BMC: Condition is always true.","secondarySourceLocations":[{"message":"Callstack:"}],"severity":"warning","sourceLocation":{"end":165,"file":"A","start":159},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_targets_constantCondition_chc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

2
test/cmdlineTests/standard_model_checker_targets_div_by_zero_bmc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

58
test/cmdlineTests/standard_model_checker_targets_div_by_zero_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x5b98fbb121c58b139f0f8baa8e153dfeb0a4621f789bf1cbbc586298bcae48e1":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x3d72a9e21e83263eacaad9b3eaa387b10f1219c1727796d9e946ddce1e99f5a3":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -13,46 +13,46 @@
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_1| () Int)
(declare-fun |x_9_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_17_0| () Int)
(declare-fun |expr_18_1| () Int)
(declare-fun |x_8_1| () Int)
(declare-fun |expr_20_0| () Int)
(declare-fun |expr_25_1| () Int)
(declare-fun |expr_26_1| () Int)
(declare-fun |expr_27_1| () Int)
(declare-fun |expr_28_0| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_31_1| () Int)
(declare-fun |expr_33_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |expr_30_1| () Int)
(declare-fun |expr_32_0| () Int)
(declare-fun |expr_35_0| () Int)
(declare-fun |state_1| () |state_type|)
(declare-fun |state_2| () |state_type|)
(declare-fun |state_3| () |state_type|)
(declare-fun |expr_39_0| () Int)
(declare-fun |expr_40_0| () Int)
(declare-fun |expr_41_0| () Int)
(declare-fun |expr_42_1| () Bool)
(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_50_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_51_0| () Int)
(declare-fun |expr_52_1| () Int)
(declare-fun |expr_41_1| () Bool)
(declare-fun |expr_44_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_44_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_49_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_50_0| () Int)
(declare-fun |expr_51_1| () Int)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- expr_18_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- expr_18_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 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) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))) (= expr_30_0 0)))
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_29_0 0) (<= expr_29_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_29_0 x_8_1) (and (implies (and true true) true) (and (= expr_28_0 2) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (+ expr_20_0 expr_25_1)) (and (implies (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (implies (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (implies (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 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) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))) (= expr_29_0 0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_7_0))
(assert (= |EVALEXPR_0| a_6_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| x_9_1))
(assert (= |EVALEXPR_1| x_8_1))
(declare-const |EVALEXPR_2| Int)
(assert (= |EVALEXPR_2| expr_30_0))
(assert (= |EVALEXPR_2| expr_29_0))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
"}},"errors":[{"component":"general","errorCode":"3046","formattedMessage":"Warning: BMC: Division by zero happens here.
@ -72,4 +72,4 @@ Note:
<result> = 0
a = 0
x = 0
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":247,"file":"A","start":242},"type":"Warning"}],"sources":{"A":{"id":0}}}
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":216,"file":"A","start":211},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

2
test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/output.json
View File

@ -22,4 +22,4 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":247,"file":"A","start":242},"type":"Warning"}],"sources":{"A":{"id":0}}}
test.f(0, 1)","severity":"warning","sourceLocation":{"end":216,"file":"A","start":211},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_targets_out_of_bounds_bmc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

2
test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

2
test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/output.json
View File

@ -22,4 +22,4 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":320,"file":"A","start":314},"type":"Warning"}],"sources":{"A":{"id":0}}}
test.f(0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":283},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_targets_overflow_bmc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

58
test/cmdlineTests/standard_model_checker_targets_overflow_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0xce4156c685d481fe03752262b478cd8877739dba34535f7bfec42a2d30d45445":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x7b2c4d6761f5d49a4a2e0ba56b832d235e93abf16fe2a1383a526aa4fb4fe028":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -13,46 +13,46 @@
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_1| () Int)
(declare-fun |x_9_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_17_0| () Int)
(declare-fun |expr_18_1| () Int)
(declare-fun |x_8_1| () Int)
(declare-fun |expr_20_0| () Int)
(declare-fun |expr_25_1| () Int)
(declare-fun |expr_26_1| () Int)
(declare-fun |expr_27_1| () Int)
(declare-fun |expr_28_0| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_31_1| () Int)
(declare-fun |expr_33_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |expr_30_1| () Int)
(declare-fun |expr_32_0| () Int)
(declare-fun |expr_35_0| () Int)
(declare-fun |state_1| () |state_type|)
(declare-fun |state_2| () |state_type|)
(declare-fun |state_3| () |state_type|)
(declare-fun |expr_39_0| () Int)
(declare-fun |expr_40_0| () Int)
(declare-fun |expr_41_0| () Int)
(declare-fun |expr_42_1| () Bool)
(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_50_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_51_0| () Int)
(declare-fun |expr_52_1| () Int)
(declare-fun |expr_41_1| () Bool)
(declare-fun |expr_44_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_44_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_49_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_50_0| () Int)
(declare-fun |expr_51_1| () Int)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- expr_18_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- expr_18_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 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) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))) (> (+ expr_21_0 expr_26_1) 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (implies (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (implies (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 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) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))) (> (+ expr_20_0 expr_25_1) 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_7_0))
(assert (= |EVALEXPR_0| a_6_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| x_9_1))
(assert (= |EVALEXPR_1| x_8_1))
(declare-const |EVALEXPR_2| Int)
(assert (= |EVALEXPR_2| (+ expr_21_0 expr_26_1)))
(assert (= |EVALEXPR_2| (+ expr_20_0 expr_25_1)))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
"}},"errors":[{"component":"general","errorCode":"2661","formattedMessage":"Warning: BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
@ -72,4 +72,4 @@ Note:
<result> = 2**256
a = 0
x = 1
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":234,"file":"A","start":216},"type":"Warning"}],"sources":{"A":{"id":0}}}
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":203,"file":"A","start":185},"type":"Warning"}],"sources":{"A":{"id":0}}}

Some files were not shown because too many files have changed in this diff Show More