From 4c2b661eaa192a4625ad07976da7c94375df9eff Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Thu, 16 Sep 2021 19:18:26 +0200 Subject: [PATCH] [SMTChecker] Report values for block, msg and tx variables in counterexamples --- Changelog.md | 3 +- libsolidity/formal/CHC.cpp | 5 +- libsolidity/formal/Predicate.cpp | 95 ++++++++++++++++--- libsolidity/formal/Predicate.h | 3 +- .../model_checker_targets_all_all_engines/err | 24 ++--- .../model_checker_targets_all_chc/err | 24 ++--- .../model_checker_targets_assert_chc/err | 4 +- .../err | 16 ++-- .../model_checker_targets_default_chc/err | 16 ++-- .../model_checker_targets_div_by_zero_chc/err | 4 +- .../err | 4 +- .../model_checker_targets_overflow_chc/err | 4 +- .../model_checker_targets_pop_empty_chc/err | 4 +- .../model_checker_targets_underflow_chc/err | 4 +- .../err | 12 +-- .../err | 8 +- .../output.json | 8 +- .../output.json | 32 +++---- .../output.json | 32 +++---- .../output.json | 8 +- .../output.json | 8 +- .../output.json | 8 +- .../output.json | 8 +- .../output.json | 8 +- .../output.json | 24 ++--- .../output.json | 16 ++-- .../array_push_string_literal.sol | 2 +- .../blockchain_state/balance_non_zero.sol | 4 +- .../blockchain_state/balance_non_zero_2.sol | 2 +- .../blockchain_state/balance_receive_2.sol | 4 +- .../blockchain_state/balance_receive_3.sol | 2 +- .../blockchain_state/balance_receive_4.sol | 2 +- .../balance_receive_calls.sol | 6 +- .../external_calls/call_mutex_unsafe.sol | 2 +- .../external_calls/call_with_value_2.sol | 2 +- .../external_calls/external_reentrancy_1.sol | 2 +- .../external_calls/external_reentrancy_2.sol | 2 +- .../constant_string_at_file_level.sol | 2 +- .../file_level/file_level_call_via_module.sol | 4 +- .../smtCheckerTests/file_level/overloads.sol | 2 +- .../function_selector/homer.sol | 2 +- .../function_selector/selector_2.sol | 2 +- .../functions/getters/address.sol | 4 +- .../functions/getters/fixed_bytes.sol | 4 +- .../smtCheckerTests/functions/payable_2.sol | 2 +- .../smtCheckerTests/imports/import_base.sol | 2 +- .../imports/import_free_functions.sol | 2 +- .../imports/import_library_2.sol | 2 +- .../inheritance/receive_fallback.sol | 2 +- .../modifier_inside_branch_assignment.sol | 2 +- ...nside_branch_assignment_multi_branches.sol | 2 +- .../operators/bitwise_not_fixed_bytes.sol | 2 +- .../operators/bitwise_or_fixed_bytes.sol | 2 +- .../smtCheckerTests/operators/bytes_new.sol | 4 +- .../compound_bitwise_and_fixed_bytes.sol | 2 +- .../compound_bitwise_or_fixed_bytes.sol | 2 +- .../compound_bitwise_string_literal_2.sol | 2 +- .../compound_bitwise_string_literal_3.sol | 4 +- .../compound_bitwise_xor_fixed_bytes.sol | 2 +- .../operators/index_access_for_bytes.sol | 2 +- .../out_of_bounds/fixed_bytes_2.sol | 2 +- .../special/abi_decode_simple.sol | 2 +- .../special/block_vars_chc_internal.sol | 3 + .../smtCheckerTests/special/msg_parens_1.sol | 5 +- .../smtCheckerTests/special/msg_sig.sol | 6 +- .../smtCheckerTests/special/msg_value_1.sol | 4 +- .../smtCheckerTests/special/msg_value_2.sol | 2 +- .../smtCheckerTests/special/msg_value_4.sol | 2 +- .../special/msg_value_inheritance_1.sol | 2 +- .../special/msg_value_inheritance_2.sol | 4 +- .../special/msg_value_inheritance_3.sol | 2 +- .../special/msg_vars_chc_internal.sol | 3 + .../smtCheckerTests/special/shadowing_1.sol | 24 +++++ .../smtCheckerTests/special/timestamp_2.sol | 2 +- .../special/tx_vars_chc_internal.sol | 3 + .../special/tx_vars_reentrancy_1.sol | 16 ++++ .../special/tx_vars_reentrancy_2.sol | 16 ++++ .../typecast/address_literal.sol | 2 +- .../typecast/bytes_to_fixed_bytes_1.sol | 8 +- .../typecast/cast_larger_3.sol | 2 +- .../implicit_cast_string_literal_byte.sol | 2 +- .../string_literal_to_dynamic_bytes.sol | 2 +- ...string_literal_to_fixed_bytes_modifier.sol | 2 +- ...ng_literal_to_fixed_bytes_return_multi.sol | 2 +- .../typecast/string_to_bytes_push_1.sol | 2 +- .../types/address_transfer.sol | 2 +- .../types/address_transfer_insufficient.sol | 2 +- .../smtCheckerTests/types/fixed_bytes_2.sol | 2 +- .../types/fixed_bytes_access_4.sol | 2 +- .../types/fixed_bytes_access_5.sol | 6 +- .../types/fixed_bytes_access_7.sol | 4 +- .../smtCheckerTests/types/mapping_5.sol | 2 +- .../types/static_array_length_1.sol | 4 +- .../types/static_array_length_2.sol | 4 +- .../types/static_array_length_3.sol | 4 +- .../types/storage_value_vars_1.sol | 2 +- .../types/storage_value_vars_2.sol | 2 +- .../types/string_literal_assignment_1.sol | 2 +- .../types/string_literal_assignment_2.sol | 2 +- .../types/string_literal_assignment_3.sol | 2 +- .../types/string_literal_assignment_4.sol | 2 +- .../types/string_literal_assignment_5.sol | 2 +- .../types/string_literal_comparison_1.sol | 2 +- .../unchecked/check_var_init.sol | 2 +- .../smtCheckerTests/userTypes/multisource.sol | 2 +- 105 files changed, 390 insertions(+), 250 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/special/shadowing_1.sol create mode 100644 test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol create mode 100644 test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_2.sol diff --git a/Changelog.md b/Changelog.md index cd38019be..1b7e87642 100644 --- a/Changelog.md +++ b/Changelog.md @@ -5,10 +5,11 @@ Language Features: Compiler Features: + * SMTChecker: Output values for ``block.*``, ``msg.*`` and ``tx.*`` variables that are present in the called functions. Bugfixes: - * SMTChecker: Fix internal error in magic type access (``block``, ``msg``, ``tx``). + * SMTChecker: Fix internal error in magic type access (``block``, ``msg``, ``tx``). diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 53098e081..fc97ab0ca 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -1892,7 +1892,10 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& if (!pred->isConstructorSummary()) for (unsigned v: callGraph[node]) _dfs(node, v, depth + 1, _dfs); - calls.push_front(string(depth * 4, ' ') + pred->formatSummaryCall(nodeArgs(node), m_charStreamProvider)); + + bool appendTxVars = pred->isConstructorSummary() || pred->isFunctionSummary() || pred->isExternalCallUntrusted(); + + calls.push_front(string(depth * 4, ' ') + pred->formatSummaryCall(nodeArgs(node), m_charStreamProvider, appendTxVars)); if (pred->isInternalCall()) calls.front() += " -- internal call"; else if (pred->isExternalCallTrusted()) diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index e058fa2b3..23aa7590e 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -200,7 +200,8 @@ bool Predicate::isInterface() const string Predicate::formatSummaryCall( vector const& _args, - langutil::CharStreamProvider const& _charStreamProvider + langutil::CharStreamProvider const& _charStreamProvider, + bool _appendTxVars ) const { solAssert(isSummary(), ""); @@ -214,19 +215,67 @@ string Predicate::formatSummaryCall( } /// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). - /// Here we are interested in preInputVars to format the function call, - /// and in txData to retrieve `msg.value`. + /// Here we are interested in preInputVars to format the function call. - string value; - if (auto v = readTxVars(_args.at(4)).at("msg.value")) + string txModel; + + if (_appendTxVars) { - bigint x(*v); - if (x > 0) - value = "{ value: " + *v + " }"; + set txVars; + if (isFunctionSummary()) + { + solAssert(programFunction(), ""); + if (programFunction()->isPayable()) + txVars.insert("msg.value"); + } + else if (isConstructorSummary()) + { + FunctionDefinition const* fun = programFunction(); + if (fun && fun->isPayable()) + txVars.insert("msg.value"); + } + + struct TxVarsVisitor: public ASTConstVisitor + { + bool visit(MemberAccess const& _memberAccess) + { + Expression const* memberExpr = SMTEncoder::innermostTuple(_memberAccess.expression()); + + Type const* exprType = memberExpr->annotation().type; + solAssert(exprType, ""); + if (exprType->category() == Type::Category::Magic) + if (auto const* identifier = dynamic_cast(memberExpr)) + { + ASTString const& name = identifier->name(); + if (name == "block" || name == "msg" || name == "tx") + txVars.insert(name + "." + _memberAccess.memberName()); + } + + return true; + } + + set txVars; + } txVarsVisitor; + + if (auto fun = programFunction()) + { + fun->accept(txVarsVisitor); + txVars += txVarsVisitor.txVars; + } + + // Here we are interested in txData from the summary predicate. + auto txValues = readTxVars(_args.at(4)); + vector values; + for (auto const& _var: txVars) + if (auto v = txValues.at(_var)) + values.push_back(_var + ": " + *v); + + if (!values.empty()) + txModel = "{ " + boost::algorithm::join(values, ", ") + " }"; } if (auto contract = programContract()) - return contract->name() + ".constructor()" + value; + return contract->name() + ".constructor()" + txModel; auto stateVars = stateVariables(); solAssert(stateVars.has_value(), ""); @@ -262,7 +311,7 @@ string Predicate::formatSummaryCall( solAssert(fun->annotation().contract, ""); prefix = fun->annotation().contract->name() + "."; } - return prefix + fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")" + value; + return prefix + fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")" + txModel; } vector> Predicate::summaryStateValues(vector const& _args) const @@ -384,7 +433,27 @@ optional Predicate::expressionToString(smtutil::Expression const& _expr, { solAssert(_expr.sort->kind == Kind::Int, ""); solAssert(_expr.arguments.empty(), ""); - // TODO assert that _expr.name is a number. + + if ( + _type->category() == Type::Category::Address || + _type->category() == Type::Category::FixedBytes + ) + { + try + { + if (_expr.name == "0") + return "0x0"; + // For some reason the code below returns "0x" for "0". + return toHex(toCompactBigEndian(bigint(_expr.name)), HexPrefix::Add, HexCase::Lower); + } + catch (out_of_range const&) + { + } + catch (invalid_argument const&) + { + } + } + return _expr.name; } if (smt::isBool(*_type)) @@ -526,9 +595,9 @@ map> Predicate::readTxVars(smtutil::Expression const& _ {"block.number", TypeProvider::uint256()}, {"block.timestamp", TypeProvider::uint256()}, {"blockhash", TypeProvider::array(DataLocation::Memory, TypeProvider::uint256())}, - {"msg.data", TypeProvider::bytesMemory()}, + {"msg.data", TypeProvider::array(DataLocation::CallData)}, {"msg.sender", TypeProvider::address()}, - {"msg.sig", TypeProvider::uint256()}, + {"msg.sig", TypeProvider::fixedBytes(4)}, {"msg.value", TypeProvider::uint256()}, {"tx.gasprice", TypeProvider::uint256()}, {"tx.origin", TypeProvider::address()} diff --git a/libsolidity/formal/Predicate.h b/libsolidity/formal/Predicate.h index 6f5a05a50..7357c9beb 100644 --- a/libsolidity/formal/Predicate.h +++ b/libsolidity/formal/Predicate.h @@ -149,7 +149,8 @@ public: /// with _args. std::string formatSummaryCall( std::vector const& _args, - langutil::CharStreamProvider const& _charStreamProvider + langutil::CharStreamProvider const& _charStreamProvider, + bool _appendTxVars = false ) const; /// @returns the values of the state variables from _args at the point diff --git a/test/cmdlineTests/model_checker_targets_all_all_engines/err b/test/cmdlineTests/model_checker_targets_all_all_engines/err index 0f2e84b48..cc8a8ea33 100644 --- a/test/cmdlineTests/model_checker_targets_all_all_engines/err +++ b/test/cmdlineTests/model_checker_targets_all_all_engines/err @@ -1,13 +1,13 @@ Warning: CHC: Underflow (resulting value less than 0) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 0) +test.f(0x0, 0) --> model_checker_targets_all_all_engines/input.sol:7:3: | 7 | --x; @@ -16,13 +16,13 @@ test.f(0, 0) Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 1 Transaction trace: test.constructor() State: arr = [] -test.f(0, 2) +test.f(0x0, 2) --> model_checker_targets_all_all_engines/input.sol:8:3: | 8 | x + type(uint).max; @@ -31,13 +31,13 @@ test.f(0, 2) Warning: CHC: Division by zero happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_all_all_engines/input.sol:9:3: | 9 | 2 / x; @@ -46,13 +46,13 @@ test.f(0, 1) Warning: CHC: Assertion violation happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_all_all_engines/input.sol:11:3: | 11 | assert(x > 0); @@ -61,13 +61,13 @@ test.f(0, 1) Warning: CHC: Empty array "pop" happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_all_all_engines/input.sol:12:3: | 12 | arr.pop(); @@ -76,13 +76,13 @@ test.f(0, 1) Warning: CHC: Out of bounds access happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_all_all_engines/input.sol:13:3: | 13 | arr[x]; diff --git a/test/cmdlineTests/model_checker_targets_all_chc/err b/test/cmdlineTests/model_checker_targets_all_chc/err index 1484e7f2d..d0404ecfb 100644 --- a/test/cmdlineTests/model_checker_targets_all_chc/err +++ b/test/cmdlineTests/model_checker_targets_all_chc/err @@ -1,13 +1,13 @@ Warning: CHC: Underflow (resulting value less than 0) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 0) +test.f(0x0, 0) --> model_checker_targets_all_chc/input.sol:7:3: | 7 | --x; @@ -16,13 +16,13 @@ test.f(0, 0) Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 1 Transaction trace: test.constructor() State: arr = [] -test.f(0, 2) +test.f(0x0, 2) --> model_checker_targets_all_chc/input.sol:8:3: | 8 | x + type(uint).max; @@ -31,13 +31,13 @@ test.f(0, 2) Warning: CHC: Division by zero happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_all_chc/input.sol:9:3: | 9 | 2 / x; @@ -46,13 +46,13 @@ test.f(0, 1) Warning: CHC: Assertion violation happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_all_chc/input.sol:11:3: | 11 | assert(x > 0); @@ -61,13 +61,13 @@ test.f(0, 1) Warning: CHC: Empty array "pop" happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_all_chc/input.sol:12:3: | 12 | arr.pop(); @@ -76,13 +76,13 @@ test.f(0, 1) Warning: CHC: Out of bounds access happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_all_chc/input.sol:13:3: | 13 | arr[x]; diff --git a/test/cmdlineTests/model_checker_targets_assert_chc/err b/test/cmdlineTests/model_checker_targets_assert_chc/err index a7b73b418..1bf48bfa9 100644 --- a/test/cmdlineTests/model_checker_targets_assert_chc/err +++ b/test/cmdlineTests/model_checker_targets_assert_chc/err @@ -1,13 +1,13 @@ Warning: CHC: Assertion violation happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_assert_chc/input.sol:11:3: | 11 | assert(x > 0); diff --git a/test/cmdlineTests/model_checker_targets_default_all_engines/err b/test/cmdlineTests/model_checker_targets_default_all_engines/err index 14f3b95ff..c1fe2f5b3 100644 --- a/test/cmdlineTests/model_checker_targets_default_all_engines/err +++ b/test/cmdlineTests/model_checker_targets_default_all_engines/err @@ -1,13 +1,13 @@ Warning: CHC: Division by zero happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_default_all_engines/input.sol:9:3: | 9 | 2 / x; @@ -16,13 +16,13 @@ test.f(0, 1) Warning: CHC: Assertion violation happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_default_all_engines/input.sol:11:3: | 11 | assert(x > 0); @@ -31,13 +31,13 @@ test.f(0, 1) Warning: CHC: Empty array "pop" happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_default_all_engines/input.sol:12:3: | 12 | arr.pop(); @@ -46,13 +46,13 @@ test.f(0, 1) Warning: CHC: Out of bounds access happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_default_all_engines/input.sol:13:3: | 13 | arr[x]; diff --git a/test/cmdlineTests/model_checker_targets_default_chc/err b/test/cmdlineTests/model_checker_targets_default_chc/err index 1c21226e1..bd2aa0b4d 100644 --- a/test/cmdlineTests/model_checker_targets_default_chc/err +++ b/test/cmdlineTests/model_checker_targets_default_chc/err @@ -1,13 +1,13 @@ Warning: CHC: Division by zero happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_default_chc/input.sol:9:3: | 9 | 2 / x; @@ -16,13 +16,13 @@ test.f(0, 1) Warning: CHC: Assertion violation happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_default_chc/input.sol:11:3: | 11 | assert(x > 0); @@ -31,13 +31,13 @@ test.f(0, 1) Warning: CHC: Empty array "pop" happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_default_chc/input.sol:12:3: | 12 | arr.pop(); @@ -46,13 +46,13 @@ test.f(0, 1) Warning: CHC: Out of bounds access happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_default_chc/input.sol:13:3: | 13 | arr[x]; diff --git a/test/cmdlineTests/model_checker_targets_div_by_zero_chc/err b/test/cmdlineTests/model_checker_targets_div_by_zero_chc/err index 4318a501e..3156dd90b 100644 --- a/test/cmdlineTests/model_checker_targets_div_by_zero_chc/err +++ b/test/cmdlineTests/model_checker_targets_div_by_zero_chc/err @@ -1,13 +1,13 @@ Warning: CHC: Division by zero happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_div_by_zero_chc/input.sol:9:3: | 9 | 2 / x; diff --git a/test/cmdlineTests/model_checker_targets_out_of_bounds_chc/err b/test/cmdlineTests/model_checker_targets_out_of_bounds_chc/err index 661ae5b79..b4426a80e 100644 --- a/test/cmdlineTests/model_checker_targets_out_of_bounds_chc/err +++ b/test/cmdlineTests/model_checker_targets_out_of_bounds_chc/err @@ -1,13 +1,13 @@ Warning: CHC: Out of bounds access happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_out_of_bounds_chc/input.sol:13:3: | 13 | arr[x]; diff --git a/test/cmdlineTests/model_checker_targets_overflow_chc/err b/test/cmdlineTests/model_checker_targets_overflow_chc/err index fca12d076..e7f98ff4d 100644 --- a/test/cmdlineTests/model_checker_targets_overflow_chc/err +++ b/test/cmdlineTests/model_checker_targets_overflow_chc/err @@ -1,13 +1,13 @@ Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 1 Transaction trace: test.constructor() State: arr = [] -test.f(0, 2) +test.f(0x0, 2) --> model_checker_targets_overflow_chc/input.sol:8:3: | 8 | x + type(uint).max; diff --git a/test/cmdlineTests/model_checker_targets_pop_empty_chc/err b/test/cmdlineTests/model_checker_targets_pop_empty_chc/err index 7ec616853..d3478a700 100644 --- a/test/cmdlineTests/model_checker_targets_pop_empty_chc/err +++ b/test/cmdlineTests/model_checker_targets_pop_empty_chc/err @@ -1,13 +1,13 @@ Warning: CHC: Empty array "pop" happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_pop_empty_chc/input.sol:12:3: | 12 | arr.pop(); diff --git a/test/cmdlineTests/model_checker_targets_underflow_chc/err b/test/cmdlineTests/model_checker_targets_underflow_chc/err index ac56c82b5..448b0e25c 100644 --- a/test/cmdlineTests/model_checker_targets_underflow_chc/err +++ b/test/cmdlineTests/model_checker_targets_underflow_chc/err @@ -1,13 +1,13 @@ Warning: CHC: Underflow (resulting value less than 0) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 0) +test.f(0x0, 0) --> model_checker_targets_underflow_chc/input.sol:7:3: | 7 | --x; diff --git a/test/cmdlineTests/model_checker_targets_underflow_overflow_assert_chc/err b/test/cmdlineTests/model_checker_targets_underflow_overflow_assert_chc/err index 25680bc15..a0fbbe61a 100644 --- a/test/cmdlineTests/model_checker_targets_underflow_overflow_assert_chc/err +++ b/test/cmdlineTests/model_checker_targets_underflow_overflow_assert_chc/err @@ -1,13 +1,13 @@ Warning: CHC: Underflow (resulting value less than 0) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 0) +test.f(0x0, 0) --> model_checker_targets_underflow_overflow_assert_chc/input.sol:7:3: | 7 | --x; @@ -16,13 +16,13 @@ test.f(0, 0) Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 1 Transaction trace: test.constructor() State: arr = [] -test.f(0, 2) +test.f(0x0, 2) --> model_checker_targets_underflow_overflow_assert_chc/input.sol:8:3: | 8 | x + type(uint).max; @@ -31,13 +31,13 @@ test.f(0, 2) Warning: CHC: Assertion violation happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> model_checker_targets_underflow_overflow_assert_chc/input.sol:11:3: | 11 | assert(x > 0); diff --git a/test/cmdlineTests/model_checker_targets_underflow_overflow_chc/err b/test/cmdlineTests/model_checker_targets_underflow_overflow_chc/err index 9bb4b52f1..0dcfb1c25 100644 --- a/test/cmdlineTests/model_checker_targets_underflow_overflow_chc/err +++ b/test/cmdlineTests/model_checker_targets_underflow_overflow_chc/err @@ -1,13 +1,13 @@ Warning: CHC: Underflow (resulting value less than 0) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 0) +test.f(0x0, 0) --> model_checker_targets_underflow_overflow_chc/input.sol:7:3: | 7 | --x; @@ -16,13 +16,13 @@ test.f(0, 0) Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 1 Transaction trace: test.constructor() State: arr = [] -test.f(0, 2) +test.f(0x0, 2) --> model_checker_targets_underflow_overflow_chc/input.sol:8:3: | 8 | x + type(uint).max; diff --git a/test/cmdlineTests/standard_model_checker_targets_assert_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_assert_chc/output.json index 0ecf87bd7..fc4b9b9da 100644 --- a/test/cmdlineTests/standard_model_checker_targets_assert_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_assert_chc/output.json @@ -1,13 +1,13 @@ {"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> A:12:7: | 12 | \t\t\t\t\t\tassert(x > 0); @@ -16,10 +16,10 @@ test.f(0, 1) ","message":"CHC: Assertion violation happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1)","severity":"warning","sourceLocation":{"end":258,"file":"A","start":245},"type":"Warning"}],"sources":{"A":{"id":0}}} +test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":258,"file":"A","start":245},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json b/test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json index d5491b274..ad6418636 100644 --- a/test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json @@ -126,13 +126,13 @@ "}},"errors":[{"component":"general","errorCode":"4281","formattedMessage":"Warning: CHC: Division by zero happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> A:10:7: | 10 | \t\t\t\t\t\t2 / x; @@ -141,22 +141,22 @@ test.f(0, 1) ","message":"CHC: Division by zero happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1)","severity":"warning","sourceLocation":{"end":216,"file":"A","start":211},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here. +test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":216,"file":"A","start":211},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> A:12:7: | 12 | \t\t\t\t\t\tassert(x > 0); @@ -165,22 +165,22 @@ test.f(0, 1) ","message":"CHC: Assertion violation happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1)","severity":"warning","sourceLocation":{"end":258,"file":"A","start":245},"type":"Warning"},{"component":"general","errorCode":"2529","formattedMessage":"Warning: CHC: Empty array \"pop\" happens here. +test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":258,"file":"A","start":245},"type":"Warning"},{"component":"general","errorCode":"2529","formattedMessage":"Warning: CHC: Empty array \"pop\" happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> A:13:7: | 13 | \t\t\t\t\t\tarr.pop(); @@ -189,22 +189,22 @@ test.f(0, 1) ","message":"CHC: Empty array \"pop\" happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1)","severity":"warning","sourceLocation":{"end":275,"file":"A","start":266},"type":"Warning"},{"component":"general","errorCode":"6368","formattedMessage":"Warning: CHC: Out of bounds access happens here. +test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":275,"file":"A","start":266},"type":"Warning"},{"component":"general","errorCode":"6368","formattedMessage":"Warning: CHC: Out of bounds access happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> A:14:7: | 14 | \t\t\t\t\t\tarr[x]; @@ -213,13 +213,13 @@ test.f(0, 1) ","message":"CHC: Out of bounds access happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":283},"type":"Warning"},{"component":"general","errorCode":"6838","formattedMessage":"Warning: BMC: Condition is always true. +test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":283},"type":"Warning"},{"component":"general","errorCode":"6838","formattedMessage":"Warning: BMC: Condition is always true. --> A:7:15: | 7 | \t\t\t\t\t\trequire(x >= 0); diff --git a/test/cmdlineTests/standard_model_checker_targets_default_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_default_chc/output.json index 4049582dc..bcdf48e50 100644 --- a/test/cmdlineTests/standard_model_checker_targets_default_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_default_chc/output.json @@ -1,13 +1,13 @@ {"errors":[{"component":"general","errorCode":"4281","formattedMessage":"Warning: CHC: Division by zero happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> A:10:7: | 10 | \t\t\t\t\t\t2 / x; @@ -16,22 +16,22 @@ test.f(0, 1) ","message":"CHC: Division by zero happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1)","severity":"warning","sourceLocation":{"end":216,"file":"A","start":211},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here. +test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":216,"file":"A","start":211},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> A:12:7: | 12 | \t\t\t\t\t\tassert(x > 0); @@ -40,22 +40,22 @@ test.f(0, 1) ","message":"CHC: Assertion violation happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1)","severity":"warning","sourceLocation":{"end":258,"file":"A","start":245},"type":"Warning"},{"component":"general","errorCode":"2529","formattedMessage":"Warning: CHC: Empty array \"pop\" happens here. +test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":258,"file":"A","start":245},"type":"Warning"},{"component":"general","errorCode":"2529","formattedMessage":"Warning: CHC: Empty array \"pop\" happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> A:13:7: | 13 | \t\t\t\t\t\tarr.pop(); @@ -64,22 +64,22 @@ test.f(0, 1) ","message":"CHC: Empty array \"pop\" happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1)","severity":"warning","sourceLocation":{"end":275,"file":"A","start":266},"type":"Warning"},{"component":"general","errorCode":"6368","formattedMessage":"Warning: CHC: Out of bounds access happens here. +test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":275,"file":"A","start":266},"type":"Warning"},{"component":"general","errorCode":"6368","formattedMessage":"Warning: CHC: Out of bounds access happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> A:14:7: | 14 | \t\t\t\t\t\tarr[x]; @@ -88,10 +88,10 @@ test.f(0, 1) ","message":"CHC: Out of bounds access happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":283},"type":"Warning"}],"sources":{"A":{"id":0}}} +test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":283},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/output.json index eca84d4b0..bd8b26c12 100644 --- a/test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/output.json @@ -1,13 +1,13 @@ {"errors":[{"component":"general","errorCode":"4281","formattedMessage":"Warning: CHC: Division by zero happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> A:10:7: | 10 | \t\t\t\t\t\t2 / x; @@ -16,10 +16,10 @@ test.f(0, 1) ","message":"CHC: Division by zero happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1)","severity":"warning","sourceLocation":{"end":216,"file":"A","start":211},"type":"Warning"}],"sources":{"A":{"id":0}}} +test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":216,"file":"A","start":211},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/output.json index bdaa14b50..436942c45 100644 --- a/test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/output.json @@ -1,13 +1,13 @@ {"errors":[{"component":"general","errorCode":"6368","formattedMessage":"Warning: CHC: Out of bounds access happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> A:14:7: | 14 | \t\t\t\t\t\tarr[x]; @@ -16,10 +16,10 @@ test.f(0, 1) ","message":"CHC: Out of bounds access happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":283},"type":"Warning"}],"sources":{"A":{"id":0}}} +test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":283},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_targets_overflow_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_overflow_chc/output.json index 794a11b04..5a5410b0c 100644 --- a/test/cmdlineTests/standard_model_checker_targets_overflow_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_overflow_chc/output.json @@ -1,13 +1,13 @@ {"errors":[{"component":"general","errorCode":"4984","formattedMessage":"Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 1 Transaction trace: test.constructor() State: arr = [] -test.f(0, 2) +test.f(0x0, 2) --> A:9:7: | 9 | \t\t\t\t\t\tx + type(uint).max; @@ -16,10 +16,10 @@ test.f(0, 2) ","message":"CHC: Overflow (resulting value larger than 2**256 - 1) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 1 Transaction trace: test.constructor() State: arr = [] -test.f(0, 2)","severity":"warning","sourceLocation":{"end":203,"file":"A","start":185},"type":"Warning"}],"sources":{"A":{"id":0}}} +test.f(0x0, 2)","severity":"warning","sourceLocation":{"end":203,"file":"A","start":185},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/output.json index b6e891d6c..87edd534d 100644 --- a/test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/output.json @@ -1,13 +1,13 @@ {"errors":[{"component":"general","errorCode":"2529","formattedMessage":"Warning: CHC: Empty array \"pop\" happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> A:13:7: | 13 | \t\t\t\t\t\tarr.pop(); @@ -16,10 +16,10 @@ test.f(0, 1) ","message":"CHC: Empty array \"pop\" happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1)","severity":"warning","sourceLocation":{"end":275,"file":"A","start":266},"type":"Warning"}],"sources":{"A":{"id":0}}} +test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":275,"file":"A","start":266},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_targets_underflow_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_underflow_chc/output.json index 7a22d148a..096bb971b 100644 --- a/test/cmdlineTests/standard_model_checker_targets_underflow_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_underflow_chc/output.json @@ -1,13 +1,13 @@ {"errors":[{"component":"general","errorCode":"3944","formattedMessage":"Warning: CHC: Underflow (resulting value less than 0) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 0) +test.f(0x0, 0) --> A:8:7: | 8 | \t\t\t\t\t\t--x; @@ -16,10 +16,10 @@ test.f(0, 0) ","message":"CHC: Underflow (resulting value less than 0) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 0)","severity":"warning","sourceLocation":{"end":177,"file":"A","start":174},"type":"Warning"}],"sources":{"A":{"id":0}}} +test.f(0x0, 0)","severity":"warning","sourceLocation":{"end":177,"file":"A","start":174},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_chc/output.json index 472866447..3ea910cba 100644 --- a/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_chc/output.json @@ -1,13 +1,13 @@ {"errors":[{"component":"general","errorCode":"3944","formattedMessage":"Warning: CHC: Underflow (resulting value less than 0) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 0) +test.f(0x0, 0) --> A:8:7: | 8 | \t\t\t\t\t\t--x; @@ -16,22 +16,22 @@ test.f(0, 0) ","message":"CHC: Underflow (resulting value less than 0) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 0)","severity":"warning","sourceLocation":{"end":177,"file":"A","start":174},"type":"Warning"},{"component":"general","errorCode":"4984","formattedMessage":"Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +test.f(0x0, 0)","severity":"warning","sourceLocation":{"end":177,"file":"A","start":174},"type":"Warning"},{"component":"general","errorCode":"4984","formattedMessage":"Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 1 Transaction trace: test.constructor() State: arr = [] -test.f(0, 2) +test.f(0x0, 2) --> A:9:7: | 9 | \t\t\t\t\t\tx + type(uint).max; @@ -40,22 +40,22 @@ test.f(0, 2) ","message":"CHC: Overflow (resulting value larger than 2**256 - 1) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 1 Transaction trace: test.constructor() State: arr = [] -test.f(0, 2)","severity":"warning","sourceLocation":{"end":203,"file":"A","start":185},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here. +test.f(0x0, 2)","severity":"warning","sourceLocation":{"end":203,"file":"A","start":185},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1) +test.f(0x0, 1) --> A:12:7: | 12 | \t\t\t\t\t\tassert(x > 0); @@ -64,10 +64,10 @@ test.f(0, 1) ","message":"CHC: Assertion violation happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 1)","severity":"warning","sourceLocation":{"end":258,"file":"A","start":245},"type":"Warning"}],"sources":{"A":{"id":0}}} +test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":258,"file":"A","start":245},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_chc/output.json index d4a502b4b..88ed4136b 100644 --- a/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_chc/output.json @@ -1,13 +1,13 @@ {"errors":[{"component":"general","errorCode":"3944","formattedMessage":"Warning: CHC: Underflow (resulting value less than 0) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 0) +test.f(0x0, 0) --> A:8:7: | 8 | \t\t\t\t\t\t--x; @@ -16,22 +16,22 @@ test.f(0, 0) ","message":"CHC: Underflow (resulting value less than 0) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 0 Transaction trace: test.constructor() State: arr = [] -test.f(0, 0)","severity":"warning","sourceLocation":{"end":177,"file":"A","start":174},"type":"Warning"},{"component":"general","errorCode":"4984","formattedMessage":"Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +test.f(0x0, 0)","severity":"warning","sourceLocation":{"end":177,"file":"A","start":174},"type":"Warning"},{"component":"general","errorCode":"4984","formattedMessage":"Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 1 Transaction trace: test.constructor() State: arr = [] -test.f(0, 2) +test.f(0x0, 2) --> A:9:7: | 9 | \t\t\t\t\t\tx + type(uint).max; @@ -40,10 +40,10 @@ test.f(0, 2) ","message":"CHC: Overflow (resulting value larger than 2**256 - 1) happens here. Counterexample: arr = [] -a = 0 +a = 0x0 x = 1 Transaction trace: test.constructor() State: arr = [] -test.f(0, 2)","severity":"warning","sourceLocation":{"end":203,"file":"A","start":185},"type":"Warning"}],"sources":{"A":{"id":0}}} +test.f(0x0, 2)","severity":"warning","sourceLocation":{"end":203,"file":"A","start":185},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/libsolidity/smtCheckerTests/array_members/array_push_string_literal.sol b/test/libsolidity/smtCheckerTests/array_members/array_push_string_literal.sol index f401bc11e..55b2160c4 100644 --- a/test/libsolidity/smtCheckerTests/array_members/array_push_string_literal.sol +++ b/test/libsolidity/smtCheckerTests/array_members/array_push_string_literal.sol @@ -15,4 +15,4 @@ contract C { // SMTEngine: all // ---- // 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() +// Warning 6328: (263-290): CHC: Assertion violation happens here.\nCounterexample:\ndata = [0x01]\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.g() diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero.sol index 22d9ae86a..bf7fc6de9 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero.sol @@ -7,5 +7,5 @@ contract C { // ==== // 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() +// Warning 6328: (40-74): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor(){ msg.value: 0 } +// Warning 6328: (93-126): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor(){ msg.value: 0 } diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero_2.sol index 1bf99fca3..100f11066 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero_2.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero_2.sol @@ -10,4 +10,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (153-188): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor(){ value: 101 }\nC.f() +// Warning 6328: (153-188): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor(){ msg.value: 101 }\nC.f() diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol index f9f0093b0..c561179ec 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol @@ -15,5 +15,5 @@ contract C { // ==== // 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 } +// 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(){ msg.value: 28100 }\nState: x = 115792089237316195423570985008687907853269984665640564039457584007913129639926, once = false\nC.f(){ msg.value: 8 } +// Warning 6328: (235-273): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, once = true\n\nTransaction trace:\nC.constructor(){ msg.value: 0 }\nState: x = 0, once = false\nC.f(){ msg.value: 8 } diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_3.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_3.sol index b581a537d..169e1a066 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_3.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_3.sol @@ -6,4 +6,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (40-82): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor() +// Warning 6328: (40-82): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor(){ msg.value: 0 } diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol index 47eade523..183e60d95 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol @@ -15,7 +15,7 @@ contract C { // 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 6328: (180-219): CHC: Assertion violation happens here.\nCounterexample:\nc = 1\n\nTransaction trace:\nC.constructor()\nState: c = 0\nC.f(){ msg.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. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_calls.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_calls.sol index 68bae9ac5..3bc569997 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_calls.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_calls.sol @@ -21,6 +21,6 @@ contract C { // ==== // 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 +// Warning 6328: (173-208): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ msg.value: 10 } +// Warning 6328: (321-356): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ msg.value: 10 }\n C.g() -- internal call +// Warning 6328: (469-504): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ msg.value: 10 }\n C.g() -- internal call\n C.h() -- internal call diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol b/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol index f53178198..ad17e3d05 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol @@ -23,4 +23,4 @@ contract C { // SMTEngine: all // ---- // Warning 9302: (212-228): Return value of low-level calls not used. -// Warning 6328: (232-246): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, lock = false\n_a = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.f(0)\n _a.call("aaaaa") -- untrusted external call, synthesized as:\n C.set(1) -- reentrant call +// Warning 6328: (232-246): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, lock = false\n_a = 0x0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.f(0x0)\n _a.call("aaaaa") -- untrusted external call, synthesized as:\n C.set(1) -- reentrant call diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_with_value_2.sol b/test/libsolidity/smtCheckerTests/external_calls/call_with_value_2.sol index 792bb0730..c38658080 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/call_with_value_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/call_with_value_2.sol @@ -11,5 +11,5 @@ contract C { // ---- // Warning 9302: (96-116): Return value of low-level calls not used. // Warning 6328: (120-156): CHC: Assertion violation might happen here. -// Warning 6328: (175-210): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n i.call{value: 0}("") -- untrusted external call +// Warning 6328: (175-210): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0x0\n\nTransaction trace:\nC.constructor()\nC.g(0x0)\n i.call{value: 0}("") -- untrusted external call // Warning 4661: (120-156): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol index d92de6f04..adde1eb61 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol @@ -16,4 +16,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (206-220): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0)\n D(target).e() -- untrusted external call, synthesized as:\n C.broken() -- reentrant call +// Warning 6328: (206-220): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0x0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0x0)\n D(target).e() -- untrusted external call, synthesized as:\n C.broken() -- reentrant call diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol index 92c53a5e8..19ff2bbad 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol @@ -13,4 +13,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (117-131): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0)\n D(target).e() -- untrusted external call, synthesized as:\n C.call(0) -- reentrant call +// Warning 6328: (117-131): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0x0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0x0)\n D(target).e() -- untrusted external call, synthesized as:\n C.call(0x0) -- reentrant call diff --git a/test/libsolidity/smtCheckerTests/file_level/constant_string_at_file_level.sol b/test/libsolidity/smtCheckerTests/file_level/constant_string_at_file_level.sol index a40fbc216..fe2ebfdde 100644 --- a/test/libsolidity/smtCheckerTests/file_level/constant_string_at_file_level.sol +++ b/test/libsolidity/smtCheckerTests/file_level/constant_string_at_file_level.sol @@ -38,4 +38,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (968-983): CHC: Assertion violation happens here.\nCounterexample:\n\nw = 56\nz = 1\nt = 44048180624707321370159228589897778088919435935156254407473833945046349512704\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call\n C.g() -- internal call\n C.h() -- internal call\n C.i() -- internal call +// Warning 6328: (968-983): CHC: Assertion violation happens here.\nCounterexample:\n\nw = 56\nz = 1\nt = 0x61626300ff5f5f00000000000000000000000000000000000000000000000000\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call\n C.g() -- internal call\n C.h() -- internal call\n C.i() -- internal call diff --git a/test/libsolidity/smtCheckerTests/file_level/file_level_call_via_module.sol b/test/libsolidity/smtCheckerTests/file_level/file_level_call_via_module.sol index 9cea98f6b..0297428c6 100644 --- a/test/libsolidity/smtCheckerTests/file_level/file_level_call_via_module.sol +++ b/test/libsolidity/smtCheckerTests/file_level/file_level_call_via_module.sol @@ -18,5 +18,5 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (b.sol:208-222): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7\nb = 3\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call\n a.sol:f(2) -- internal call\n a.sol:f([97, 98, 99]) -- internal call -// Warning 6328: (b.sol:274-288): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7\nb = 3\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call\n a.sol:f(2) -- internal call\n a.sol:f([97, 98, 99]) -- internal call +// Warning 6328: (b.sol:208-222): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7\nb = 3\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call\n a.sol:f(2) -- internal call\n a.sol:f([0x61, 0x62, 0x63]) -- internal call +// Warning 6328: (b.sol:274-288): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7\nb = 3\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call\n a.sol:f(2) -- internal call\n a.sol:f([0x61, 0x62, 0x63]) -- internal call diff --git a/test/libsolidity/smtCheckerTests/file_level/overloads.sol b/test/libsolidity/smtCheckerTests/file_level/overloads.sol index 9f7e63466..7224464b4 100644 --- a/test/libsolidity/smtCheckerTests/file_level/overloads.sol +++ b/test/libsolidity/smtCheckerTests/file_level/overloads.sol @@ -15,4 +15,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (229-243): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\ny = 3\n\nTransaction trace:\nC.constructor()\nC.g()\n f(2) -- internal call\n f([97, 98, 99]) -- internal call +// Warning 6328: (229-243): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\ny = 3\n\nTransaction trace:\nC.constructor()\nC.g()\n f(2) -- internal call\n f([0x61, 0x62, 0x63]) -- internal call diff --git a/test/libsolidity/smtCheckerTests/function_selector/homer.sol b/test/libsolidity/smtCheckerTests/function_selector/homer.sol index 4fec30995..552a4d895 100644 --- a/test/libsolidity/smtCheckerTests/function_selector/homer.sol +++ b/test/libsolidity/smtCheckerTests/function_selector/homer.sol @@ -43,4 +43,4 @@ contract Homer is ERC165, Simpson { // ==== // SMTEngine: all // ---- -// Warning 6328: (1340-1395): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nHomer.constructor()\nHomer.check()\n Homer.supportsInterface(1941353618) -- internal call\n Homer.supportsInterface(33540519) -- internal call\n Homer.supportsInterface(2342435274) -- internal call +// Warning 6328: (1340-1395): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nHomer.constructor()\nHomer.check()\n Homer.supportsInterface(0x73b6b492) -- internal call\n Homer.supportsInterface(0x01ffc9a7) -- internal call\n Homer.supportsInterface(0x8b9eb9ca) -- internal call diff --git a/test/libsolidity/smtCheckerTests/function_selector/selector_2.sol b/test/libsolidity/smtCheckerTests/function_selector/selector_2.sol index 7cabb7ade..c3a4b8866 100644 --- a/test/libsolidity/smtCheckerTests/function_selector/selector_2.sol +++ b/test/libsolidity/smtCheckerTests/function_selector/selector_2.sol @@ -9,4 +9,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (92-126): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (92-126): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(){ msg.sig: 0x26121ff0 } diff --git a/test/libsolidity/smtCheckerTests/functions/getters/address.sol b/test/libsolidity/smtCheckerTests/functions/getters/address.sol index ff4032a65..92bb2761d 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/address.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/address.sol @@ -14,5 +14,5 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (171-197): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\na = 0\nb = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.f() -// Warning 6328: (249-275): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\na = 0\nb = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.f() +// Warning 6328: (171-197): CHC: Assertion violation happens here.\nCounterexample:\nx = 0x0, y = 0x0\na = 0x0\nb = 0x0\n\nTransaction trace:\nC.constructor()\nState: x = 0x0, y = 0x0\nC.f() +// Warning 6328: (249-275): CHC: Assertion violation happens here.\nCounterexample:\nx = 0x0, y = 0x0\na = 0x0\nb = 0x0\n\nTransaction trace:\nC.constructor()\nState: x = 0x0, y = 0x0\nC.f() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/fixed_bytes.sol b/test/libsolidity/smtCheckerTests/functions/getters/fixed_bytes.sol index fa56e15c8..ac47ded03 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/fixed_bytes.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/fixed_bytes.sol @@ -14,5 +14,5 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (159-175): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\na = 0\nb = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.f() -// Warning 6328: (227-245): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\na = 0\nb = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.f() +// Warning 6328: (159-175): CHC: Assertion violation happens here.\nCounterexample:\nx = 0x0, y = 0x0\na = 0x0\nb = 0x0\n\nTransaction trace:\nC.constructor()\nState: x = 0x0, y = 0x0\nC.f() +// Warning 6328: (227-245): CHC: Assertion violation happens here.\nCounterexample:\nx = 0x0, y = 0x0\na = 0x0\nb = 0x0\n\nTransaction trace:\nC.constructor()\nState: x = 0x0, y = 0x0\nC.f() diff --git a/test/libsolidity/smtCheckerTests/functions/payable_2.sol b/test/libsolidity/smtCheckerTests/functions/payable_2.sol index 6411eae62..98717b133 100644 --- a/test/libsolidity/smtCheckerTests/functions/payable_2.sol +++ b/test/libsolidity/smtCheckerTests/functions/payable_2.sol @@ -24,4 +24,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (261-283): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g2(){ value: 35 }\n C.i(){ value: 35 } -- internal call +// Warning 6328: (261-283): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g2(){ msg.value: 35 }\n C.i() -- internal call diff --git a/test/libsolidity/smtCheckerTests/imports/import_base.sol b/test/libsolidity/smtCheckerTests/imports/import_base.sol index f0ca042be..4ad653357 100644 --- a/test/libsolidity/smtCheckerTests/imports/import_base.sol +++ b/test/libsolidity/smtCheckerTests/imports/import_base.sol @@ -20,4 +20,4 @@ contract Der is Base { // ==== // SMTEngine: all // ---- -// Warning 6328: (der:173-186): CHC: Assertion violation happens here.\nCounterexample:\nx = 3, a = 0\ny = 0\n\nTransaction trace:\nDer.constructor()\nState: x = 0, a = 0\nDer.g(0)\n Base.f() -- internal call +// Warning 6328: (der:173-186): CHC: Assertion violation happens here.\nCounterexample:\nx = 3, a = 0x0\ny = 0\n\nTransaction trace:\nDer.constructor()\nState: x = 0, a = 0x0\nDer.g(0)\n Base.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/imports/import_free_functions.sol b/test/libsolidity/smtCheckerTests/imports/import_free_functions.sol index 4eec2c76a..6e9621b30 100644 --- a/test/libsolidity/smtCheckerTests/imports/import_free_functions.sol +++ b/test/libsolidity/smtCheckerTests/imports/import_free_functions.sol @@ -20,4 +20,4 @@ contract ERC20 { // ==== // SMTEngine: all // ---- -// Warning 3944: (ERC20.sol:121-126): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\n\namount = 1\n\nTransaction trace:\nERC20.constructor()\nERC20.transferFrom(1)\n ERC20.sol:sub(0, 1) -- internal call +// Warning 3944: (ERC20.sol:121-126): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\n\namount = 1\n\nTransaction trace:\nERC20.constructor()\nERC20.transferFrom(1){ msg.sender: 0x52f6 }\n ERC20.sol:sub(0, 1) -- internal call diff --git a/test/libsolidity/smtCheckerTests/imports/import_library_2.sol b/test/libsolidity/smtCheckerTests/imports/import_library_2.sol index d5c42dad6..4d33d4002 100644 --- a/test/libsolidity/smtCheckerTests/imports/import_library_2.sol +++ b/test/libsolidity/smtCheckerTests/imports/import_library_2.sol @@ -25,4 +25,4 @@ contract ERC20 { // ==== // SMTEngine: all // ---- -// Warning 3944: (ERC20.sol:157-162): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\n\namount = 1\n\nTransaction trace:\nERC20.constructor()\nERC20.transferFrom(1)\n SafeMath.sub(0, 1) -- internal call +// Warning 3944: (ERC20.sol:157-162): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\n\namount = 1\n\nTransaction trace:\nERC20.constructor()\nERC20.transferFrom(1){ msg.sender: 0x52f6 }\n SafeMath.sub(0, 1) -- internal call diff --git a/test/libsolidity/smtCheckerTests/inheritance/receive_fallback.sol b/test/libsolidity/smtCheckerTests/inheritance/receive_fallback.sol index 9df407cd2..95ae12019 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/receive_fallback.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/receive_fallback.sol @@ -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: 2 } +// Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.receive(){ msg.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() diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment.sol index 8268d8520..f8091f9df 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment.sol @@ -20,4 +20,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (254-267): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, owner = 0\ny = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, owner = 0\nC.g(1)\n C.f() -- internal call +// Warning 6328: (254-267): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, owner = 0x0\ny = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, owner = 0x0\nC.g(1)\n C.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_multi_branches.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_multi_branches.sol index df6c12cba..9a578cf89 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_multi_branches.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_multi_branches.sol @@ -34,4 +34,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (540-554): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, owner = 0\ny = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, owner = 0\nC.g(1) +// Warning 6328: (540-554): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, owner = 0x0\ny = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, owner = 0x0\nC.g(1){ msg.sender: 0x0 } diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol index e9e1dea53..6a9d4e90a 100644 --- a/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol @@ -9,4 +9,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (100-123): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 65535\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (100-123): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0xffff\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_or_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_or_fixed_bytes.sol index 125e54db5..acbe3fa6d 100644 --- a/test/libsolidity/smtCheckerTests/operators/bitwise_or_fixed_bytes.sol +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_or_fixed_bytes.sol @@ -9,4 +9,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (150-175): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0\nb = 255\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (150-175): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0x0\nb = 0xff\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/bytes_new.sol b/test/libsolidity/smtCheckerTests/operators/bytes_new.sol index e41c8740f..b961c53d5 100644 --- a/test/libsolidity/smtCheckerTests/operators/bytes_new.sol +++ b/test/libsolidity/smtCheckerTests/operators/bytes_new.sol @@ -34,5 +34,5 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6368: (468-472): CHC: Out of bounds access happens here.\nCounterexample:\n\nx = [18, 52, 0]\n\nTransaction trace:\nC.constructor()\nC.h() -// Warning 6368: (490-494): CHC: Out of bounds access happens here.\nCounterexample:\n\nx = [18, 52, 0]\n\nTransaction trace:\nC.constructor()\nC.h() +// Warning 6368: (468-472): CHC: Out of bounds access happens here.\nCounterexample:\n\nx = [0x12, 0x34, 0x0]\n\nTransaction trace:\nC.constructor()\nC.h() +// Warning 6368: (490-494): CHC: Out of bounds access happens here.\nCounterexample:\n\nx = [0x12, 0x34, 0x0]\n\nTransaction trace:\nC.constructor()\nC.h() diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_fixed_bytes.sol index 03e25854e..b634e8468 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_fixed_bytes.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_fixed_bytes.sol @@ -13,4 +13,4 @@ contract C { // SMTEngine: all // ---- // Warning 6321: (51-57): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. -// Warning 6328: (177-191): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0\na = 0\nb = 240\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (177-191): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0x0\na = 0x0\nb = 0xf0\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_fixed_bytes.sol index c80c3fb65..edcf3230b 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_fixed_bytes.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_fixed_bytes.sol @@ -13,4 +13,4 @@ contract C { // SMTEngine: all // ---- // Warning 6321: (51-57): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. -// Warning 6328: (177-191): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0\na = 255\nb = 255\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (177-191): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0x0\na = 0xff\nb = 0xff\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal_2.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal_2.sol index e142ee930..59bd6c7b9 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal_2.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal_2.sol @@ -14,4 +14,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (147-165): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 6579559\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (147-165): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 0x646567\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal_3.sol index 933f15980..3ac248fb2 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal_3.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal_3.sol @@ -17,5 +17,5 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (229-276): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 43595849750559157961410616371195012376776328331498503227444818324475146035296\nz = 43595849750559157961410616371195012376776328331498503227444818324475146035296\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (394-437): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 44959890247538927454655645290332771782915717053340361485195502024921998844258\nz = 44959890247538927454655645290332771782915717053340361485195502024921998844258\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (229-276): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 0x6062606464666060606260646466606060626064646660606062606464666060\nz = 0x6062606464666060606260646466606060626064646660606062606464666060\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (394-437): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 0x63666566676e616263666566676e616263666566676e616263666566676e6162\nz = 0x63666566676e616263666566676e616263666566676e616263666566676e6162\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_fixed_bytes.sol index 5d53d9132..6856f72e0 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_fixed_bytes.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_fixed_bytes.sol @@ -13,4 +13,4 @@ contract C { // SMTEngine: all // ---- // Warning 6321: (51-57): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. -// Warning 6328: (178-195): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0\na = 255\nb = 240\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (178-195): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0x0\na = 0xff\nb = 0xf0\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol b/test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol index 8a27f6f63..4cb34c49e 100644 --- a/test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol +++ b/test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol @@ -9,4 +9,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (152-173): CHC: Assertion violation happens here.\nCounterexample:\n\nx = [0, 17, 34, 51]\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (152-173): CHC: Assertion violation happens here.\nCounterexample:\n\nx = [0x0, 0x11, 0x22, 0x33]\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/out_of_bounds/fixed_bytes_2.sol b/test/libsolidity/smtCheckerTests/out_of_bounds/fixed_bytes_2.sol index ab1275ab2..f4e90ddb7 100644 --- a/test/libsolidity/smtCheckerTests/out_of_bounds/fixed_bytes_2.sol +++ b/test/libsolidity/smtCheckerTests/out_of_bounds/fixed_bytes_2.sol @@ -6,4 +6,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6368: (83-87): CHC: Out of bounds access happens here.\nCounterexample:\n\nx = 0\ny = 4\n = 0\n\nTransaction trace:\nC.constructor()\nC.r(0, 4) +// Warning 6368: (83-87): CHC: Out of bounds access happens here.\nCounterexample:\n\nx = 0x0\ny = 4\n = 0x0\n\nTransaction trace:\nC.constructor()\nC.r(0x0, 4) diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol index bb82c659e..618f76276 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol @@ -13,4 +13,4 @@ contract C { // Warning 2072: (82-86): Unused local variable. // Warning 2072: (140-150): Unused local variable. // Warning 2072: (152-156): Unused local variable. -// 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 6328: (220-236): CHC: Assertion violation happens here.\nCounterexample:\n\na1 = 2437\nb1 = 0x0a\nc1 = 9\na2 = 2437\nb2 = 0x0a\nc2 = 9\n\nTransaction trace:\nC.constructor()\nC.f(data) diff --git a/test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol b/test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol index ca4873d67..2ebf4d326 100644 --- a/test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol +++ b/test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol @@ -25,8 +25,11 @@ contract C { assert(gas == block.gaslimit); // should hold with CHC assert(number == block.number); // should hold with CHC assert(timestamp == block.timestamp); // should hold with CHC + + assert(coin == address(this)); // should fail } } // ==== // SMTEngine: chc // ---- +// Warning 6328: (770-799): CHC: Assertion violation happens here.\nCounterexample:\ncoin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\n\nTransaction trace:\nC.constructor()\nState: coin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\nC.f(){ block.coinbase: 0x0, block.difficulty: 0, block.gaslimit: 0, block.number: 0, block.timestamp: 0 }\n C.g() -- internal call diff --git a/test/libsolidity/smtCheckerTests/special/msg_parens_1.sol b/test/libsolidity/smtCheckerTests/special/msg_parens_1.sol index 9a1df3724..6eb19e5e8 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_parens_1.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_parens_1.sol @@ -7,6 +7,7 @@ contract C { // ==== // SMTEngine: all // SMTIgnoreOS: macos +// SMTIgnoreCex: yes // ---- -// Warning 6328: (46-71): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(){ value: 11 } -// Warning 6328: (75-113): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (46-71): CHC: Assertion violation happens here. +// Warning 6328: (75-113): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/special/msg_sig.sol b/test/libsolidity/smtCheckerTests/special/msg_sig.sol index a87dc18b3..cf701f6d0 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_sig.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_sig.sol @@ -25,6 +25,6 @@ contract C // ==== // SMTEngine: all // ---- -// Warning 6328: (43-72): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (370-399): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()\n C.fi() -- internal call\n C.gi() -- internal call -// Warning 6328: (510-539): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.h() +// Warning 6328: (43-72): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(){ msg.sig: 0x26121ff0 } +// Warning 6328: (370-399): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(){ msg.sig: 0x26121ff0 }\n C.fi() -- internal call\n C.gi() -- internal call +// Warning 6328: (510-539): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.h(){ msg.sig: 0xb8c9d365 } diff --git a/test/libsolidity/smtCheckerTests/special/msg_value_1.sol b/test/libsolidity/smtCheckerTests/special/msg_value_1.sol index 9888d326d..51e696f56 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_value_1.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_value_1.sol @@ -6,5 +6,5 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 4984: (55-68): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(){ value: 115792089237316195423570985008687907853269984665640564039457584007913129639931 } -// Warning 4984: (55-80): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(){ value: 57896044618658097711785492504343953926634992332820282019728792003956564819966 } +// Warning 4984: (55-68): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(){ msg.value: 115792089237316195423570985008687907853269984665640564039457584007913129639931 } +// Warning 4984: (55-80): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(){ msg.value: 57896044618658097711785492504343953926634992332820282019728792003956564819966 } diff --git a/test/libsolidity/smtCheckerTests/special/msg_value_2.sol b/test/libsolidity/smtCheckerTests/special/msg_value_2.sol index 1c37ce029..acf1b9e5d 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_value_2.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_value_2.sol @@ -6,4 +6,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (46-67): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (46-67): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(){ msg.value: 0 } diff --git a/test/libsolidity/smtCheckerTests/special/msg_value_4.sol b/test/libsolidity/smtCheckerTests/special/msg_value_4.sol index f9bfb0173..82edb4a39 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_value_4.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_value_4.sol @@ -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: 39 } +// Warning 6328: (154-176): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nB.constructor(){ msg.value: 39 } diff --git a/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_1.sol b/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_1.sol index 00e183832..8b69352c2 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_1.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_1.sol @@ -14,4 +14,4 @@ contract C is A { // ==== // SMTEngine: all // ---- -// Warning 6328: (68-82): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nA.constructor(){ value: 1 } +// Warning 6328: (68-82): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nA.constructor(){ msg.value: 1 } diff --git a/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_2.sol b/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_2.sol index efc59fcfc..10b8ef0c2 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_2.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_2.sol @@ -14,5 +14,5 @@ contract C is A { // ==== // SMTEngine: all // ---- -// Warning 6328: (60-74): CHC: Assertion violation happens here.\nCounterexample:\nv = 0, x = 1\n\nTransaction trace:\nC.constructor(){ value: 1 } -// Warning 6328: (240-254): CHC: Assertion violation happens here.\nCounterexample:\nv = 1, x = 1\n\nTransaction trace:\nC.constructor(){ value: 1 } +// Warning 6328: (60-74): CHC: Assertion violation happens here.\nCounterexample:\nv = 0, x = 1\n\nTransaction trace:\nC.constructor(){ msg.value: 1 } +// Warning 6328: (240-254): CHC: Assertion violation happens here.\nCounterexample:\nv = 1, x = 1\n\nTransaction trace:\nC.constructor(){ msg.value: 1 } diff --git a/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_3.sol b/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_3.sol index 08457c0ec..4e1d2a99f 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_3.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_3.sol @@ -19,4 +19,4 @@ contract C is A, B { // ==== // SMTEngine: all // ---- -// Warning 6328: (60-74): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(){ value: 1 } +// Warning 6328: (60-74): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(){ msg.value: 1 } diff --git a/test/libsolidity/smtCheckerTests/special/msg_vars_chc_internal.sol b/test/libsolidity/smtCheckerTests/special/msg_vars_chc_internal.sol index e8190ce3a..b7984d21e 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_vars_chc_internal.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_vars_chc_internal.sol @@ -21,8 +21,11 @@ contract C { assert(sender == msg.sender); // should hold with CHC assert(sig == msg.sig); // should hold with CHC assert(value == msg.value); // should hold with CHC + + assert(msg.value == 10); // should fail } } // ==== // SMTEngine: chc // ---- +// Warning 6328: (621-644): CHC: Assertion violation happens here.\nCounterexample:\ndata = [0x26, 0x12, 0x1f, 0xf0], sender = 0x0, sig = 0x26121ff0, value = 0\n\nTransaction trace:\nC.constructor()\nState: data = [], sender = 0x0, sig = 0x0, value = 0\nC.f(){ msg.data: [0x26, 0x12, 0x1f, 0xf0], msg.sender: 0x0, msg.sig: 0x26121ff0, msg.value: 0 }\n C.g() -- internal call diff --git a/test/libsolidity/smtCheckerTests/special/shadowing_1.sol b/test/libsolidity/smtCheckerTests/special/shadowing_1.sol new file mode 100644 index 000000000..d54548314 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/shadowing_1.sol @@ -0,0 +1,24 @@ +contract C { + struct S { + uint value; + address origin; + uint number; + } + function f() public payable { + S memory msg = S(42, address(0), 666); + S memory tx = S(42, address(0), 666); + S memory block = S(42, address(0), 666); + assert(msg.value == 42); // should hold + assert(msg.value == 41); // should fail + assert(tx.origin == address(0)); // should hold + assert(block.number == 666); // should hold + } +} +// ==== +// SMTEngine: all +// SMTIgnoreCex: yes +// ---- +// Warning 2319: (108-120): This declaration shadows a builtin symbol. +// Warning 2319: (149-160): This declaration shadows a builtin symbol. +// Warning 2319: (189-203): This declaration shadows a builtin symbol. +// Warning 6328: (274-297): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/special/timestamp_2.sol b/test/libsolidity/smtCheckerTests/special/timestamp_2.sol index 73af1d4da..7173185da 100644 --- a/test/libsolidity/smtCheckerTests/special/timestamp_2.sol +++ b/test/libsolidity/smtCheckerTests/special/timestamp_2.sol @@ -9,4 +9,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 4984: (107-126): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\nTransaction trace:\nC.constructor() +// Warning 4984: (107-126): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\nTransaction trace:\nC.constructor(){ block.timestamp: 115792089237316195423570985008687907853269984665640564039457584007913129639935 } diff --git a/test/libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol b/test/libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol index 53ce010aa..ad958fe95 100644 --- a/test/libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol +++ b/test/libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol @@ -13,8 +13,11 @@ contract C { assert(gas == tx.gasprice); // should hold with CHC assert(origin == tx.origin); // should hold with CHC + + assert(tx.origin == address(this)); // should fail } } // ==== // SMTEngine: chc // ---- +// Warning 6328: (343-377): CHC: Assertion violation happens here.\nCounterexample:\ngas = 0, origin = 0x0\n\nTransaction trace:\nC.constructor()\nState: gas = 0, origin = 0x0\nC.f(){ tx.gasprice: 0, tx.origin: 0x0 }\n C.g() -- internal call diff --git a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol new file mode 100644 index 000000000..50260aa3d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol @@ -0,0 +1,16 @@ +interface I { + function f() external; +} + +contract C { + function g(I _i) public payable { + uint x = address(this).balance; + _i.f(); + assert(x == address(this).balance); // should fail + } +} +// ==== +// SMTEngine: all +// SMTIgnoreOS: macos +// ---- +// Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 841\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 38 }\n _i.f() -- untrusted external call, synthesized as:\n C.g(0){ msg.value: 0 } -- reentrant call\n _i.f() -- untrusted external call diff --git a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_2.sol b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_2.sol new file mode 100644 index 000000000..aaddec5b5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_2.sol @@ -0,0 +1,16 @@ +interface I { + function f() external payable; +} + +contract C { + function g(I _i) public payable { + uint x = address(this).balance; + _i.f{ value: 100 }(); + assert(x == address(this).balance); // should fail + } +} +// ==== +// SMTEngine: all +// SMTIgnoreOS: macos +// ---- +// Warning 6328: (157-191): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 2537\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 38 }\n _i.f{ value: 100 }() -- untrusted external call diff --git a/test/libsolidity/smtCheckerTests/typecast/address_literal.sol b/test/libsolidity/smtCheckerTests/typecast/address_literal.sol index c37c36ded..d56275fed 100644 --- a/test/libsolidity/smtCheckerTests/typecast/address_literal.sol +++ b/test/libsolidity/smtCheckerTests/typecast/address_literal.sol @@ -22,4 +22,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (454-468): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\nb = 1\nc = 0\nd = 0\ne = 305419896\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g() +// Warning 6328: (454-468): CHC: Assertion violation happens here.\nCounterexample:\nx = 0x0\na = 0x0\nb = 0x01\nc = 0x0\nd = 0x0\ne = 0x12345678\n\nTransaction trace:\nC.constructor()\nState: x = 0x0\nC.g() diff --git a/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol b/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol index 6f2dd33a4..91166baa8 100644 --- a/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol +++ b/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol @@ -16,7 +16,7 @@ contract C { } } // ---- -// Warning 6328: (225-256): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 283686952306183\nd = 0\ne = 0\ng = 0\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (352-399): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 283686952306183\nd = 5233100606242806050944357496980485\ne = 0\ng = 0\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (526-589): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 283686952306183\nd = 5233100606242806050944357496980485\ne = 96533667595335344310996525432040024692804347064549891\ng = 0\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (732-811): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 283686952306183\nd = 5233100606242806050944357496980485\ne = 96533667595335344310996525432040024692804347064549891\ng = 1780731860627700044956966451854862080991451332659079878538166652776284161\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (225-256): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x0\ne = 0x0\ng = 0x0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (352-399): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x010203040506070809000102030405\ne = 0x0\ng = 0x0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (526-589): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x010203040506070809000102030405\ne = 0x0102030405060708090001020304050607080900010203\ng = 0x0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (732-811): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x010203040506070809000102030405\ne = 0x0102030405060708090001020304050607080900010203\ng = 0x01020304050607080900010203040506070809000102030405060708090001\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_larger_3.sol b/test/libsolidity/smtCheckerTests/typecast/cast_larger_3.sol index b8a69f946..3a14cbb24 100644 --- a/test/libsolidity/smtCheckerTests/typecast/cast_larger_3.sol +++ b/test/libsolidity/smtCheckerTests/typecast/cast_larger_3.sol @@ -12,4 +12,4 @@ contract C // ==== // SMTEngine: all // ---- -// Warning 6328: (240-254): CHC: Assertion violation happens here.\nCounterexample:\n\na = 4660\nb = 305397760\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (240-254): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0x1234\nb = 0x12340000\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/typecast/implicit_cast_string_literal_byte.sol b/test/libsolidity/smtCheckerTests/typecast/implicit_cast_string_literal_byte.sol index 6acb0d16f..093a20d7f 100644 --- a/test/libsolidity/smtCheckerTests/typecast/implicit_cast_string_literal_byte.sol +++ b/test/libsolidity/smtCheckerTests/typecast/implicit_cast_string_literal_byte.sol @@ -13,4 +13,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (153-174): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\nb = 0\n\nTransaction trace:\nC.constructor()\nC.f()\n C.g(0) -- internal call +// Warning 6328: (153-174): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\nb = 0x0\n\nTransaction trace:\nC.constructor()\nC.f()\n C.g(0x0) -- internal call diff --git a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_dynamic_bytes.sol b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_dynamic_bytes.sol index 04d973b99..db54c9035 100644 --- a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_dynamic_bytes.sol +++ b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_dynamic_bytes.sol @@ -9,4 +9,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (173-207): CHC: Assertion violation happens here.\nCounterexample:\n\nb = [255, 255]\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (173-207): CHC: Assertion violation happens here.\nCounterexample:\n\nb = [0xff, 0xff]\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_modifier.sol b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_modifier.sol index 4d1d832f9..c3fda61b8 100644 --- a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_modifier.sol +++ b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_modifier.sol @@ -9,4 +9,4 @@ contract B { // ==== // SMTEngine: all // ---- -// Warning 6328: (120-142): CHC: Assertion violation happens here.\nCounterexample:\n\na = 13564890559296822\n\nTransaction trace:\nB.constructor()\nB.f() +// Warning 6328: (120-142): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0x30313233343536\n\nTransaction trace:\nB.constructor()\nB.f() diff --git a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_return_multi.sol b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_return_multi.sol index c869fca05..e443beb43 100644 --- a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_return_multi.sol +++ b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_return_multi.sol @@ -13,4 +13,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (410-429): CHC: Assertion violation happens here.\nCounterexample:\n\nv1 = 44048180597813453602326562734351324025098966208897425494240603688123167145984\nv2 = 6579558\n\nTransaction trace:\nC.constructor()\nC.a()\n C.f2() -- internal call\n C.h() -- internal call +// Warning 6328: (410-429): CHC: Assertion violation happens here.\nCounterexample:\n\nv1 = 0x6162630000000000000000000000000000000000000000000000000000000000\nv2 = 0x646566\n\nTransaction trace:\nC.constructor()\nC.a()\n C.f2() -- internal call\n C.h() -- internal call diff --git a/test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol b/test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol index 1b571c9f2..4910c417e 100644 --- a/test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol +++ b/test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol @@ -11,4 +11,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (132-160): CHC: Assertion violation happens here.\nCounterexample:\nx = [97, 98, 99, 97]\n\nTransaction trace:\nC.constructor()\nState: x = []\nC.s() +// Warning 6328: (132-160): CHC: Assertion violation happens here.\nCounterexample:\nx = [0x61, 0x62, 0x63, 0x61]\n\nTransaction trace:\nC.constructor()\nState: x = []\nC.s() diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer.sol b/test/libsolidity/smtCheckerTests/types/address_transfer.sol index 1715a8773..654c24969 100644 --- a/test/libsolidity/smtCheckerTests/types/address_transfer.sol +++ b/test/libsolidity/smtCheckerTests/types/address_transfer.sol @@ -11,5 +11,5 @@ contract C // ==== // SMTEngine: all // ---- -// Warning 6328: (162-186): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nx = 100\n\nTransaction trace:\nC.constructor()\nC.f(0) +// Warning 6328: (162-186): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0x0\nx = 100\n\nTransaction trace:\nC.constructor()\nC.f(0x0) // Warning 1236: (98-113): BMC: Insufficient funds happens here. diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol b/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol index 3cfaabb23..4b55c3241 100644 --- a/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol +++ b/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol @@ -11,6 +11,6 @@ contract C // ==== // SMTEngine: all // ---- -// 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 6328: (180-204): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0x2297\nb = 0x2297\n\nTransaction trace:\nC.constructor()\nC.f(0x2297, 0x2297) // Warning 1236: (101-116): BMC: Insufficient funds happens here. // Warning 1236: (120-136): BMC: Insufficient funds happens here. diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_2.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_2.sol index cb8caa3c7..187689b88 100644 --- a/test/libsolidity/smtCheckerTests/types/fixed_bytes_2.sol +++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_2.sol @@ -12,4 +12,4 @@ contract C // ==== // SMTEngine: all // ---- -// Warning 6328: (83-97): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0)\n C.g() -- internal call +// Warning 6328: (83-97): CHC: Assertion violation happens here.\nCounterexample:\nx = 0x0\ny = 0x0\n\nTransaction trace:\nC.constructor()\nState: x = 0x0\nC.f(0x0)\n C.g() -- internal call diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_4.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_4.sol index ed675ce60..ae3bbf9ce 100644 --- a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_4.sol +++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_4.sol @@ -12,4 +12,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (231-252): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 450552876409790643671482431940419874915447411150352389258589821042463539455\nz = 0\no = 255\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (231-252): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0xff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff\nz = 0x0\no = 0xff\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_5.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_5.sol index d2d4956f2..cb3cd1e0f 100644 --- a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_5.sol +++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_5.sol @@ -11,6 +11,6 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (87-104): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 16909060\nb = 2\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (138-155): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 16909060\nb = 2\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (168-185): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 16909060\nb = 2\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (87-104): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0x01020304\nb = 0x02\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (138-155): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0x01020304\nb = 0x02\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (168-185): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0x01020304\nb = 0x02\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_7.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_7.sol index e264cf713..b97ffbe24 100644 --- a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_7.sol +++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_7.sol @@ -8,5 +8,5 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6368: (99-103): CHC: Out of bounds access happens here.\nCounterexample:\n\ni = 4\nx = 16909060\n\nTransaction trace:\nC.constructor()\nC.f(4) -// Warning 6328: (92-112): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 4\nx = 16909060\n\nTransaction trace:\nC.constructor()\nC.f(4) +// Warning 6368: (99-103): CHC: Out of bounds access happens here.\nCounterexample:\n\ni = 4\nx = 0x01020304\n\nTransaction trace:\nC.constructor()\nC.f(4) +// Warning 6328: (92-112): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 4\nx = 0x01020304\n\nTransaction trace:\nC.constructor()\nC.f(4) diff --git a/test/libsolidity/smtCheckerTests/types/mapping_5.sol b/test/libsolidity/smtCheckerTests/types/mapping_5.sol index 04bec4948..632191a67 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_5.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_5.sol @@ -8,4 +8,4 @@ contract C // ==== // SMTEngine: all // ---- -// Warning 6328: (92-111): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0) +// Warning 6328: (92-111): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0x0\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f(0x0, 0) diff --git a/test/libsolidity/smtCheckerTests/types/static_array_length_1.sol b/test/libsolidity/smtCheckerTests/types/static_array_length_1.sol index dd7b8abd5..e8b6f1a32 100644 --- a/test/libsolidity/smtCheckerTests/types/static_array_length_1.sol +++ b/test/libsolidity/smtCheckerTests/types/static_array_length_1.sol @@ -8,5 +8,5 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (102-122): CHC: Assertion violation happens here.\nCounterexample:\n\na = [9, 9]\n\nTransaction trace:\nC.constructor()\nC.f([9, 9]) -// Warning 6328: (141-161): CHC: Assertion violation happens here.\nCounterexample:\n\na = [9, 9]\n\nTransaction trace:\nC.constructor()\nC.f([9, 9]) +// Warning 6328: (102-122): CHC: Assertion violation happens here.\nCounterexample:\n\na = [0x09, 0x09]\n\nTransaction trace:\nC.constructor()\nC.f([0x09, 0x09]) +// Warning 6328: (141-161): CHC: Assertion violation happens here.\nCounterexample:\n\na = [0x09, 0x09]\n\nTransaction trace:\nC.constructor()\nC.f([0x09, 0x09]) diff --git a/test/libsolidity/smtCheckerTests/types/static_array_length_2.sol b/test/libsolidity/smtCheckerTests/types/static_array_length_2.sol index 11ba621d2..f1128583b 100644 --- a/test/libsolidity/smtCheckerTests/types/static_array_length_2.sol +++ b/test/libsolidity/smtCheckerTests/types/static_array_length_2.sol @@ -8,5 +8,5 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (113-133): CHC: Assertion violation happens here.\nCounterexample:\n\na = [0, 0]\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (152-172): CHC: Assertion violation happens here.\nCounterexample:\n\na = [0, 0]\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (113-133): CHC: Assertion violation happens here.\nCounterexample:\n\na = [0x0, 0x0]\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (152-172): CHC: Assertion violation happens here.\nCounterexample:\n\na = [0x0, 0x0]\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/types/static_array_length_3.sol b/test/libsolidity/smtCheckerTests/types/static_array_length_3.sol index b5f47414c..691c25843 100644 --- a/test/libsolidity/smtCheckerTests/types/static_array_length_3.sol +++ b/test/libsolidity/smtCheckerTests/types/static_array_length_3.sol @@ -9,5 +9,5 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (106-126): CHC: Assertion violation happens here.\nCounterexample:\n\na = [0, 0]\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (145-165): CHC: Assertion violation happens here.\nCounterexample:\n\na = [0, 0]\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (106-126): CHC: Assertion violation happens here.\nCounterexample:\n\na = [0x0, 0x0]\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (145-165): CHC: Assertion violation happens here.\nCounterexample:\n\na = [0x0, 0x0]\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/types/storage_value_vars_1.sol b/test/libsolidity/smtCheckerTests/types/storage_value_vars_1.sol index acdaf3ae0..e1523a380 100644 --- a/test/libsolidity/smtCheckerTests/types/storage_value_vars_1.sol +++ b/test/libsolidity/smtCheckerTests/types/storage_value_vars_1.sol @@ -20,4 +20,4 @@ contract C // ==== // SMTEngine: all // ---- -// Warning 6328: (330-389): CHC: Assertion violation happens here.\nCounterexample:\na = 512, b = false, c = 0\nx = 1\n\nTransaction trace:\nC.constructor()\nState: a = 0, b = false, c = 0\nC.f(1) +// Warning 6328: (330-389): CHC: Assertion violation happens here.\nCounterexample:\na = 0x0200, b = false, c = 0\nx = 1\n\nTransaction trace:\nC.constructor()\nState: a = 0x0, b = false, c = 0\nC.f(1) diff --git a/test/libsolidity/smtCheckerTests/types/storage_value_vars_2.sol b/test/libsolidity/smtCheckerTests/types/storage_value_vars_2.sol index 77ef26488..6bda2d66b 100644 --- a/test/libsolidity/smtCheckerTests/types/storage_value_vars_2.sol +++ b/test/libsolidity/smtCheckerTests/types/storage_value_vars_2.sol @@ -10,4 +10,4 @@ contract C // ==== // SMTEngine: all // ---- -// Warning 6328: (91-104): CHC: Assertion violation happens here.\nCounterexample:\na = 0, b = false, c = 0\n\nTransaction trace:\nC.constructor()\nState: a = 0, b = false, c = 0\nC.f() +// Warning 6328: (91-104): CHC: Assertion violation happens here.\nCounterexample:\na = 0x0, b = false, c = 0\n\nTransaction trace:\nC.constructor()\nState: a = 0x0, b = false, c = 0\nC.f() diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_1.sol b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_1.sol index 8015d2a1e..c568b2267 100644 --- a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_1.sol +++ b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_1.sol @@ -10,4 +10,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (142-157): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293568\ny = 52647538817385212172903286807934654968315727694643370704309751478220717293568\nz = 154717211199090701642289212291190620160\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293568) +// Warning 6328: (142-157): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 0x7465737400000000000000000000000000000000000000000000000000000000\ny = 0x7465737400000000000000000000000000000000000000000000000000000000\nz = 0x746573747a0000000000000000000000\n\nTransaction trace:\nC.constructor()\nC.f(0x7465737400000000000000000000000000000000000000000000000000000000) diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_2.sol b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_2.sol index c534ce93b..fc68b7958 100644 --- a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_2.sol +++ b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_2.sol @@ -9,4 +9,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (143-158): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293568\ny = 52647538817385212172903286807934654968315727694643370704309751478220717293568\nz = 154717211199090701642289212291190620160\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293568) +// Warning 6328: (143-158): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 0x7465737400000000000000000000000000000000000000000000000000000000\ny = 0x7465737400000000000000000000000000000000000000000000000000000000\nz = 0x746573747a0000000000000000000000\n\nTransaction trace:\nC.constructor()\nC.f(0x7465737400000000000000000000000000000000000000000000000000000000) diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_3.sol b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_3.sol index b6fe29658..7219e15bd 100644 --- a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_3.sol +++ b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_3.sol @@ -11,4 +11,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (153-168): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293568\ny = 52647538817385212172903286807934654968315727694643370704309751478220717293568\nz = 154717211199090701642289212291190620160\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293568) +// Warning 6328: (153-168): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 0x7465737400000000000000000000000000000000000000000000000000000000\ny = 0x7465737400000000000000000000000000000000000000000000000000000000\nz = 0x746573747a0000000000000000000000\n\nTransaction trace:\nC.constructor()\nC.f(0x7465737400000000000000000000000000000000000000000000000000000000) diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_4.sol b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_4.sol index 8514d785d..954aee7f4 100644 --- a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_4.sol +++ b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_4.sol @@ -15,4 +15,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (228-243): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293568\ny = 52647538817385212172903286807934654968315727694643370704309751478220717293568\nz = 154717211199090701642289212291190620160\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293568)\n C.g() -- internal call +// Warning 6328: (228-243): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 0x7465737400000000000000000000000000000000000000000000000000000000\ny = 0x7465737400000000000000000000000000000000000000000000000000000000\nz = 0x746573747a0000000000000000000000\n\nTransaction trace:\nC.constructor()\nC.f(0x7465737400000000000000000000000000000000000000000000000000000000)\n C.g() -- internal call diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_5.sol b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_5.sol index 9586b7b3e..71e331122 100644 --- a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_5.sol +++ b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_5.sol @@ -13,4 +13,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (218-233): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293568\ny = 52647538817385212172903286807934654968315727694643370704309751478220717293568\nz = 154717211199090701642289212291190620160\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293568)\n C.g() -- internal call +// Warning 6328: (218-233): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 0x7465737400000000000000000000000000000000000000000000000000000000\ny = 0x7465737400000000000000000000000000000000000000000000000000000000\nz = 0x746573747a0000000000000000000000\n\nTransaction trace:\nC.constructor()\nC.f(0x7465737400000000000000000000000000000000000000000000000000000000)\n C.g() -- internal call diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_comparison_1.sol b/test/libsolidity/smtCheckerTests/types/string_literal_comparison_1.sol index 72c4b500d..3c5742e65 100644 --- a/test/libsolidity/smtCheckerTests/types/string_literal_comparison_1.sol +++ b/test/libsolidity/smtCheckerTests/types/string_literal_comparison_1.sol @@ -10,4 +10,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (137-157): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293568\ny = 52647538817385212172903286807934654968315727694643370704309751478220717293568\nz = 52647538817385212172903286807934654968315727694643370704309751478220717293568\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293568) +// Warning 6328: (137-157): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 0x7465737400000000000000000000000000000000000000000000000000000000\ny = 0x7465737400000000000000000000000000000000000000000000000000000000\nz = 0x7465737400000000000000000000000000000000000000000000000000000000\n\nTransaction trace:\nC.constructor()\nC.f(0x7465737400000000000000000000000000000000000000000000000000000000) diff --git a/test/libsolidity/smtCheckerTests/unchecked/check_var_init.sol b/test/libsolidity/smtCheckerTests/unchecked/check_var_init.sol index 805409c01..b7d19c0bd 100644 --- a/test/libsolidity/smtCheckerTests/unchecked/check_var_init.sol +++ b/test/libsolidity/smtCheckerTests/unchecked/check_var_init.sol @@ -16,5 +16,5 @@ contract D { // ==== // SMTEngine: all // ---- -// Warning 3944: (33-47): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor() +// Warning 3944: (33-47): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor(){ msg.value: 0 } // Warning 3944: (160-174): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\n\n\nTransaction trace:\nD.constructor()\nD.f()\n D.h() -- internal call diff --git a/test/libsolidity/smtCheckerTests/userTypes/multisource.sol b/test/libsolidity/smtCheckerTests/userTypes/multisource.sol index fef83a8ee..23fbef98a 100644 --- a/test/libsolidity/smtCheckerTests/userTypes/multisource.sol +++ b/test/libsolidity/smtCheckerTests/userTypes/multisource.sol @@ -18,4 +18,4 @@ contract A { // SMTEngine: all // ---- // Warning 6328: (B:296-332): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nA.constructor()\nA.g()\n A.f(5) -- internal call\n A.f(5) -- internal call -// Warning 6328: (B:409-463): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nA.constructor()\nA.g()\n A.f(5) -- internal call\n A.f(5) -- internal call\n A.f(5) -- internal call\n A.f(5) -- internal call +// Warning 6328: (B:409-463): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nA.constructor()\nA.g()\n A.f(5) -- internal call\n A.f(5) -- internal call\n A.f(0x05) -- internal call\n A.f(0x05) -- internal call