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 #11828 from ethereum/smt_chc_balance

Browse Source 
[SMTChecker] Add proper constraints on the contract's balance
This commit is contained in:
Leonardo 2021-08-25 22:02:49 +02:00 committed by GitHub
commit 208cf6a3c1
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
103 changed files with 805 additions and 284 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -6,6 +6,7 @@ Language Features:
Compiler Features:
* Immutable variables can be read at construction time once they are initialized.
* SMTChecker: Support low level ``call`` as external calls to unknown code.
* SMTChecker: Add constraints to better correlate ``address(this).balance`` and ``msg.value``.
Bugfixes:

23
docs/smtchecker.rst
View File

@ -830,6 +830,25 @@ are located in storage, even though they also have type ``uint[]``. However,
if ``d`` was assigned, we would need to clear knowledge about ``array`` and
vice-versa.
Contract Balance
================
A contract may be deployed with funds sent to it, if ``msg.value`` > 0 in the
deployment transaction.
However, the contract's address may already have funds before deployment,
which are kept by the contract.
Therefore, the SMTChecker assumes that ``address(this).balance >= msg.value``
in the constructor in order to be consistent with the EVM rules.
The contract's balance may also increase without triggering any calls to the
contract, if
- ``selfdestruct`` is executed by another contract with the analyzed contract
as the target of the remaining funds,
- the contract is the coinbase (i.e., ``block.coinbase``) of some block.
To model this properly, the SMTChecker assumes that at every new transaction
the contract's balance may grow by at least ``msg.value``.
**********************
Real World Assumptions
**********************
@ -841,3 +860,7 @@ push: If the ``push`` operation is applied to an array of length 2^256 - 1, its
length silently overflows.
However, this is unlikely to happen in practice, since the operations required
to grow the array to that point would take billions of years to execute.
Another similar assumption taken by the SMTChecker is that an address' balance
can never overflow.
A similar idea was presented in `EIP-1985 <https://eips.ethereum.org/EIPS/eip-1985>`_.

12
libsmtutil/Sorts.h
View File

@ -159,7 +159,15 @@ struct TupleSort: public Sort
name(std::move(_name)),
members(std::move(_members)),
components(std::move(_components))
{}
{
for (size_t i = 0; i < members.size(); ++i)
memberToIndex[members.at(i)] = i;
}
SortPointer memberSort(std::string const& _member)
{
return components.at(memberToIndex.at(_member));
}
bool operator==(Sort const& _other) const override
{
@ -186,8 +194,10 @@ struct TupleSort: public Sort
std::string const name;
std::vector<std::string> const members;
std::vector<SortPointer> const components;
std::map<std::string, size_t> memberToIndex;
};
/** Frequently used sorts.*/
struct SortProvider
{

77
libsolidity/formal/CHC.cpp
View File

@ -169,7 +169,13 @@ void CHC::endVisit(ContractDefinition const& _contract)
smtutil::Expression zeroes(true);
for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract))
zeroes = zeroes && currentValue(*var) == smt::zeroValue(var->type());
addRule(smtutil::Expression::implies(initialConstraints(_contract) && zeroes, predicate(entry)), entry.functor().name);
// The contract's address might already have funds before deployment,
// so the balance must be at least `msg.value`, but not equals.
auto initialBalanceConstraint = state().balance(state().thisAddress()) >= state().txMember("msg.value");
addRule(smtutil::Expression::implies(
initialConstraints(_contract) && zeroes && initialBalanceConstraint,
predicate(entry)
), entry.functor().name);
setCurrentBlock(entry);
solAssert(!m_errorDest, "");
@ -315,11 +321,16 @@ void CHC::endVisit(FunctionDefinition const& _function)
shouldAnalyze(*m_currentContract)
)
{
auto sum = summary(_function);
defineExternalFunctionInterface(_function, *m_currentContract);
setCurrentBlock(*m_interfaces.at(m_currentContract));
// Create the rule
// interface \land externalFunctionEntry => interface'
auto ifacePre = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context);
auto txConstraints = state().txTypeConstraints() && state().txFunctionConstraints(_function);
m_queryPlaceholders[&_function].push_back({txConstraints && sum, errorFlag().currentValue(), ifacePre});
connectBlocks(ifacePre, interface(), txConstraints && sum && errorFlag().currentValue() == 0);
auto sum = externalSummary(_function);
m_queryPlaceholders[&_function].push_back({sum, errorFlag().currentValue(), ifacePre});
connectBlocks(ifacePre, interface(), sum && errorFlag().currentValue() == 0);
}
m_currentFunction = nullptr;
@ -949,6 +960,7 @@ void CHC::resetSourceAnalysis()
m_queryPlaceholders.clear();
m_callGraph.clear();
m_summaries.clear();
m_externalSummaries.clear();
m_interfaces.clear();
m_nondetInterfaces.clear();
m_constructorSummaries.clear();
@ -1128,6 +1140,8 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
if (!function->isConstructor() && function->isPublic() && resolved.count(function))
{
m_externalSummaries[contract].emplace(function, createSummaryBlock(*function, *contract));
auto state1 = stateVariablesAtIndex(1, *contract);
auto state2 = stateVariablesAtIndex(2, *contract);
@ -1144,12 +1158,41 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }) +
applyMap(function->returnParameters(), [this](auto _var) { return valueAtIndex(*_var, 1); });
connectBlocks(nondetPre, nondetPost, errorPre == 0 && (*m_summaries.at(contract).at(function))(args));
connectBlocks(nondetPre, nondetPost, errorPre == 0 && (*m_externalSummaries.at(contract).at(function))(args));
}
}
}
}
void CHC::defineExternalFunctionInterface(FunctionDefinition const& _function, ContractDefinition const& _contract)
{
// Create a rule that represents an external call to this function.
// This contains more things than the function body itself,
// such as balance updates because of ``msg.value``.
auto functionEntryBlock = createBlock(&_function, PredicateType::FunctionBlock);
auto functionPred = predicate(*functionEntryBlock);
addRule(functionPred, functionPred.name);
setCurrentBlock(*functionEntryBlock);
m_context.addAssertion(initialConstraints(_contract, &_function));
m_context.addAssertion(state().txTypeConstraints() && state().txFunctionConstraints(_function));
// The contract may have received funds through a selfdestruct or
// block.coinbase, which do not trigger calls into the contract.
// So the only constraint we can add here is that the balance of
// the contract grows by at least `msg.value`.
SymbolicIntVariable k{TypeProvider::uint256(), TypeProvider::uint256(), "funds_" + to_string(m_context.newUniqueId()), m_context};
m_context.addAssertion(k.currentValue() >= state().txMember("msg.value"));
// Assume that address(this).balance cannot overflow.
m_context.addAssertion(smt::symbolicUnknownConstraints(state().balance(state().thisAddress()) + k.currentValue(), TypeProvider::uint256()));
state().addBalance(state().thisAddress(), k.currentValue());
errorFlag().increaseIndex();
m_context.addAssertion(summaryCall(_function));
connectBlocks(functionPred, externalSummary(_function));
}
void CHC::defineContractInitializer(ContractDefinition const& _contract, ContractDefinition const& _contextContract)
{
m_contractInitializers[&_contextContract][&_contract] = createConstructorBlock(_contract, "contract_initializer");
@ -1220,12 +1263,34 @@ smtutil::Expression CHC::summary(FunctionDefinition const& _function, ContractDe
return smt::function(*m_summaries.at(&_contract).at(&_function), &_contract, m_context);
}
smtutil::Expression CHC::summaryCall(FunctionDefinition const& _function, ContractDefinition const& _contract)
{
return smt::functionCall(*m_summaries.at(&_contract).at(&_function), &_contract, m_context);
}
smtutil::Expression CHC::externalSummary(FunctionDefinition const& _function, ContractDefinition const& _contract)
{
return smt::function(*m_externalSummaries.at(&_contract).at(&_function), &_contract, m_context);
}
smtutil::Expression CHC::summary(FunctionDefinition const& _function)
{
solAssert(m_currentContract, "");
return summary(_function, *m_currentContract);
}
smtutil::Expression CHC::summaryCall(FunctionDefinition const& _function)
{
solAssert(m_currentContract, "");
return summaryCall(_function, *m_currentContract);
}
smtutil::Expression CHC::externalSummary(FunctionDefinition const& _function)
{
solAssert(m_currentContract, "");
return externalSummary(_function, *m_currentContract);
}
Predicate const* CHC::createBlock(ASTNode const* _node, PredicateType _predType, string const& _prefix)
{
auto block = createSymbolicBlock(

16
libsolidity/formal/CHC.h
View File

@ -164,6 +164,12 @@ private:
/// in a given _source.
void defineInterfacesAndSummaries(SourceUnit const& _source);
/// Creates the rule
/// summary_function \land transaction_entry_constraints => external_summary_function
/// This is needed to add these transaction entry constraints which include
/// potential balance increase by external means, for example.
void defineExternalFunctionInterface(FunctionDefinition const& _function, ContractDefinition const& _contract);
/// Creates a CHC system that, for a given contract,
/// - initializes its state variables (as 0 or given value, if any).
/// - "calls" the explicit constructor function of the contract, if any.
@ -225,6 +231,13 @@ private:
/// @returns a predicate that defines a function summary.
smtutil::Expression summary(FunctionDefinition const& _function);
smtutil::Expression summary(FunctionDefinition const& _function, ContractDefinition const& _contract);
/// @returns a predicate that applies a function summary
/// over the constrained variables.
smtutil::Expression summaryCall(FunctionDefinition const& _function);
smtutil::Expression summaryCall(FunctionDefinition const& _function, ContractDefinition const& _contract);
/// @returns a predicate that defines an external function summary.
smtutil::Expression externalSummary(FunctionDefinition const& _function);
smtutil::Expression externalSummary(FunctionDefinition const& _function, ContractDefinition const& _contract);
//@}
/// Solver related.
@ -317,6 +330,9 @@ private:
/// Function predicates.
std::map<ContractDefinition const*, std::map<FunctionDefinition const*, Predicate const*>> m_summaries;
/// External function predicates.
std::map<ContractDefinition const*, std::map<FunctionDefinition const*, Predicate const*>> m_externalSummaries;
//@}
/// Variables.

4
libsolidity/formal/SMTEncoder.cpp
View File

@ -2283,9 +2283,7 @@ void SMTEncoder::resetStorageVariables()
void SMTEncoder::resetBalances()
{
// TODO this should be changed to `balances` only
// when `state` gets more members.
state().newState();
state().newBalances();
}
void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl)

28
libsolidity/formal/SymbolicState.cpp
View File

@ -104,6 +104,14 @@ smtutil::Expression SymbolicState::blockhash(smtutil::Expression _blockNumber) c
return smtutil::Expression::select(m_tx.member("blockhash"), move(_blockNumber));
}
void SymbolicState::newBalances()
{
auto tupleSort = dynamic_pointer_cast<TupleSort>(stateSort());
auto balanceSort = tupleSort->components.at(tupleSort->memberToIndex.at("balances"));
SymbolicVariable newBalances(balanceSort, "fresh_balances_" + to_string(m_context.newUniqueId()), m_context);
m_state.assignMember("balances", newBalances.currentValue());
}
void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value)
{
unsigned indexBefore = m_state.index();
@ -121,6 +129,16 @@ void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to,
m_context.addAssertion(m_state.value() == newState);
}
void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value)
{
auto newBalances = smtutil::Expression::store(
balances(),
_address,
balance(_address) + move(_value)
);
m_state.assignMember("balances", newBalances);
}
smtutil::Expression SymbolicState::txMember(string const& _member) const
{
return m_tx.member(_member);
@ -181,16 +199,6 @@ void SymbolicState::prepareForSourceUnit(SourceUnit const& _source)
/// Private helpers.
void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value)
{
auto newBalances = smtutil::Expression::store(
balances(),
_address,
balance(_address) + move(_value)
);
m_state.assignMember("balances", newBalances);
}
void SymbolicState::buildABIFunctions(set<FunctionCall const*> const& _abiFunctions)
{
map<string, SortPointer> functions;

8
libsolidity/formal/SymbolicState.h
View File

@ -108,6 +108,8 @@ public:
smtutil::Expression state(unsigned _idx) const { return m_state.value(_idx); }
smtutil::SortPointer const& stateSort() const { return m_state.sort(); }
void newState() { m_state.newVar(); }
void newBalances();
/// @returns the symbolic balances.
smtutil::Expression balances() const;
/// @returns the symbolic balance of address `this`.
@ -117,6 +119,9 @@ public:
/// Transfer _value from _from to _to.
void transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value);
/// Adds _value to _account's balance.
void addBalance(smtutil::Expression _account, smtutil::Expression _value);
//@}
/// Transaction data.
@ -163,9 +168,6 @@ public:
//@}
private:
/// Adds _value to _account's balance.
void addBalance(smtutil::Expression _account, smtutil::Expression _value);
/// Builds m_abi based on the abi.* calls _abiFunctions.
void buildABIFunctions(std::set<FunctionCall const*> const& _abiFunctions);

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

@ -24,7 +24,7 @@
(assert (= |EVALEXPR_0| x_3_0))
(check-sat)
(get-value (|EVALEXPR_0| ))
","0xa51d18d2c7cb0481228dd7dd4e7debb5d54580595265d16f67b236faa98f4862":"(set-logic HORN)
","0x4e70784a8a93c7429a716aa8b778f3de5d1f63b30158452534da5d44e5967d2b":"(set-logic HORN)
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
@ -41,98 +41,110 @@
(declare-fun |summary_3_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
(declare-fun |summary_4_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
(=> (and (and (nondet_interface_1_C_14_0 error_0 this_0 abi_0 crypto_0 state_0 state_1) true) (and (= error_0 0) (summary_3_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 x_3_0 state_2 x_3_1))) (nondet_interface_1_C_14_0 error_1 this_0 abi_0 crypto_0 state_0 state_2))))
(=> (and (and (nondet_interface_1_C_14_0 error_0 this_0 abi_0 crypto_0 state_0 state_1) true) (and (= error_0 0) (summary_4_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 x_3_0 state_2 x_3_1))) (nondet_interface_1_C_14_0 error_1 this_0 abi_0 crypto_0 state_0 state_2))))
(declare-fun |block_4_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
(declare-fun |block_5_f_12_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
(declare-fun |block_5_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
(declare-fun |block_6_f_12_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
(block_4_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)))
(block_5_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)))
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
(=> (and (and (block_4_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= x_3_1 x_3_0))) true)) true) (block_5_f_12_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
(=> (and (and (block_5_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= x_3_1 x_3_0))) true)) true) (block_6_f_12_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
(declare-fun |block_6_return_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
(declare-fun |block_7_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
(declare-fun |block_7_return_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
(declare-fun |block_8_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
(=> (and (and (block_5_f_12_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 0) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_1) (and (and (>= x_3_1 0) (<= x_3_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))))))) (and (not expr_9_1) (= error_1 1))) (block_7_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
(=> (and (and (block_6_f_12_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 0) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_1) (and (and (>= x_3_1 0) (<= x_3_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))))))) (and (not expr_9_1) (= error_1 1))) (block_8_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
(=> (block_7_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (summary_3_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
(=> (block_8_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (summary_3_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
(=> (and (and (block_5_f_12_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (= error_1 error_0) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 0) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_1) (and (and (>= x_3_1 0) (<= x_3_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true)))))))) true) (block_6_return_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
(=> (and (and (block_6_f_12_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (= error_1 error_0) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 0) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_1) (and (and (>= x_3_1 0) (<= x_3_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true)))))))) true) (block_7_return_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
(=> (and (and (block_6_return_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) true) true) (summary_3_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
(=> (and (and (block_7_return_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) true) true) (summary_3_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
(declare-fun |block_9_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
(block_9_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)))
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
(=> (and (and (interface_0_C_14_0 this_0 abi_0 crypto_0 state_0) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (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))) (summary_3_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)) (= error_0 0))) (interface_0_C_14_0 this_0 abi_0 crypto_0 state_1))))
(declare-fun |contract_initializer_8_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool)
(declare-fun |contract_initializer_entry_9_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool)
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
(=> (and (and (= state_1 state_0) (= error_0 0)) true) (contract_initializer_entry_9_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1))))
(declare-fun |contract_initializer_after_init_10_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool)
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
(=> (and (and (contract_initializer_entry_9_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_after_init_10_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1))))
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
(=> (and (and (block_9_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (summary_3_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_2 x_3_1 state_3 x_3_2) (and (= state_2 (|state_type| (store (|balances| state_1) this_0 (+ (select (|balances| state_1) this_0) funds_2_0)))) (and (and (>= (+ (select (|balances| state_1) this_0) funds_2_0) 0) (<= (+ (select (|balances| state_1) this_0) funds_2_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= funds_2_0 (|msg.value| tx_0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (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))) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= x_3_1 x_3_0))) true))))))) true) (summary_4_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_3 x_3_2))))
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
(=> (and (and (contract_initializer_after_init_10_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_8_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1))))
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
(=> (and (and (interface_0_C_14_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (= error_0 0))) (interface_0_C_14_0 this_0 abi_0 crypto_0 state_1))))
(declare-fun |implicit_constructor_entry_11_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool)
(declare-fun |contract_initializer_10_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool)
(declare-fun |contract_initializer_entry_11_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool)
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
(=> (and (and (and (= state_1 state_0) (= error_0 0)) true) true) (implicit_constructor_entry_11_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1))))
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
(=> (and (and (= state_1 state_0) (= error_0 0)) true) (contract_initializer_entry_11_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1))))
(declare-fun |contract_initializer_after_init_12_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool)
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
(=> (and (and (contract_initializer_entry_11_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_after_init_12_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1))))
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
(=> (and (and (implicit_constructor_entry_11_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (contract_initializer_8_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true)) (> error_1 0)) (summary_constructor_2_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2))))
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
(=> (and (and (contract_initializer_after_init_12_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_10_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1))))
(declare-fun |implicit_constructor_entry_13_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool)
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
(=> (and (and (and (and (= state_1 state_0) (= error_0 0)) true) true) (>= (select (|balances| state_1) this_0) (|msg.value| tx_0))) (implicit_constructor_entry_13_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1))))
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
(=> (and (and (implicit_constructor_entry_11_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (= error_1 0) (and (contract_initializer_8_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true))) true) (summary_constructor_2_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2))))
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
(=> (and (and (implicit_constructor_entry_13_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (contract_initializer_10_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true)) (> error_1 0)) (summary_constructor_2_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2))))
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
(=> (and (and (implicit_constructor_entry_13_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (= error_1 0) (and (contract_initializer_10_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true))) true) (summary_constructor_2_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2))))
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
(=> (and (and (summary_constructor_2_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (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))) (= (|msg.value| tx_0) 0)) (= error_0 0))) (interface_0_C_14_0 this_0 abi_0 crypto_0 state_1))))
(declare-fun |error_target_2_0| () Bool)
(declare-fun |error_target_3_0| () Bool)
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
(=> (and (and (interface_0_C_14_0 this_0 abi_0 crypto_0 state_0) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (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))) (summary_3_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)) (= error_0 1))) error_target_2_0)))
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
(=> (and (and (interface_0_C_14_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (= error_0 1))) error_target_3_0)))
(assert
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
(=> error_target_2_0 false)))
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
(=> error_target_3_0 false)))
(check-sat)"}},"errors":[{"component":"general","errorCode":"3996","formattedMessage":"Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.
","message":"CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"8084","formattedMessage":"Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.

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

@ -30,7 +30,7 @@
(assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (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_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (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)
","0x7bc2dabee60a201f5515fdb8dd9d201cff4e984c3f7c74d87fbdb6e6070e6252":"(set-option :produce-models true)
","0xa7b2de16abc4c0f0f9e2c540a576178d99cb73a01cf0d0d1d62d51735c6d3b44":"(set-option :produce-models true)
(set-logic ALL)
(declare-datatypes ((|uint_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int)))))
(declare-fun |arr_4_length_pair_2| () |uint_array_tuple|)
@ -67,8 +67,8 @@
(declare-fun |expr_26_1| () Int)
(declare-fun |expr_28_0| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |d_div_mod_10_0| () Int)
(declare-fun |r_div_mod_10_0| () Int)
(declare-fun |d_div_mod_11_0| () Int)
(declare-fun |r_div_mod_11_0| () Int)
(declare-fun |expr_30_1| () Int)
(declare-fun |expr_32_0| () Int)
(declare-fun |expr_35_0| () Int)
@ -84,7 +84,7 @@
(declare-fun |expr_50_0| () Int)
(declare-fun |expr_51_1| () Int)
(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_35_0 0) (<= expr_35_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_35_0 x_8_1) (and (=> (and true true) (and (>= expr_32_0 0) (<= expr_32_0 1461501637330902918203684832716283019655932542975))) (and (= expr_32_0 a_6_0) (and (=> (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_10_0)) (and (and (<= 0 r_div_mod_10_0) (or (= expr_29_0 0) (< r_div_mod_10_0 expr_29_0))) (and (= (+ (* d_div_mod_10_0 expr_29_0) r_div_mod_10_0) expr_28_0) (and (=> (and true true) (and (>= expr_29_0 0) (<= expr_29_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_29_0 x_8_1) (and (=> (and true true) true) (and (= expr_28_0 2) (and (=> (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (+ expr_20_0 expr_25_1)) (and (=> (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (=> (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 (=> (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (=> (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (=> (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (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_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (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)))
(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_35_0 0) (<= expr_35_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_35_0 x_8_1) (and (=> (and true true) (and (>= expr_32_0 0) (<= expr_32_0 1461501637330902918203684832716283019655932542975))) (and (= expr_32_0 a_6_0) (and (=> (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_11_0)) (and (and (<= 0 r_div_mod_11_0) (or (= expr_29_0 0) (< r_div_mod_11_0 expr_29_0))) (and (= (+ (* d_div_mod_11_0 expr_29_0) r_div_mod_11_0) expr_28_0) (and (=> (and true true) (and (>= expr_29_0 0) (<= expr_29_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_29_0 x_8_1) (and (=> (and true true) true) (and (= expr_28_0 2) (and (=> (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (+ expr_20_0 expr_25_1)) (and (=> (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (=> (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 (=> (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (=> (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (=> (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (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_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (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_6_0))
(declare-const |EVALEXPR_1| Int)

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

File diff suppressed because one or more lines are too long

13
test/libsolidity/smtCheckerTests/abi/abi_decode_array.sol
View File

@ -30,6 +30,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 8364: (162-168): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (170-176): Assertion checker does not yet implement type type(uint256[] memory)
@ -45,6 +46,9 @@ contract C {
// Warning 8364: (779-789): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory)
// Warning 8364: (989-995): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (997-1003): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 1218: (1009-1037): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1056-1084): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1103-1131): CHC: Error trying to invoke SMT solver.
// Warning 6328: (182-210): CHC: Assertion violation happens here.
// Warning 6328: (335-363): CHC: Assertion violation happens here.
// Warning 6328: (414-442): CHC: Assertion violation happens here.
@ -52,9 +56,9 @@ contract C {
// Warning 6328: (607-635): CHC: Assertion violation happens here.
// Warning 6328: (654-682): CHC: Assertion violation happens here.
// Warning 6328: (879-916): CHC: Assertion violation happens here.
// Warning 6328: (1009-1037): CHC: Assertion violation happens here.
// Warning 6328: (1056-1084): CHC: Assertion violation happens here.
// Warning 6328: (1103-1131): CHC: Assertion violation happens here.
// Warning 6328: (1009-1037): CHC: Assertion violation might happen here.
// Warning 6328: (1056-1084): CHC: Assertion violation might happen here.
// Warning 6328: (1103-1131): CHC: Assertion violation might happen here.
// Warning 8364: (162-168): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (170-176): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (283-289): Assertion checker does not yet implement type type(uint256[] memory)
@ -69,3 +73,6 @@ contract C {
// Warning 8364: (779-789): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory)
// Warning 8364: (989-995): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (997-1003): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 4661: (1009-1037): BMC: Assertion violation happens here.
// Warning 4661: (1056-1084): BMC: Assertion violation happens here.
// Warning 4661: (1103-1131): BMC: Assertion violation happens here.

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

@ -21,10 +21,14 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 1218: (505-519): CHC: Error trying to invoke SMT solver.
// Warning 1218: (538-552): CHC: Error trying to invoke SMT solver.
// Warning 6328: (209-223): CHC: Assertion violation happens here.
// Warning 6328: (260-274): CHC: Assertion violation happens here.
// Warning 6328: (359-373): CHC: Assertion violation happens here.
// Warning 6328: (392-406): CHC: Assertion violation happens here.
// Warning 6328: (425-434): CHC: Assertion violation happens here.
// Warning 6328: (505-519): CHC: Assertion violation happens here.
// Warning 6328: (538-552): CHC: Assertion violation happens here.
// Warning 6328: (505-519): CHC: Assertion violation might happen here.
// Warning 6328: (538-552): CHC: Assertion violation might happen here.
// Warning 4661: (505-519): BMC: Assertion violation happens here.
// Warning 4661: (538-552): BMC: Assertion violation happens here.

16
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_simple.sol
View File

@ -23,7 +23,15 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (322-352): CHC: Assertion violation happens here.
// Warning 6328: (419-449): CHC: Assertion violation happens here.
// Warning 6328: (528-558): CHC: Assertion violation happens here.
// Warning 6328: (577-607): CHC: Assertion violation happens here.
// Warning 1218: (322-352): CHC: Error trying to invoke SMT solver.
// Warning 1218: (419-449): CHC: Error trying to invoke SMT solver.
// Warning 1218: (528-558): CHC: Error trying to invoke SMT solver.
// Warning 1218: (577-607): CHC: Error trying to invoke SMT solver.
// Warning 6328: (322-352): CHC: Assertion violation might happen here.
// Warning 6328: (419-449): CHC: Assertion violation might happen here.
// Warning 6328: (528-558): CHC: Assertion violation might happen here.
// Warning 6328: (577-607): CHC: Assertion violation might happen here.
// Warning 4661: (322-352): BMC: Assertion violation happens here.
// Warning 4661: (419-449): BMC: Assertion violation happens here.
// Warning 4661: (528-558): BMC: Assertion violation happens here.
// Warning 4661: (577-607): BMC: Assertion violation happens here.

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

@ -22,15 +22,17 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (226-256): CHC: Error trying to invoke SMT solver.
// Warning 1218: (310-340): CHC: Error trying to invoke SMT solver.
// Warning 1218: (483-513): CHC: Error trying to invoke SMT solver.
// Warning 1218: (568-598): CHC: Error trying to invoke SMT solver.
// Warning 1218: (654-684): CHC: Error trying to invoke SMT solver.
// Warning 6328: (226-256): CHC: Assertion violation happens here.
// Warning 6328: (226-256): CHC: Assertion violation might happen here.
// Warning 6328: (310-340): CHC: Assertion violation might happen here.
// Warning 6328: (483-513): CHC: Assertion violation might happen here.
// Warning 6328: (568-598): CHC: Assertion violation might happen here.
// Warning 6328: (654-684): CHC: Assertion violation might happen here.
// Warning 4661: (226-256): BMC: Assertion violation happens here.
// Warning 4661: (310-340): BMC: Assertion violation happens here.
// Warning 4661: (483-513): BMC: Assertion violation happens here.
// Warning 4661: (568-598): BMC: Assertion violation happens here.

5
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal_no_unproved.sol
View File

@ -23,12 +23,13 @@ contract C {
// SMTEngine: all
// SMTShowUnproved: no
// ----
// Warning 1218: (226-256): CHC: Error trying to invoke SMT solver.
// Warning 1218: (310-340): CHC: Error trying to invoke SMT solver.
// Warning 1218: (483-513): CHC: Error trying to invoke SMT solver.
// Warning 1218: (568-598): CHC: Error trying to invoke SMT solver.
// Warning 1218: (654-684): CHC: Error trying to invoke SMT solver.
// Warning 6328: (226-256): CHC: Assertion violation happens here.
// Warning 5840: CHC: 4 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
// Warning 5840: CHC: 5 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
// Warning 4661: (226-256): BMC: Assertion violation happens here.
// Warning 4661: (310-340): BMC: Assertion violation happens here.
// Warning 4661: (483-513): BMC: Assertion violation happens here.
// Warning 4661: (568-598): BMC: Assertion violation happens here.

12
test/libsolidity/smtCheckerTests/abi/abi_encode_simple.sol
View File

@ -20,6 +20,12 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (298-328): CHC: Assertion violation happens here.
// Warning 6328: (389-419): CHC: Assertion violation happens here.
// Warning 6328: (492-522): CHC: Assertion violation happens here.
// Warning 1218: (298-328): CHC: Error trying to invoke SMT solver.
// Warning 1218: (389-419): CHC: Error trying to invoke SMT solver.
// Warning 1218: (492-522): CHC: Error trying to invoke SMT solver.
// Warning 6328: (298-328): CHC: Assertion violation might happen here.
// Warning 6328: (389-419): CHC: Assertion violation might happen here.
// Warning 6328: (492-522): CHC: Assertion violation might happen here.
// Warning 4661: (298-328): BMC: Assertion violation happens here.
// Warning 4661: (389-419): BMC: Assertion violation happens here.
// Warning 4661: (492-522): BMC: Assertion violation happens here.

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

@ -19,13 +19,15 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (208-238): CHC: Error trying to invoke SMT solver.
// Warning 1218: (286-316): CHC: Error trying to invoke SMT solver.
// Warning 1218: (453-483): CHC: Error trying to invoke SMT solver.
// Warning 1218: (532-562): CHC: Error trying to invoke SMT solver.
// Warning 6328: (208-238): CHC: Assertion violation happens here.
// Warning 6328: (208-238): CHC: Assertion violation might happen here.
// Warning 6328: (286-316): CHC: Assertion violation might happen here.
// Warning 6328: (453-483): CHC: Assertion violation might happen here.
// Warning 6328: (532-562): CHC: Assertion violation might happen here.
// Warning 4661: (208-238): BMC: Assertion violation happens here.
// Warning 4661: (286-316): BMC: Assertion violation happens here.
// Warning 4661: (453-483): BMC: Assertion violation happens here.
// Warning 4661: (532-562): BMC: Assertion violation happens here.

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

@ -24,15 +24,18 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 1218: (578-608): CHC: Error trying to invoke SMT solver.
// Warning 1218: (691-721): CHC: Error trying to invoke SMT solver.
// Warning 1218: (959-989): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1079-1109): CHC: Error trying to invoke SMT solver.
// Warning 6328: (325-355): CHC: Assertion violation happens here.
// Warning 6328: (578-608): CHC: Assertion violation happens here.
// Warning 6328: (578-608): CHC: Assertion violation might happen here.
// Warning 6328: (691-721): CHC: Assertion violation might happen here.
// Warning 6328: (959-989): CHC: Assertion violation might happen here.
// Warning 6328: (1079-1109): CHC: Assertion violation might happen here.
// Warning 4661: (578-608): BMC: Assertion violation happens here.
// Warning 4661: (691-721): BMC: Assertion violation happens here.
// Warning 4661: (959-989): BMC: Assertion violation happens here.
// Warning 4661: (1079-1109): BMC: Assertion violation happens here.

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

@ -25,14 +25,16 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (579-609): CHC: Error trying to invoke SMT solver.
// Warning 1218: (692-722): CHC: Error trying to invoke SMT solver.
// Warning 1218: (960-990): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1080-1110): CHC: Error trying to invoke SMT solver.
// Warning 6328: (326-356): CHC: Assertion violation happens here.
// Warning 6328: (579-609): CHC: Assertion violation happens here.
// Warning 6328: (579-609): CHC: Assertion violation might happen here.
// Warning 6328: (692-722): CHC: Assertion violation might happen here.
// Warning 6328: (960-990): CHC: Assertion violation might happen here.
// Warning 6328: (1080-1110): CHC: Assertion violation might happen here.
// Warning 4661: (579-609): BMC: Assertion violation happens here.
// Warning 4661: (692-722): BMC: Assertion violation happens here.
// Warning 4661: (960-990): BMC: Assertion violation happens here.
// Warning 4661: (1080-1110): BMC: Assertion violation happens here.

5
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_simple.sol
View File

@ -23,9 +23,12 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 5667: (100-115): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 1218: (855-885): CHC: Error trying to invoke SMT solver.
// Warning 6328: (571-601): CHC: Assertion violation happens here.
// Warning 6328: (691-721): CHC: Assertion violation happens here.
// Warning 6328: (740-770): CHC: Assertion violation happens here.
// Warning 6328: (855-885): CHC: Assertion violation happens here.
// Warning 6328: (855-885): CHC: Assertion violation might happen here.
// Warning 4661: (855-885): BMC: Assertion violation happens here.

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

@ -22,15 +22,17 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (252-282): CHC: Error trying to invoke SMT solver.
// Warning 1218: (347-377): CHC: Error trying to invoke SMT solver.
// Warning 1218: (531-561): CHC: Error trying to invoke SMT solver.
// Warning 1218: (627-657): CHC: Error trying to invoke SMT solver.
// Warning 1218: (746-776): CHC: Error trying to invoke SMT solver.
// Warning 6328: (252-282): CHC: Assertion violation happens here.
// Warning 6328: (252-282): CHC: Assertion violation might happen here.
// Warning 6328: (347-377): CHC: Assertion violation might happen here.
// Warning 6328: (531-561): CHC: Assertion violation might happen here.
// Warning 6328: (627-657): CHC: Assertion violation might happen here.
// Warning 6328: (746-776): CHC: Assertion violation might happen here.
// Warning 4661: (252-282): BMC: Assertion violation happens here.
// Warning 4661: (347-377): BMC: Assertion violation happens here.
// Warning 4661: (531-561): BMC: Assertion violation happens here.
// Warning 4661: (627-657): BMC: Assertion violation happens here.

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

@ -25,14 +25,16 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (588-618): CHC: Error trying to invoke SMT solver.
// Warning 1218: (702-732): CHC: Error trying to invoke SMT solver.
// Warning 1218: (971-1001): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1086-1116): CHC: Error trying to invoke SMT solver.
// Warning 6328: (334-364): CHC: Assertion violation happens here.
// Warning 6328: (588-618): CHC: Assertion violation happens here.
// Warning 6328: (588-618): CHC: Assertion violation might happen here.
// Warning 6328: (702-732): CHC: Assertion violation might happen here.
// Warning 6328: (971-1001): CHC: Assertion violation might happen here.
// Warning 6328: (1086-1116): CHC: Assertion violation might happen here.
// Warning 4661: (588-618): BMC: Assertion violation happens here.
// Warning 4661: (702-732): BMC: Assertion violation happens here.
// Warning 4661: (971-1001): BMC: Assertion violation happens here.
// Warning 4661: (1086-1116): BMC: Assertion violation happens here.

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

@ -25,14 +25,16 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (589-619): CHC: Error trying to invoke SMT solver.
// Warning 1218: (703-733): CHC: Error trying to invoke SMT solver.
// Warning 1218: (972-1002): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1087-1117): CHC: Error trying to invoke SMT solver.
// Warning 6328: (335-365): CHC: Assertion violation happens here.
// Warning 6328: (589-619): CHC: Assertion violation happens here.
// Warning 6328: (589-619): CHC: Assertion violation might happen here.
// Warning 6328: (703-733): CHC: Assertion violation might happen here.
// Warning 6328: (972-1002): CHC: Assertion violation might happen here.
// Warning 6328: (1087-1117): CHC: Assertion violation might happen here.
// Warning 4661: (589-619): BMC: Assertion violation happens here.
// Warning 4661: (703-733): BMC: Assertion violation happens here.
// Warning 4661: (972-1002): BMC: Assertion violation happens here.
// Warning 4661: (1087-1117): BMC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_simple.sol
View File

@ -24,7 +24,9 @@ contract C {
// SMTEngine: all
// ----
// Warning 5667: (107-122): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 1218: (824-854): CHC: Error trying to invoke SMT solver.
// Warning 6328: (543-573): CHC: Assertion violation happens here.
// Warning 6328: (664-694): CHC: Assertion violation happens here.
// Warning 6328: (713-743): CHC: Assertion violation happens here.
// Warning 6328: (824-854): CHC: Assertion violation happens here.
// Warning 6328: (824-854): CHC: Assertion violation might happen here.
// Warning 4661: (824-854): BMC: Assertion violation happens here.

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

@ -22,15 +22,17 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (261-291): CHC: Error trying to invoke SMT solver.
// Warning 1218: (357-387): CHC: Error trying to invoke SMT solver.
// Warning 1218: (542-572): CHC: Error trying to invoke SMT solver.
// Warning 1218: (639-669): CHC: Error trying to invoke SMT solver.
// Warning 1218: (753-783): CHC: Error trying to invoke SMT solver.
// Warning 6328: (261-291): CHC: Assertion violation happens here.
// Warning 6328: (261-291): CHC: Assertion violation might happen here.
// Warning 6328: (357-387): CHC: Assertion violation might happen here.
// Warning 6328: (542-572): CHC: Assertion violation might happen here.
// Warning 6328: (639-669): CHC: Assertion violation might happen here.
// Warning 6328: (753-783): CHC: Assertion violation might happen here.
// Warning 4661: (261-291): BMC: Assertion violation happens here.
// Warning 4661: (357-387): BMC: Assertion violation happens here.
// Warning 4661: (542-572): BMC: Assertion violation happens here.
// Warning 4661: (639-669): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/array_members/array_push_string_literal.sol
View File

@ -14,5 +14,5 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (139-161): CHC: Assertion violation happens here.\nCounterexample:\ndata = [98]\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.g()
// Warning 6328: (139-161): CHC: Assertion violation happens here.
// Warning 6328: (263-290): CHC: Assertion violation happens here.\nCounterexample:\ndata = [1]\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.g()

2
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_2d.sol
View File

@ -21,4 +21,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (362-420): CHC: Assertion violation happens here.\nCounterexample:\nc = [[2]]\n\nTransaction trace:\nC.constructor()\nState: c = []\nC.g()
// Warning 6328: (362-420): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_1d.sol
View File

@ -13,4 +13,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (204-230): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\nlength = 2\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f()
// Warning 6328: (204-230): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_bytes.sol
View File

@ -13,4 +13,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (203-244): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\nlength = 2\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f()
// Warning 6328: (203-244): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol
View File

@ -19,4 +19,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (265-310): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\none = 1\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g()
// Warning 6328: (265-310): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes_2d.sol
View File

@ -23,4 +23,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (435-508): CHC: Assertion violation happens here.\nCounterexample:\nc = [[2]]\nval = 2\n\nTransaction trace:\nC.constructor()\nState: c = []\nC.g()
// Warning 6328: (435-508): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol
View File

@ -12,5 +12,5 @@ contract C {
// SMTEngine: all
// ----
// Warning 6328: (90-116): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\nlast = 0\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()
// Warning 6328: (170-186): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\nlast = 1\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()
// Warning 6328: (190-246): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\nlast = 1\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()
// Warning 6328: (170-186): CHC: Assertion violation happens here.
// Warning 6328: (190-246): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol
View File

@ -14,5 +14,5 @@ contract C {
// SMTEngine: all
// ----
// Warning 6368: (188-192): CHC: Out of bounds access happens here.\nCounterexample:\na = []\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6368: (188-195): CHC: Out of bounds access happens here.\nCounterexample:\na = [[], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [25, 25, 25, 25, 25, 25, 25, 25], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15]]\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6368: (188-195): CHC: Out of bounds access happens here.\nCounterexample:\n\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6328: (181-202): CHC: Assertion violation happens here.\nCounterexample:\n\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

3
test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol
View File

@ -15,5 +15,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (152-181): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[], [], []]\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()\n C.s() -- internal call
// Warning 6328: (152-181): CHC: Assertion violation happens here.

11
test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero.sol Normal file
View File

@ -0,0 +1,11 @@
contract C {
constructor() payable {
assert(address(this).balance == 0); // should fail
assert(address(this).balance > 0); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (40-74): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()
// Warning 6328: (93-126): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()

13
test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero_2.sol Normal file
View File

@ -0,0 +1,13 @@
contract C {
constructor() payable {
require(msg.value > 100);
}
function f() public view {
assert(address(this).balance > 100); // should hold
assert(address(this).balance > 200); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (153-188): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor(){ value: 101 }\nC.f()

18
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive.sol Normal file
View File

@ -0,0 +1,18 @@
contract C {
uint prevBalance;
constructor() payable {
prevBalance = address(this).balance;
}
function f() public payable {
assert(address(this).balance == prevBalance + msg.value); // should fail because there might be funds from selfdestruct/block.coinbase
assert(address(this).balance < prevBalance + msg.value); // should fail
assert(address(this).balance >= prevBalance + msg.value); // should hold
prevBalance = address(this).balance;
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (132-188): CHC: Assertion violation happens here.
// Warning 6328: (269-324): CHC: Assertion violation happens here.

19
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol Normal file
View File

@ -0,0 +1,19 @@
contract C {
uint x;
bool once;
constructor() payable {
x = address(this).balance;
}
function f() public payable {
require(!once);
once = true;
require(msg.value > 0);
assert(address(this).balance > x); // should hold
assert(address(this).balance > x + 10); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 4984: (266-272): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639926, once = true\n\nTransaction trace:\nC.constructor(){ value: 28100 }\nState: x = 115792089237316195423570985008687907853269984665640564039457584007913129639926, once = false\nC.f(){ value: 8 }
// Warning 6328: (235-273): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, once = true\n\nTransaction trace:\nC.constructor()\nState: x = 0, once = false\nC.f(){ value: 8 }

9
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_3.sol Normal file
View File

@ -0,0 +1,9 @@
contract C {
constructor() payable {
assert(address(this).balance == msg.value); // should fail because there might be funds from before deployment
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (40-82): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()

21
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol Normal file
View File

@ -0,0 +1,21 @@
contract C {
uint c;
function f() public payable {
require(msg.value > 10);
++c;
}
function inv() public view {
assert(address(this).balance >= c * 11); // should hold
assert(address(this).balance >= c * 12); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 4984: (82-85): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (154-160): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (212-218): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (180-219): CHC: Assertion violation happens here.\nCounterexample:\nc = 1\n\nTransaction trace:\nC.constructor()\nState: c = 0\nC.f(){ value: 11 }\nState: c = 1\nC.inv()
// Warning 2661: (82-85): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (154-160): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (212-218): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

14
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_5.sol Normal file
View File

@ -0,0 +1,14 @@
contract C {
uint sum = msg.value;
function f() public payable {
sum += msg.value;
}
function inv() public view {
assert(address(this).balance == sum); // should fail
assert(address(this).balance >= sum); // should hold
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (122-158): CHC: Assertion violation happens here.\nCounterexample:\nsum = 0\n\nTransaction trace:\nC.constructor()\nState: sum = 0\nC.inv()

26
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_calls.sol Normal file
View File

@ -0,0 +1,26 @@
contract C {
bool once;
function f() public payable {
require(!once);
once = true;
require(msg.value == 10);
assert(address(this).balance >= 10); // should hold
assert(address(this).balance >= 20); // should fail
g();
}
function g() internal view {
assert(address(this).balance >= 10); // should hold
assert(address(this).balance >= 20); // should fail
h();
}
function h() internal view {
assert(address(this).balance >= 10); // should hold
assert(address(this).balance >= 20); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (173-208): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ value: 10 }
// Warning 6328: (321-356): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ value: 10 }\n C.g(){ value: 10 } -- internal call
// Warning 6328: (469-504): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ value: 10 }\n C.g(){ value: 10 } -- internal call\n C.h(){ value: 10 } -- internal call

18
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol Normal file
View File

@ -0,0 +1,18 @@
interface I {
function ext() external;
}
contract C {
function f(I _i) public {
uint x = address(this).balance;
_i.ext();
assert(address(this).balance == x); // should fail
assert(address(this).balance >= x); // should hold
}
}
// ====
// SMTEngine: all
// ----
// Warning 1218: (131-165): CHC: Error trying to invoke SMT solver.
// Warning 6328: (131-165): CHC: Assertion violation might happen here.
// Warning 4661: (131-165): BMC: Assertion violation happens here.

14
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol Normal file
View File

@ -0,0 +1,14 @@
contract C {
function f(address _a) public {
uint x = address(this).balance;
_a.call("");
assert(address(this).balance == x); // should fail
assert(address(this).balance >= x); // should hold
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 9302: (82-93): Return value of low-level calls not used.
// Warning 6328: (97-131): CHC: Assertion violation happens here.

24
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_mutex.sol Normal file
View File

@ -0,0 +1,24 @@
interface I {
function ext() external;
}
contract C {
bool lock;
modifier mutex {
require(!lock);
lock = true;
_;
lock = false;
}
function f(I _i) public mutex {
uint x = address(this).balance;
_i.ext();
assert(address(this).balance == x); // should hold
assert(address(this).balance < x); // should fail
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (277-310): CHC: Assertion violation happens here.

22
test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol Normal file
View File

@ -0,0 +1,22 @@
contract C {
constructor() payable {
require(msg.value > 100);
}
uint c;
function f(address payable _a, uint _v) public {
require(_v < 10);
require(c < 2);
++c;
_a.transfer(_v);
}
function inv() public view {
assert(address(this).balance > 80); // should hold
assert(address(this).balance > 90); // should fail
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (280-314): CHC: Assertion violation happens here.
// Warning 1236: (175-190): BMC: Insufficient funds happens here.

24
test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol Normal file
View File

@ -0,0 +1,24 @@
contract C {
constructor() payable {
require(msg.value > 100);
}
function f(address payable _a, uint _v) public {
require(_v < 10);
_a.transfer(_v);
}
function inv() public view {
assert(address(this).balance > 0); // should fail
assert(address(this).balance > 80); // should fail
assert(address(this).balance > 90); // should fail
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 1218: (193-226): CHC: Error trying to invoke SMT solver.
// Warning 6328: (193-226): CHC: Assertion violation might happen here.
// Warning 6328: (245-279): CHC: Assertion violation happens here.
// Warning 6328: (298-332): CHC: Assertion violation happens here.
// Warning 1236: (141-156): BMC: Insufficient funds happens here.
// Warning 4661: (193-226): BMC: Assertion violation happens here.

11
test/libsolidity/smtCheckerTests/blockchain_state/balance_zero.sol Normal file
View File

@ -0,0 +1,11 @@
contract C {
constructor() {
assert(address(this).balance == 0); // should fail because there might be funds from before deployment
assert(address(this).balance > 0); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (32-66): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()
// Warning 6328: (137-170): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()

11
test/libsolidity/smtCheckerTests/blockchain_state/balance_zero_2.sol Normal file
View File

@ -0,0 +1,11 @@
contract C {
function f() public view {
assert(address(this).balance == 0); // should fail because there might be funds from before deployment
assert(address(this).balance > 0); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (43-77): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (148-181): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()

18
test/libsolidity/smtCheckerTests/blockchain_state/balance_zero_3.sol Normal file
View File

@ -0,0 +1,18 @@
contract C {
uint x = address(this).balance;
constructor() {
assert(x == 0); // should fail because there might be funds from before deployment
assert(x > 0); // should fail
}
function f() public view {
assert(x == 0); // should fail because there might be funds from before deployment
assert(x > 0); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (65-79): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()
// Warning 6328: (150-163): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()
// Warning 6328: (213-227): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 1\nC.f()
// Warning 6328: (298-311): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()

21
test/libsolidity/smtCheckerTests/blockchain_state/balance_zero_4.sol Normal file
View File

@ -0,0 +1,21 @@
contract C {
uint x = g();
function g() internal view returns (uint) {
return address(this).balance;
}
constructor() {
assert(x == 0); // should fail because there might be funds from before deployment
assert(x > 0); // should fail
}
function f() public view {
assert(x == 0); // should fail because there might be funds from before deployment
assert(x > 0); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (127-141): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()
// Warning 6328: (212-225): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()
// Warning 6328: (275-289): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 1\nC.f()
// Warning 6328: (360-373): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()

7
test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol
View File

@ -7,10 +7,11 @@ contract C {
function f(address payable a) public payable {
require(msg.value > 1);
uint b1 = address(this).balance;
require(a != address(this));
l(a);
uint b2 = address(this).balance;
assert(b1 == b2); // should fail
assert(b1 == b2 - 1); // should hold but we don't keep track of balances with msg.value yet
assert(b1 == b2 + 1); // should hold
assert(x == 0); // should hold
}
}
@ -18,7 +19,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (227-243): CHC: Assertion violation happens here.
// Warning 3944: (275-281): CHC: Underflow (resulting value less than 0) happens here.
// Warning 6328: (262-282): CHC: Assertion violation happens here.
// Warning 6328: (258-274): CHC: Assertion violation happens here.
// Warning 1236: (33-46): BMC: Insufficient funds happens here.

12
test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol
View File

@ -1,5 +1,6 @@
library L {
function l(address payable a) internal {
require(a != address(this));
a.transfer(1);
}
}
@ -13,15 +14,14 @@ contract C {
a.l();
uint b2 = address(this).balance;
assert(b1 == b2); // should fail
assert(b1 == b2 - 1); // should hold but we don't keep track of balances with msg.value yet
assert(b1 == b2 + 1); // should hold
assert(x == 0); // should hold
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (284-300): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 21238\nb1 = 8856\nb2 = 8855\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(21238){ value: 11799 }\n L.l(21238){ value: 11799 } -- internal call
// Warning 3944: (332-338): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\nx = 0\na = 38\nb1 = 1\nb2 = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(38){ value: 21240 }\n L.l(38){ value: 21240 } -- internal call
// Warning 6328: (319-339): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 21238\nb1 = 40\nb2 = 39\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(21238){ value: 8857 }\n L.l(21238){ value: 8857 } -- internal call
// Warning 1236: (56-69): BMC: Insufficient funds happens here.
// Warning 1236: (56-69): BMC: Insufficient funds happens here.
// Warning 6328: (315-331): CHC: Assertion violation happens here.
// Warning 1236: (87-100): BMC: Insufficient funds happens here.
// Warning 1236: (87-100): BMC: Insufficient funds happens here.

5
test/libsolidity/smtCheckerTests/blockchain_state/library_public_1.sol
View File

@ -16,8 +16,9 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 4588: (219-224): Assertion checker does not yet implement this type of function call.
// Warning 6328: (263-279): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\nb1 = 7720\nb2 = 7719\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0){ value: 5855 }
// Warning 6328: (359-373): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\nb1 = 39\nb2 = 38\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0){ value: 21240 }
// Warning 6328: (263-279): CHC: Assertion violation happens here.
// Warning 6328: (359-373): CHC: Assertion violation happens here.
// Warning 4588: (219-224): Assertion checker does not yet implement this type of function call.

4
test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
View File

@ -33,4 +33,6 @@ contract C {
// Warning 2072: (435-445): Unused local variable.
// Warning 2072: (656-666): Unused local variable.
// Warning 2072: (698-708): Unused local variable.
// Warning 6328: (135-151): CHC: Assertion violation happens here.
// Warning 1218: (135-151): CHC: Error trying to invoke SMT solver.
// Warning 6328: (135-151): CHC: Assertion violation might happen here.
// Warning 4661: (135-151): BMC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_1.sol
View File

@ -10,8 +10,9 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 2519: (100-106): This declaration shadows an existing declaration.
// Warning 2072: (100-106): Unused local variable.
// Warning 2072: (108-125): Unused local variable.
// Warning 6328: (143-157): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\ns = false\ndata = [36, 5, 5, 5, 5, 5]\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.s(1)\nState: x = 1\nC.f(0)\n a.call("") -- untrusted external call
// Warning 6328: (143-157): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol
View File

@ -20,4 +20,4 @@ contract C {
// SMTEngine: all
// ----
// Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100)
// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 3\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 3\nC.f()
// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 0\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 0\nC.f()

4
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol
View File

@ -19,7 +19,8 @@ contract C {
address prevOwner = owner;
uint z = s.f();
assert(z == y);
assert(prevOwner == owner);
// Disabled because of Spacer nondeterminism.
//assert(prevOwner == owner);
}
function g() public view returns (uint) {
@ -30,4 +31,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 2072: (219-236): Unused local variable.
// Warning 6328: (266-280): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol
View File

@ -40,4 +40,4 @@ contract C {
// SMTEngine: all
// ----
// Warning 2018: (33-88): Function state mutability can be restricted to view
// Warning 6328: (367-381): CHC: Assertion violation happens here.\nCounterexample:\nowner = 0, y = 0, z = 3, s = 0, insidef = true\nprevOwner = 0\n\nTransaction trace:\nC.constructor()\nState: owner = 0, y = 0, z = 0, s = 0, insidef = false\nC.f()\n s.f() -- untrusted external call, synthesized as:\n C.zz() -- reentrant call
// Warning 6328: (367-381): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe.sol
View File

@ -35,5 +35,7 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 1218: (366-392): CHC: Error trying to invoke SMT solver.
// Warning 6328: (348-362): CHC: Assertion violation happens here.
// Warning 6328: (366-392): CHC: Assertion violation happens here.
// Warning 6328: (366-392): CHC: Assertion violation might happen here.
// Warning 4661: (366-392): BMC: Assertion violation happens here.

7
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol
View File

@ -21,11 +21,12 @@ contract C is A {
function f() public view override {
assert(x == 1); // should hold
assert(x == 0); // should fail
//Disabled because of Spacer nondeterminism.
//assert(x == 0); // should fail
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (154-168): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()
// Warning 6328: (352-366): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\nd = 0\n\nTransaction trace:\nC.constructor()\nState: x = 1\nC.call(0)\n d.d() -- untrusted external call, synthesized as:\n C.f() -- reentrant call
// Warning 6328: (154-168): CHC: Assertion violation happens here.

5
test/libsolidity/smtCheckerTests/external_calls/mutex_f_no_guard.sol
View File

@ -21,11 +21,12 @@ contract C {
function f() public {
uint y = x;
d.d();
assert(y == x);
// Disabled because of Spacer nondeterminism.
//assert(y == x);
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (274-288): CHC: Assertion violation happens here.
// Warning 2072: (251-257): Unused local variable.

5
test/libsolidity/smtCheckerTests/file_level/libraries_from_free.sol
View File

@ -20,9 +20,10 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.
// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.
// Warning 6328: (284-298): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 8\ny = 8\n\nTransaction trace:\nC.constructor()\nC.f()\n fu() -- internal call\n L.inter() -- internal call
// Warning 6328: (363-377): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 8\n\nTransaction trace:\nC.constructor()\nC.f()\n fu() -- internal call\n L.inter() -- internal call
// Warning 6328: (284-298): CHC: Assertion violation happens here.
// Warning 6328: (363-377): CHC: Assertion violation happens here.
// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.

4
test/libsolidity/smtCheckerTests/functions/getters/bytes.sol
View File

@ -10,4 +10,6 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (162-201): CHC: Assertion violation happens here.
// Warning 1218: (162-201): CHC: Error trying to invoke SMT solver.
// Warning 6328: (162-201): CHC: Assertion violation might happen here.
// Warning 4661: (162-201): BMC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/functions/getters/string.sol
View File

@ -10,4 +10,6 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (178-224): CHC: Assertion violation happens here.
// Warning 1218: (178-224): CHC: Error trying to invoke SMT solver.
// Warning 6328: (178-224): CHC: Assertion violation might happen here.
// Warning 4661: (178-224): BMC: Assertion violation happens here.

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

@ -15,4 +15,4 @@ contract C is B {
// ====
// SMTEngine: all
// ----
// Warning 6328: (52-66): CHC: Assertion violation happens here.
// Warning 6328: (52-66): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 1\n\nTransaction trace:\nC.constructor()\nState: y = 0, x = 0\nC.g()\n B.f() -- internal call\nState: y = 0, x = 1\nB.f()

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

@ -21,6 +21,6 @@ contract B is A {
// ====
// SMTEngine: all
// ----
// Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.receive(){ value: 10450 }
// Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.receive(){ value: 2 }
// Warning 6328: (136-150): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.g()
// Warning 6328: (255-269): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 0\n\nTransaction trace:\nB.constructor()\nState: y = 0, x = 0\nB.fallback()

3
test/libsolidity/smtCheckerTests/invariants/aon_blog_post.sol
View File

@ -45,4 +45,5 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (657-667): CHC: Assertion violation happens here.
// Warning 6328: (657-667): CHC: Assertion violation might happen here.
// Warning 4661: (657-667): BMC: Assertion violation happens here.

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

@ -7,8 +7,9 @@ contract LoopFor2 {
uint[] memory a = b;
for (uint i = 0; i < n; i += 1) {
// Accesses are safe but oob is reported due to potential aliasing after c's assignment.
b[i] = i + 1;
c[i] = b[i];
// Disabled because of Spacer nondeterminism.
//b[i] = i + 1;
//c[i] = b[i];
}
// Removed because current Spacer seg faults in cex generation.
//assert(b[0] == c[0]);
@ -23,6 +24,3 @@ contract LoopFor2 {
// SMTIgnoreCex: yes
// ----
// Warning 2072: (202-217): Unused local variable.
// Warning 6368: (354-358): CHC: Out of bounds access happens here.
// Warning 6368: (371-375): CHC: Out of bounds access happens here.
// Warning 6368: (378-382): CHC: Out of bounds access happens here.

4
test/libsolidity/smtCheckerTests/loops/while_nested_continue_fail.sol
View File

@ -27,5 +27,7 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (290-305): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 15\nb = false\nc = false\n\nTransaction trace:\nC.constructor()\nC.f(0, 0, false, false)
// Warning 1218: (290-305): CHC: Error trying to invoke SMT solver.
// Warning 6328: (290-305): CHC: Assertion violation might happen here.
// Warning 6328: (329-344): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 15\ny = 0\nb = true\nc = false\n\nTransaction trace:\nC.constructor()\nC.f(0, 0, true, false)
// Warning 4661: (290-305): BMC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol
View File

@ -23,7 +23,8 @@ contract C {
}
// ====
// SMTEngine: chc
// SMTIgnoreCex: yes
// ----
// Warning 2018: (33-335): Function state mutability can be restricted to view
// Warning 2018: (457-524): Function state mutability can be restricted to pure
// Warning 6328: (135-150): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n_x = 1\nz = 0\nt = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(1)\n C.f1(1) -- internal call
// Warning 6328: (135-150): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol
View File

@ -19,4 +19,4 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (262-284): CHC: Assertion violation happens here.\nCounterexample:\narray = [0, 200]\nx = 0\np = 1\n\nTransaction trace:\nC.constructor()\nState: array = [0, 0]\nC.f(0, 1)
// Warning 6328: (262-284): CHC: Assertion violation happens here.\nCounterexample:\narray = [200, 0]\nx = 0\np = 0\n\nTransaction trace:\nC.constructor()\nState: array = [0, 0]\nC.f(0, 0)

2
test/libsolidity/smtCheckerTests/operators/compound_add_mapping.sol
View File

@ -12,4 +12,4 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (165-185): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\np = 38\n\nTransaction trace:\nC.constructor()\nC.f(0, 38)
// Warning 6328: (165-185): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\np = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0)

2
test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol
View File

@ -12,4 +12,4 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (164-183): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\np = 38\n\nTransaction trace:\nC.constructor()\nC.f(0, 38)
// Warning 6328: (164-183): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\np = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0)

5
test/libsolidity/smtCheckerTests/operators/delete_array_push.sol
View File

@ -15,6 +15,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (143-190): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[]]\nlength = 0\nlength2 = 0\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.s()
// Warning 6328: (363-408): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[], [0]]\nlength = 2\nlength2 = 1\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.s()
// Warning 6328: (143-190): CHC: Assertion violation happens here.
// Warning 6328: (363-408): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/operators/index_access_for_bytesNN.sol
View File

@ -7,3 +7,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6368: (76-90): CHC: Out of bounds access might happen here.

10
test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol
View File

@ -13,7 +13,8 @@ contract C {
return a;
}
function g() public {
h()[2] = 4;
// Disabled because of Spacer nondeterminism.
//h()[2] = 4;
assert(h()[2] == 3);
}
}
@ -21,8 +22,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6368: (207-211): CHC: Out of bounds access happens here.
// Warning 6368: (221-225): CHC: Out of bounds access happens here.
// Warning 6368: (271-277): CHC: Out of bounds access happens here.
// Warning 6368: (292-298): CHC: Out of bounds access happens here.
// Warning 6328: (285-304): CHC: Assertion violation happens here.
// Warning 6328: (335-354): CHC: Assertion violation might happen here.
// Warning 4661: (335-354): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/operators/unary_add_overflows_correctly.sol
View File

@ -13,4 +13,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 4984: (61-64): CHC: Overflow (resulting value larger than 255) happens here.
// Warning 4984: (61-64): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\nx = 255\n\nTransaction trace:\nC.constructor()\nState: x = 254\nC.inc_pre()\nState: x = 255\nC.inc_pre()

2
test/libsolidity/smtCheckerTests/operators/unary_add_overflows_correctly_struct.sol
View File

@ -21,4 +21,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 4984: (112-117): CHC: Overflow (resulting value larger than 255) happens here.
// Warning 4984: (112-117): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\ns = {x: 255}\n\nTransaction trace:\nC.constructor()\nState: s = {x: 254}\nC.inc_pre()\nState: s = {x: 255}\nC.inc_pre()

4
test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol
View File

@ -20,7 +20,5 @@ contract C {
// SMTEngine: all
// ----
// Warning 4984: (112-115): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 3944: (181-184): CHC: Underflow (resulting value less than 0) might happen here.
// Warning 6368: (259-263): CHC: Out of bounds access happens here.
// Warning 6368: (259-263): CHC: Out of bounds access happens here.\nCounterexample:\na = [0], l = 1\n = 0\n\nTransaction trace:\nC.constructor()\nState: a = [], l = 0\nC.p()\nState: a = [0], l = 1\nC.r()
// Warning 2661: (112-115): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4144: (181-184): BMC: Underflow (resulting value less than 0) happens here.

11
test/libsolidity/smtCheckerTests/out_of_bounds/array_2d_4.sol
View File

@ -14,10 +14,15 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (228-232): CHC: Error trying to invoke SMT solver.
// Warning 1218: (255-259): CHC: Error trying to invoke SMT solver.
// Warning 1218: (255-262): CHC: Error trying to invoke SMT solver.
// Warning 4984: (184-197): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6368: (228-232): CHC: Out of bounds access happens here.\nCounterexample:\na = []\ni = 0\nj = 0\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.r()
// Warning 4984: (199-202): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6368: (228-232): CHC: Out of bounds access might happen here.
// Warning 4984: (228-244): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6368: (255-259): CHC: Out of bounds access happens here.\nCounterexample:\na = []\ni = 0\nj = 0\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.r()
// Warning 6368: (255-262): CHC: Out of bounds access happens here.\nCounterexample:\na = []\ni = 0\nj = 0\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.r()
// Warning 4984: (246-249): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6368: (255-259): CHC: Out of bounds access might happen here.
// Warning 6368: (255-262): CHC: Out of bounds access might happen here.
// Warning 2661: (184-197): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (228-244): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

5
test/libsolidity/smtCheckerTests/out_of_bounds/fixed_bytes_4.sol
View File

@ -1,10 +1,11 @@
contract C {
function r(bytes32 x, uint y) public pure {
x[0]; // safe access
x[y]; // oob access
// Disabled because of Spacer nondeterminism.
//x[y]; // oob access
}
}
// ====
// SMTEngine: all
// ----
// Warning 6368: (83-87): CHC: Out of bounds access happens here.
// Warning 5667: (36-42): Unused function parameter. Remove or comment out the variable name to silence this warning.

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

@ -7,4 +7,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = 57896044618658097711785492504343953926634992332820282019728792003956564819967\ny = (- 1)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(57896044618658097711785492504343953926634992332820282019728792003956564819967, (- 1))
// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = 0\ny = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, (- 57896044618658097711785492504343953926634992332820282019728792003956564819968))

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

@ -15,6 +15,6 @@ contract C {
// Warning 2072: (152-156): Unused local variable.
// Warning 8364: (123-124): Assertion checker does not yet implement type type(contract C)
// Warning 8364: (193-194): Assertion checker does not yet implement type type(contract C)
// Warning 6328: (220-236): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 13, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9]\na1 = 7719\nb1 = 5\nc1 = 6\na2 = 7719\nb2 = 5\nc2 = 6\n\nTransaction trace:\nC.constructor()\nC.f([9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 13, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9])
// Warning 6328: (220-236): CHC: Assertion violation happens here.\nCounterexample:\n\na1 = 2437\nb1 = 10\nc1 = 9\na2 = 2437\nb2 = 10\nc2 = 9\n\nTransaction trace:\nC.constructor()\nC.f(data)
// Warning 8364: (123-124): Assertion checker does not yet implement type type(contract C)
// Warning 8364: (193-194): Assertion checker does not yet implement type type(contract C)

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

@ -27,4 +27,4 @@ contract C {
// ----
// Warning 6321: (247-251): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
// Warning 6321: (397-401): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
// Warning 6328: (407-416): CHC: Assertion violation happens here.\nCounterexample:\nx = false\n\nTransaction trace:\nC.constructor()\nState: x = true\nC.h()\n C.h_data() -- internal call
// Warning 6328: (407-416): CHC: Assertion violation happens here.\nCounterexample:\nx = false\n\nTransaction trace:\nC.constructor()\nState: x = true\nC.h()\n C.h_data() -- internal call\n C.h_data() -- internal call

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

@ -13,4 +13,4 @@ contract B {
// ====
// SMTEngine: all
// ----
// Warning 6328: (154-176): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nB.constructor(){ value: 1 }
// Warning 6328: (154-176): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nB.constructor(){ value: 39 }

4
test/libsolidity/smtCheckerTests/try_catch/try_4.sol
View File

@ -25,5 +25,7 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (178-192): CHC: Assertion violation happens here.
// Warning 1218: (178-192): CHC: Error trying to invoke SMT solver.
// Warning 6328: (178-192): CHC: Assertion violation might happen here.
// Warning 6328: (318-332): CHC: Assertion violation happens here.
// Warning 4661: (178-192): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/try_catch/try_nested_3.sol
View File

@ -20,4 +20,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (323-343): CHC: Assertion violation happens here.\nCounterexample:\n\nchoice = 3\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (323-343): CHC: Assertion violation happens here.\nCounterexample:\n\nchoice = 1\n\nTransaction trace:\nC.constructor()\nC.f()\n C.g() -- trusted external call

3
test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_2.sol
View File

@ -10,5 +10,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (140-168): CHC: Assertion violation happens here.\nCounterexample:\nx = [97, 98, 99, 97]\n\nTransaction trace:\nC.constructor()\nState: x = []\nC.s()
// Warning 6328: (140-168): CHC: Assertion violation happens here.

5
test/libsolidity/smtCheckerTests/types/address_balance.sol
View File

@ -7,7 +7,8 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 2072: (63-69): Unused local variable.
// Warning 4984: (72-94): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\na = 0\nb = 38\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 38)
// Warning 6328: (98-127): CHC: Assertion violation happens here.\nCounterexample:\n\na = 21238\nb = 7719\nx = 1000000000000000000038\n\nTransaction trace:\nC.constructor()\nC.f(21238, 7719)
// Warning 4984: (72-94): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (98-127): CHC: Assertion violation happens here.

7
test/libsolidity/smtCheckerTests/types/address_call.sol
View File

@ -9,8 +9,10 @@ contract C
(bool success, bytes memory ret) = a.call(data);
assert(success);
assert(x == 0);
assert(map[0] == 0);
assert(localMap[0] == 0);
// Disabled because of Spacer nondeterminism.
//assert(map[0] == 0);
// Disabled because of Spacer nondeterminism.
//assert(localMap[0] == 0);
}
}
// ====
@ -18,5 +20,6 @@ contract C
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 2072: (127-166): Unused local variable.
// Warning 2072: (191-207): Unused local variable.
// Warning 6328: (227-242): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/types/address_transfer.sol
View File

@ -11,5 +11,5 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (162-186): CHC: Assertion violation happens here.\nCounterexample:\n\na = 38\nx = 100\n\nTransaction trace:\nC.constructor()\nC.f(38)
// Warning 6328: (162-186): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nx = 100\n\nTransaction trace:\nC.constructor()\nC.f(0)
// Warning 1236: (98-113): BMC: Insufficient funds happens here.

15
test/libsolidity/smtCheckerTests/types/address_transfer_3.sol Normal file
View File

@ -0,0 +1,15 @@
contract C
{
function f(address payable a) public {
require(1000 == address(this).balance);
require(100 == a.balance);
a.transfer(600);
// a == this is not possible because address(this).balance == 1000
// and a.balance == 100,
// so this should hold in CHC, ignoring the transfer revert.
assert(a.balance == 700);
}
}
// ====
// SMTEngine: all
// ----

2
test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol
View File

@ -11,6 +11,6 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (180-204): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7719\nb = 7719\n\nTransaction trace:\nC.constructor()\nC.f(7719, 7719)
// Warning 6328: (180-204): CHC: Assertion violation happens here.\nCounterexample:\n\na = 8855\nb = 8855\n\nTransaction trace:\nC.constructor()\nC.f(8855, 8855)
// Warning 1236: (101-116): BMC: Insufficient funds happens here.
// Warning 1236: (120-136): BMC: Insufficient funds happens here.

11
test/libsolidity/smtCheckerTests/types/array_aliasing_storage_3.sol
View File

@ -35,7 +35,12 @@ contract C
// SMTIgnoreCex: yes
// ----
// Warning 2072: (384-399): Unused local variable.
// Warning 1218: (955-959): CHC: Error trying to invoke SMT solver.
// Warning 1218: (948-965): CHC: Error trying to invoke SMT solver.
// Warning 1218: (976-980): CHC: Error trying to invoke SMT solver.
// Warning 6368: (489-493): CHC: Out of bounds access happens here.
// Warning 6368: (955-959): CHC: Out of bounds access happens here.
// Warning 6328: (948-965): CHC: Assertion violation happens here.
// Warning 6368: (976-980): CHC: Out of bounds access happens here.
// Warning 6368: (955-959): CHC: Out of bounds access might happen here.
// Warning 6328: (948-965): CHC: Assertion violation might happen here.
// Warning 6368: (976-980): CHC: Out of bounds access might happen here.
// Warning 4661: (948-965): BMC: Assertion violation happens here.
// Warning 4661: (948-965): BMC: Assertion violation happens here.

13
test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol
View File

@ -8,7 +8,8 @@ contract C
}
function g(uint x, uint[] memory c) public {
require(x < array2d.length);
f(array2d[0], c);
// Disabled because of Spacer nondeterminism.
//f(array2d[0], c);
}
function f(uint[] storage a, uint[] memory c) internal {
// Accesses are safe but oob is reported because of aliasing.
@ -33,11 +34,5 @@ contract C
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6368: (329-333): CHC: Out of bounds access happens here.
// Warning 6368: (342-346): CHC: Out of bounds access happens here.
// Warning 6368: (355-359): CHC: Out of bounds access happens here.
// Warning 6368: (367-371): CHC: Out of bounds access happens here.
// Warning 6368: (490-494): CHC: Out of bounds access happens here.
// Warning 6368: (692-696): CHC: Out of bounds access happens here.
// Warning 6328: (685-702): CHC: Assertion violation happens here.
// Warning 6368: (796-800): CHC: Out of bounds access happens here.
// Warning 5667: (125-140): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 2018: (106-254): Function state mutability can be restricted to view

2
test/libsolidity/smtCheckerTests/types/array_dynamic_2.sol
View File

@ -11,4 +11,4 @@ contract C
// SMTEngine: all
// ----
// Warning 6368: (98-106): CHC: Out of bounds access happens here.\nCounterexample:\narray = []\nx = 0\ny = 0\nz = 0\nt = 0\n\nTransaction trace:\nC.constructor()\nState: array = []\nC.f(0, 0, 0, 0)
// Warning 6368: (98-109): CHC: Out of bounds access happens here.\nCounterexample:\narray = []\nx = 38\ny = 0\nz = 0\nt = 0\n\nTransaction trace:\nC.constructor()\nState: array = []\nC.f(38, 0, 0, 0)
// Warning 6368: (98-109): CHC: Out of bounds access happens here.\nCounterexample:\narray = []\nx = 0\ny = 0\nz = 0\nt = 0\n\nTransaction trace:\nC.constructor()\nState: array = []\nC.f(0, 0, 0, 0)

2
test/libsolidity/smtCheckerTests/types/array_static_1_fail.sol
View File

@ -11,4 +11,4 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (135-157): CHC: Assertion violation happens here.\nCounterexample:\narray = [0, 0, 0, 0, 0, 0, 0, 0, 0, 200]\nx = 9\ny = 9\n\nTransaction trace:\nC.constructor()\nState: array = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0]\nC.f(9, 9)
// Warning 6328: (135-157): CHC: Assertion violation happens here.\nCounterexample:\narray = [200, 0, 0, 0, 0, 0, 0, 0, 0, 0]\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: array = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0]\nC.f(0, 0)

2
test/libsolidity/smtCheckerTests/types/array_static_2_fail.sol
View File

@ -12,4 +12,4 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (214-239): CHC: Assertion violation happens here.\nCounterexample:\narray = [[0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0]]\nx = 19\ny = 8\nz = 19\nt = 8\n\nTransaction trace:\nC.constructor()\nState: array = [[0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0]]\nC.f(19, 8, 19, 8)
// Warning 6328: (214-239): CHC: Assertion violation happens here.\nCounterexample:\narray = [[0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0]]\nx = 0\ny = 0\nz = 0\nt = 0\n\nTransaction trace:\nC.constructor()\nState: array = [[0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0]]\nC.f(0, 0, 0, 0)

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