From ba97d6ac4e7068c43a6a689a4e8c366470dffb63 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 21 Jan 2021 19:04:34 +0100 Subject: [PATCH] Add local vars to cex --- Changelog.md | 1 + libsolidity/formal/CHC.cpp | 92 +++++++++++++++++-- libsolidity/formal/CHC.h | 5 + libsolidity/formal/Predicate.cpp | 52 ++++++++++- libsolidity/formal/Predicate.h | 24 ++++- libsolidity/formal/SMTEncoder.cpp | 5 + libsolidity/formal/SMTEncoder.h | 7 ++ .../abi/abi_encode_array_slice_2.sol | 5 +- .../abi/abi_encode_no_arguments.sol | 6 +- .../array_members/length_basic.sol | 2 +- .../length_same_after_assignment_3_fail.sol | 8 +- .../array_members/push_as_lhs_and_rhs_1d.sol | 2 +- .../push_as_lhs_and_rhs_2d_1.sol | 2 +- .../push_as_lhs_and_rhs_bytes.sol | 2 +- .../array_members/push_as_lhs_bytes.sol | 2 +- .../array_members/push_as_lhs_bytes_2d.sol | 2 +- .../push_push_no_args_2_fail.sol | 6 +- .../push_storage_ref_unsafe_aliasing.sol | 6 +- .../push_storage_ref_unsafe_length.sol | 8 +- .../blockchain_state/transfer.sol | 4 +- .../branches_inside_modifiers_4.sol | 4 +- .../branches_in_modifiers_2.sol | 2 +- .../control_flow/revert_complex_flow.sol | 2 +- .../control_flow/short_circuit_and_fail.sol | 2 +- .../short_circuit_and_inside_branch.sol | 4 +- .../short_circuit_and_need_both_fail.sol | 2 +- .../control_flow/short_circuit_or_fail.sol | 2 +- .../short_circuit_or_inside_branch.sol | 2 +- .../short_circuit_or_need_both_fail.sol | 2 +- .../ways_to_merge_variables_1.sol | 2 +- .../ways_to_merge_variables_2.sol | 2 +- .../ways_to_merge_variables_3.sol | 2 +- ...ernal_hash_known_code_state_reentrancy.sol | 4 +- ...nal_hash_known_code_state_reentrancy_2.sol | 43 +++++++++ ...nal_hash_known_code_state_reentrancy_3.sol | 42 +++++++++ ...uctor_hierarchy_mixed_chain_local_vars.sol | 2 +- .../functions/functions_bound_1_fail.sol | 2 +- .../functions/functions_identity_1_fail.sol | 2 +- .../functions/functions_identity_2_fail.sol | 2 +- .../functions_identity_as_tuple_fail.sol | 2 +- .../functions/functions_library_1_fail.sol | 2 +- .../functions/getters/address.sol | 4 +- .../functions/getters/array_1.sol | 2 +- .../functions/getters/array_of_structs_2.sol | 2 +- .../functions/getters/array_of_structs_3.sol | 2 +- .../functions/getters/contract.sol | 2 +- .../functions/getters/double_access.sol | 2 +- .../functions/getters/enum.sol | 2 +- .../functions/getters/fixed_bytes.sol | 4 +- .../functions/getters/function.sol | 4 +- .../functions/getters/mapping_1.sol | 2 +- .../functions/getters/mapping_2.sol | 2 +- .../functions/getters/mapping_with_cast.sol | 2 +- .../getters/nested_arrays_mappings_1.sol | 2 +- .../getters/nested_arrays_mappings_7.sol | 2 +- .../getters/nested_arrays_mappings_8.sol | 2 +- .../getters/nested_arrays_mappings_9.sol | 2 +- .../functions/getters/struct_1.sol | 2 +- .../functions/getters/struct_2.sol | 2 +- .../functions/getters/struct_4.sol | 2 +- .../getters/struct_with_reassignment.sol | 4 +- .../functions/getters/uint.sol | 2 +- .../imports/import_library.sol | 2 +- .../base_contract_assertion_fail_1.sol | 2 +- .../inheritance/fallback_receive.sol | 2 +- .../overriden_function_static_call_parent.sol | 4 +- .../smtCheckerTests/inheritance/receive.sol | 4 +- .../inheritance/receive_fallback.sol | 2 +- .../inline_assembly/assembly_2.sol | 2 +- .../inline_assembly/assembly_3.sol | 2 +- ...y_local_storage_access_inside_function.sol | 4 +- .../inline_assembly/assembly_memory_write.sol | 6 +- .../loops/do_while_break_2_fail.sol | 2 +- .../loops/do_while_break_fail.sol | 2 +- .../smtCheckerTests/loops/for_loop_4.sol | 2 +- .../smtCheckerTests/loops/for_loop_5.sol | 2 +- .../loops/while_2_break_fail.sol | 3 +- ...le_loop_array_assignment_memory_memory.sol | 7 +- ..._loop_array_assignment_storage_storage.sol | 6 +- .../loops/while_loop_simple_3.sol | 3 +- .../smtCheckerTests/math/addmod_1.sol | 4 +- .../math/addmod_mulmod_zero.sol | 8 +- .../smtCheckerTests/math/mulmod_1.sol | 4 +- .../modifiers/modifier_multi_functions.sol | 2 +- .../modifiers/modifier_multi_parameters.sol | 2 +- .../modifiers/modifier_overriding_1.sol | 2 +- .../modifiers/modifier_overriding_3.sol | 2 +- .../modifiers/modifier_parameter_copy.sol | 2 +- .../modifier_same_local_variables.sol | 2 +- ...nment_contract_member_variable_array_3.sol | 8 +- .../operators/bitwise_and_int.sol | 2 +- .../operators/bitwise_and_uint.sol | 6 +- .../operators/bitwise_not_fixed_bytes.sol | 2 +- .../operators/bitwise_not_int.sol | 8 +- .../operators/bitwise_not_uint.sol | 4 +- .../operators/bitwise_or_fixed_bytes.sol | 2 +- .../operators/bitwise_or_int.sol | 4 +- .../operators/bitwise_or_uint.sol | 4 +- .../operators/bitwise_rational_2.sol | 2 +- .../operators/bitwise_xor_int.sol | 4 +- .../operators/bitwise_xor_uint.sol | 4 +- .../smtCheckerTests/operators/bytes_new.sol | 4 +- .../operators/compound_add.sol | 2 +- .../compound_assignment_division_1.sol | 2 +- .../compound_bitwise_and_fixed_bytes.sol | 2 +- .../operators/compound_bitwise_and_int.sol | 2 +- .../operators/compound_bitwise_and_uint.sol | 6 +- .../compound_bitwise_or_fixed_bytes.sol | 2 +- .../operators/compound_bitwise_or_int.sol | 2 +- .../operators/compound_bitwise_or_uint.sol | 6 +- .../compound_bitwise_string_literal_2.sol | 2 +- .../compound_bitwise_string_literal_3.sol | 4 +- .../compound_bitwise_xor_fixed_bytes.sol | 2 +- .../operators/compound_bitwise_xor_int.sol | 2 +- .../operators/compound_bitwise_xor_uint.sol | 6 +- .../operators/compound_mul.sol | 2 +- .../operators/compound_sub.sol | 2 +- .../operators/conditional_assignment_1.sol | 2 +- .../operators/conditional_assignment_2.sol | 4 +- .../conditional_assignment_always_true.sol | 2 +- .../conditional_assignment_function_1.sol | 2 +- .../conditional_assignment_nested_unsafe.sol | 2 +- .../operators/delete_array_index_2d.sol | 19 ++-- .../operators/delete_array_push.sol | 4 +- .../smtCheckerTests/operators/division_6.sol | 2 +- .../function_call_named_arguments.sol | 2 +- .../operators/index_access_for_bytes.sol | 2 +- .../smtCheckerTests/operators/integer_new.sol | 4 +- .../shifts/shift_left_larger_type.sol | 2 +- .../smtCheckerTests/operators/unary_add.sol | 2 +- .../unary_add_overflows_correctly.sol | 2 +- .../unary_add_overflows_correctly_struct.sol | 2 +- .../operators/unary_operators_tuple_3.sol | 2 +- .../smtCheckerTests/operators/unary_sub.sol | 2 +- .../smtCheckerTests/out_of_bounds/array_1.sol | 2 +- .../out_of_bounds/array_2d_4.sol | 8 +- .../overflow/overflow_constant_bound.sol | 1 + .../smtCheckerTests/overflow/overflow_mul.sol | 2 +- .../overflow/overflow_mul_cex_with_array.sol | 6 +- .../overflow/overflow_mul_signed.sol | 2 +- .../smtCheckerTests/overflow/overflow_sum.sol | 2 +- .../overflow/signed_guard_sum_overflow.sol | 6 +- .../overflow/signed_sub_overflow.sol | 6 +- .../overflow/signed_sum_overflow.sol | 6 +- .../overflow/unsigned_guard_sum_overflow.sol | 4 +- .../overflow/unsigned_mul_overflow.sol | 2 +- .../overflow/unsigned_sum_overflow.sol | 4 +- .../special/abi_decode_simple.sol | 2 +- .../smtCheckerTests/special/blockhash.sol | 4 +- .../smtCheckerTests/special/difficulty.sol | 4 +- .../smtCheckerTests/special/event.sol | 2 +- .../smtCheckerTests/special/gasleft.sol | 4 +- .../special/msg_sender_fail_1.sol | 4 +- .../smtCheckerTests/special/this.sol | 4 +- .../smtCheckerTests/try_catch/try_1.sol | 2 +- .../smtCheckerTests/try_catch/try_3.sol | 2 +- .../try_catch/try_multiple_catch_clauses.sol | 2 +- .../try_multiple_catch_clauses_2.sol | 2 +- .../try_multiple_returned_values.sol | 4 +- ...ry_multiple_returned_values_with_tuple.sol | 2 +- .../try_catch/try_nested_1.sol | 4 +- .../try_catch/try_nested_2.sol | 2 +- .../try_catch/try_nested_3.sol | 2 +- .../typecast/address_literal.sol | 2 +- .../typecast/cast_larger_2_fail.sol | 2 +- .../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 +- .../smtCheckerTests/types/address_balance.sol | 4 +- .../smtCheckerTests/types/address_call.sol | 9 +- .../types/address_delegatecall.sol | 9 +- .../types/address_transfer.sol | 2 +- .../types/array_aliasing_storage_1.sol | 2 + .../types/array_dynamic_parameter_1_fail.sol | 2 +- .../smtCheckerTests/types/array_literal_2.sol | 2 +- .../smtCheckerTests/types/array_literal_3.sol | 2 +- .../smtCheckerTests/types/array_literal_5.sol | 2 +- .../smtCheckerTests/types/array_literal_6.sol | 4 +- .../smtCheckerTests/types/array_literal_7.sol | 4 +- .../types/array_static_mapping_aliasing_2.sol | 2 + .../types/contract_address_conversion.sol | 4 +- .../types/fixed_bytes_access_4.sol | 2 +- .../types/fixed_bytes_access_5.sol | 6 +- .../types/fixed_bytes_access_7.sol | 4 +- .../types/mapping_as_parameter_1.sol | 4 +- .../types/mapping_equal_keys_2.sol | 2 +- .../types/rational_large_1.sol | 2 +- .../smtCheckerTests/types/string_1.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 +- .../types/string_literal_comparison_2.sol | 4 +- .../types/struct/struct_aliasing_storage.sol | 2 +- ...uct_array_struct_array_memory_unsafe_1.sol | 10 +- ...ct_array_struct_array_storage_unsafe_1.sol | 2 +- .../struct/struct_constructor_named_args.sol | 2 +- .../struct_constructor_named_args_2.sol | 2 +- .../struct/struct_nested_constructor.sol | 2 +- .../types/struct/struct_return.sol | 2 +- .../types/tuple_assignment_compound.sol | 2 +- .../types/tuple_assignment_empty.sol | 2 +- .../tuple_declarations_function_empty.sol | 2 +- .../tuple_different_count_assignment_1.sol | 2 +- .../tuple_different_count_assignment_2.sol | 2 +- .../smtCheckerTests/types/tuple_function.sol | 4 +- .../types/tuple_function_2.sol | 2 +- .../types/tuple_function_3.sol | 4 +- .../checked_modifier_called_by_unchecked.sol | 2 +- .../unchecked/flipping_sign_tests.sol | 2 +- .../smtCheckerTests/unchecked/signed_mod.sol | 2 +- ...ked_function_call_with_unchecked_block.sol | 2 +- 216 files changed, 601 insertions(+), 306 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_3.sol diff --git a/Changelog.md b/Changelog.md index f31dc10c6..a3ce22a8e 100644 --- a/Changelog.md +++ b/Changelog.md @@ -6,6 +6,7 @@ Language Features: Compiler Features: * Commandline Interface: Model checker option ``--model-checker-targets`` also accepts ``outOfBounds``. * Low-Level Inliner: Inline ordinary jumps to small blocks and jumps to small blocks that terminate. + * SMTChecker: Report local variables in CHC counterexamples. * SMTChecker: Report out of bounds index access for arrays and fixed bytes. * Standard JSON: Model checker option ``settings.modelChecker.targets`` also accepts ``outOfBounds``. * Yul Optimizer: Added a new step FunctionSpecializer, that specializes a function with its literal arguments. diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 456e71123..42194c18e 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -32,6 +32,8 @@ #include #include +#include + #include #ifdef HAVE_Z3_DLOPEN @@ -130,6 +132,8 @@ bool CHC::visit(ContractDefinition const& _contract) initContract(_contract); clearIndices(&_contract); + m_scopes.push_back(&_contract); + m_stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract); solAssert(m_currentContract, ""); @@ -208,6 +212,10 @@ void CHC::endVisit(ContractDefinition const& _contract) m_queryPlaceholders[&_contract].push_back({txConstraints, errorFlag().currentValue(), m_currentBlock}); connectBlocks(m_currentBlock, interface(), txConstraints && errorFlag().currentValue() == 0); } + + solAssert(m_scopes.back() == &_contract, ""); + m_scopes.pop_back(); + SMTEncoder::endVisit(_contract); } @@ -223,6 +231,8 @@ bool CHC::visit(FunctionDefinition const& _function) solAssert(!m_currentFunction, "Function inlining should not happen in CHC."); m_currentFunction = &_function; + m_scopes.push_back(&_function); + initFunction(_function); auto functionEntryBlock = createBlock(m_currentFunction, PredicateType::FunctionBlock); @@ -257,6 +267,9 @@ void CHC::endVisit(FunctionDefinition const& _function) // No inlining. solAssert(m_currentFunction == &_function, ""); + solAssert(m_scopes.back() == &_function, ""); + m_scopes.pop_back(); + connectBlocks(m_currentBlock, summary(_function)); setCurrentBlock(*m_summaries.at(m_currentContract).at(&_function)); @@ -282,6 +295,19 @@ void CHC::endVisit(FunctionDefinition const& _function) SMTEncoder::endVisit(_function); } +bool CHC::visit(Block const& _block) +{ + m_scopes.push_back(&_block); + return SMTEncoder::visit(_block); +} + +void CHC::endVisit(Block const& _block) +{ + solAssert(m_scopes.back() == &_block, ""); + m_scopes.pop_back(); + SMTEncoder::endVisit(_block); +} + bool CHC::visit(IfStatement const& _if) { solAssert(m_currentFunction, ""); @@ -382,6 +408,8 @@ bool CHC::visit(WhileStatement const& _while) bool CHC::visit(ForStatement const& _for) { + m_scopes.push_back(&_for); + bool unknownFunctionCallWasSeen = m_unknownFunctionCallSeen; m_unknownFunctionCallSeen = false; @@ -441,6 +469,12 @@ bool CHC::visit(ForStatement const& _for) return false; } +void CHC::endVisit(ForStatement const& _for) +{ + solAssert(m_scopes.back() == &_for, ""); + m_scopes.pop_back(); +} + void CHC::endVisit(FunctionCall const& _funCall) { auto functionCallKind = *_funCall.annotation().kind; @@ -552,6 +586,18 @@ void CHC::endVisit(Return const& _return) m_currentBlock = predicate(*returnGhost); } +bool CHC::visit(TryCatchClause const& _tryStatement) +{ + m_scopes.push_back(&_tryStatement); + return SMTEncoder::visit(_tryStatement); +} + +void CHC::endVisit(TryCatchClause const& _tryStatement) +{ + solAssert(m_scopes.back() == &_tryStatement, ""); + m_scopes.pop_back(); +} + bool CHC::visit(TryStatement const& _tryStatement) { FunctionCall const* externalCall = dynamic_cast(&_tryStatement.externalCall()); @@ -975,7 +1021,7 @@ SortPointer CHC::sort(ASTNode const* _node) Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, PredicateType _predType, ASTNode const* _node, ContractDefinition const* _contractContext) { - auto const* block = Predicate::create(_sort, _name, _predType, m_context, _node, _contractContext); + auto const* block = Predicate::create(_sort, _name, _predType, m_context, _node, _contractContext, m_scopes); m_interface->registerRelation(block->functor()); return block; } @@ -1150,7 +1196,11 @@ Predicate const* CHC::createConstructorBlock(ContractDefinition const& _contract void CHC::createErrorBlock() { - m_errorPredicate = createSymbolicBlock(arity0FunctionSort(), "error_target_" + to_string(m_context.newUniqueId()), PredicateType::Error); + m_errorPredicate = createSymbolicBlock( + arity0FunctionSort(), + "error_target_" + to_string(m_context.newUniqueId()), + PredicateType::Error + ); m_interface->registerRelation(m_errorPredicate->functor()); } @@ -1240,6 +1290,7 @@ smtutil::Expression CHC::predicate(Predicate const& _block) case PredicateType::ExternalCallUntrusted: return smt::function(_block, m_currentContract, m_context); case PredicateType::FunctionBlock: + case PredicateType::FunctionErrorBlock: solAssert(m_currentFunction, ""); return functionBlock(_block, *m_currentFunction, m_currentContract, m_context); case PredicateType::Error: @@ -1375,7 +1426,6 @@ void CHC::verificationTargetEncountered( smtutil::Expression const& _errorCondition ) { - if (!m_settings.targets.has(_type)) return; @@ -1396,13 +1446,18 @@ void CHC::verificationTargetEncountered( auto previousError = errorFlag().currentValue(); errorFlag().increaseIndex(); - // create an error edge to the summary - solAssert(m_errorDest, ""); + Predicate const* localBlock = m_currentFunction ? + createBlock(m_currentFunction, PredicateType::FunctionErrorBlock) : + createConstructorBlock(*m_currentContract, "local_error"); + + auto pred = predicate(*localBlock); connectBlocks( m_currentBlock, - predicate(*m_errorDest), + pred, _errorCondition && errorFlag().currentValue() == errorId ); + solAssert(m_errorDest, ""); + addRule(smtutil::Expression::implies(pred, predicate(*m_errorDest)), pred.name); m_context.addAssertion(errorFlag().currentValue() == previousError); } @@ -1606,6 +1661,7 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& first = false; /// Generate counterexample message local to the failed target. localState = formatVariableModel(*stateVars, stateValues, ", ") + "\n"; + if (auto calledFun = summaryPredicate->programFunction()) { auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs); @@ -1616,6 +1672,30 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& auto const& outParams = calledFun->returnParameters(); if (auto outStr = formatVariableModel(outParams, outValues, "\n"); !outStr.empty()) localState += outStr + "\n"; + + optional localErrorId; + solidity::util::BreadthFirstSearch bfs{{summaryId}}; + bfs.run([&](auto _nodeId, auto&& _addChild) { + auto const& children = _graph.edges.at(_nodeId); + if ( + children.size() == 1 && + nodePred(children.front())->isFunctionErrorBlock() + ) + { + localErrorId = children.front(); + bfs.abort(); + } + ranges::for_each(children, _addChild); + }); + + if (localErrorId.has_value()) + { + auto const* localError = nodePred(*localErrorId); + solAssert(localError && localError->isFunctionErrorBlock(), ""); + auto const [localValues, localVars] = localError->localVariableValues(nodeArgs(*localErrorId)); + if (auto localStr = formatVariableModel(localVars, localValues, "\n"); !localStr.empty()) + localState += localStr + "\n"; + } } } else diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index ef6d0ec69..4d09556f2 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -77,14 +77,19 @@ private: void endVisit(ContractDefinition const& _node) override; bool visit(FunctionDefinition const& _node) override; void endVisit(FunctionDefinition const& _node) override; + bool visit(Block const& _block) override; + void endVisit(Block const& _block) override; bool visit(IfStatement const& _node) override; bool visit(WhileStatement const&) override; bool visit(ForStatement const&) override; + void endVisit(ForStatement const&) override; void endVisit(FunctionCall const& _node) override; void endVisit(Break const& _node) override; void endVisit(Continue const& _node) override; void endVisit(IndexRangeAccess const& _node) override; void endVisit(Return const& _node) override; + bool visit(TryCatchClause const&) override; + void endVisit(TryCatchClause const&) override; bool visit(TryStatement const& _node) override; void pushInlineFrame(CallableDeclaration const& _callable) override; diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index 812e907c3..064815869 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -41,7 +41,8 @@ Predicate const* Predicate::create( PredicateType _type, EncodingContext& _context, ASTNode const* _node, - ContractDefinition const* _contractContext + ContractDefinition const* _contractContext, + vector _scopeStack ) { smt::SymbolicFunctionVariable predicate{_sort, move(_name), _context}; @@ -50,7 +51,7 @@ Predicate const* Predicate::create( return &m_predicates.emplace( std::piecewise_construct, std::forward_as_tuple(functorName), - std::forward_as_tuple(move(predicate), _type, _node, _contractContext) + std::forward_as_tuple(move(predicate), _type, _node, _contractContext, move(_scopeStack)) ).first->second; } @@ -58,12 +59,14 @@ Predicate::Predicate( smt::SymbolicFunctionVariable&& _predicate, PredicateType _type, ASTNode const* _node, - ContractDefinition const* _contractContext + ContractDefinition const* _contractContext, + vector _scopeStack ): m_predicate(move(_predicate)), m_type(_type), m_node(_node), - m_contractContext(_contractContext) + m_contractContext(_contractContext), + m_scopeStack(_scopeStack) { } @@ -102,6 +105,11 @@ ASTNode const* Predicate::programNode() const return m_node; } +ContractDefinition const* Predicate::contextContract() const +{ + return m_contractContext; +} + ContractDefinition const* Predicate::programContract() const { if (auto const* contract = dynamic_cast(m_node)) @@ -153,6 +161,16 @@ bool Predicate::isFunctionSummary() const return m_type == PredicateType::FunctionSummary; } +bool Predicate::isFunctionBlock() const +{ + return m_type == PredicateType::FunctionBlock; +} + +bool Predicate::isFunctionErrorBlock() const +{ + return m_type == PredicateType::FunctionErrorBlock; +} + bool Predicate::isInternalCall() const { return m_type == PredicateType::InternalCall; @@ -308,6 +326,32 @@ vector> Predicate::summaryPostOutputValues(vector>, vector> Predicate::localVariableValues(vector const& _args) const +{ + /// The signature of a local block predicate is: + /// block(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars, localVars). + /// Here we are interested in localVars. + auto const* function = programFunction(); + solAssert(function, ""); + + auto const& localVars = SMTEncoder::localVariablesIncludingModifiers(*function, m_contractContext); + auto first = _args.end() - static_cast(localVars.size()); + vector outValues(first, _args.end()); + + auto mask = applyMap( + localVars, + [this](auto _var) { + auto varScope = dynamic_cast(_var->scope()); + return find(begin(m_scopeStack), end(m_scopeStack), varScope) != end(m_scopeStack); + } + ); + auto localVarsInScope = util::filter(localVars, mask); + auto outValuesInScope = util::filter(outValues, mask); + + auto outTypes = applyMap(localVarsInScope, [](auto _var) { return _var->type(); }); + return {formatExpressions(outValuesInScope, outTypes), localVarsInScope}; +} + vector> Predicate::formatExpressions(vector const& _exprs, vector const& _types) const { solAssert(_exprs.size() == _types.size(), ""); diff --git a/libsolidity/formal/Predicate.h b/libsolidity/formal/Predicate.h index 430734275..ee9a13716 100644 --- a/libsolidity/formal/Predicate.h +++ b/libsolidity/formal/Predicate.h @@ -37,6 +37,7 @@ enum class PredicateType ConstructorSummary, FunctionSummary, FunctionBlock, + FunctionErrorBlock, InternalCall, ExternalCallTrusted, ExternalCallUntrusted, @@ -56,14 +57,16 @@ public: PredicateType _type, smt::EncodingContext& _context, ASTNode const* _node = nullptr, - ContractDefinition const* _contractContext = nullptr + ContractDefinition const* _contractContext = nullptr, + std::vector _scopeStack = {} ); Predicate( smt::SymbolicFunctionVariable&& _predicate, PredicateType _type, ASTNode const* _node = nullptr, - ContractDefinition const* _contractContext = nullptr + ContractDefinition const* _contractContext = nullptr, + std::vector _scopeStack = {} ); /// Predicate should not be copiable. @@ -89,6 +92,10 @@ public: /// @returns the program node this predicate represents. ASTNode const* programNode() const; + /// @returns the ContractDefinition of the most derived contract + /// being analyzed. + ContractDefinition const* contextContract() const; + /// @returns the ContractDefinition that this predicate represents /// or nullptr otherwise. ContractDefinition const* programContract() const; @@ -110,6 +117,12 @@ public: /// @returns true if this predicate represents a function summary. bool isFunctionSummary() const; + /// @returns true if this predicate represents a function block. + bool isFunctionBlock() const; + + /// @returns true if this predicate represents a function error block. + bool isFunctionErrorBlock() const; + /// @returns true if this predicate represents an internal function call. bool isInternalCall() const; @@ -143,6 +156,9 @@ public: /// where this summary was reached. std::vector> summaryPostOutputValues(std::vector const& _args) const; + /// @returns the values of the local variables used by this predicate. + std::pair>, std::vector> localVariableValues(std::vector const& _args) const; + private: /// @returns the formatted version of the given SMT expressions. Those expressions must be SMT constants. std::vector> formatExpressions(std::vector const& _exprs, std::vector const& _types) const; @@ -177,6 +193,10 @@ private: /// Maps the name of the predicate to the actual Predicate. /// Used in counterexample generation. static std::map m_predicates; + + /// The scope stack when the predicate was created. + /// Used to identify the subset of variables in scope. + std::vector const m_scopeStack; }; } diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 3dd7b8a28..9cb9472d1 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -192,7 +192,12 @@ void SMTEncoder::visitFunctionOrModifier() if (dynamic_cast(refDecl)) visitFunctionOrModifier(); else if (auto modifier = resolveModifierInvocation(*modifierInvocation, m_currentContract)) + { + m_scopes.push_back(modifier); inlineModifierInvocation(modifierInvocation.get(), modifier); + solAssert(m_scopes.back() == modifier, ""); + m_scopes.pop_back(); + } else solAssert(false, ""); } diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index fa9ba796f..00236bf2a 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -129,6 +129,7 @@ protected: bool visit(IfStatement const&) override { return false; } bool visit(WhileStatement const&) override { return false; } bool visit(ForStatement const&) override { return false; } + void endVisit(ForStatement const&) override {} void endVisit(VariableDeclarationStatement const& _node) override; bool visit(Assignment const& _node) override; void endVisit(Assignment const& _node) override; @@ -150,6 +151,8 @@ protected: bool visit(InlineAssembly const& _node) override; void endVisit(Break const&) override {} void endVisit(Continue const&) override {} + bool visit(TryCatchClause const&) override { return true; } + void endVisit(TryCatchClause const&) override {} bool visit(TryStatement const&) override { return false; } virtual void pushInlineFrame(CallableDeclaration const&); @@ -400,6 +403,10 @@ protected: /// Stores the current function/modifier call/invocation path. std::vector m_callStack; + + /// Stack of scopes. + std::vector m_scopes; + /// Returns true if the current function was not visited by /// a function call. bool isRootFunction(); diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice_2.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice_2.sol index c7b8dee56..e1261521c 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice_2.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice_2.sol @@ -19,7 +19,8 @@ contract C { uint y = 10; bytes memory b5 = abi.encode(data[x:y]); // should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately - assert(b1.length == b5.length); // fails for now + // Disabled because of Spacer nondeterminism. + //assert(b1.length == b5.length); // fails for now } } // ==== @@ -27,5 +28,5 @@ contract C { // ---- // Warning 2072: (364-379): Unused local variable. // Warning 2072: (650-665): Unused local variable. +// Warning 2072: (823-838): Unused local variable. // Warning 6328: (312-342): CHC: Assertion violation happens here. -// Warning 6328: (995-1025): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_no_arguments.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_no_arguments.sol index bdc95c9c6..b30842302 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_no_arguments.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_no_arguments.sol @@ -13,8 +13,10 @@ contract C { assert(res.length == 4); // should hold, but SMTChecker cannot know this yet } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (152-174): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (263-285): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (152-174): CHC: Assertion violation happens here. +// Warning 6328: (263-285): CHC: Assertion violation happens here. // Warning 6328: (339-362): CHC: Assertion violation happens here. // Warning 6328: (455-478): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/array_members/length_basic.sol b/test/libsolidity/smtCheckerTests/array_members/length_basic.sol index 5f958be46..9cbf1023b 100644 --- a/test/libsolidity/smtCheckerTests/array_members/length_basic.sol +++ b/test/libsolidity/smtCheckerTests/array_members/length_basic.sol @@ -10,4 +10,4 @@ contract C { } } // ---- -// Warning 6328: (153-176): CHC: Assertion violation happens here.\nCounterexample:\narr = []\n\nTransaction trace:\nC.constructor()\nState: arr = []\nC.f() +// Warning 6328: (153-176): CHC: Assertion violation happens here.\nCounterexample:\narr = []\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: arr = []\nC.f() diff --git a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol index 46406e8d3..6e40c3b07 100644 --- a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol +++ b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol @@ -26,7 +26,7 @@ contract C { } } // ---- -// Warning 6328: (352-378): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f() -// Warning 6328: (382-408): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f() -// Warning 6328: (412-435): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f() -// Warning 6328: (439-465): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f() +// Warning 6328: (352-378): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f() +// Warning 6328: (382-408): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f() +// Warning 6328: (412-435): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f() +// Warning 6328: (439-465): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f() diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_1d.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_1d.sol index c40b7f1e3..9214b530b 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_1d.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_1d.sol @@ -13,4 +13,4 @@ contract C { } } // ---- -// Warning 6328: (237-263): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f() +// Warning 6328: (237-263): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\nlength = 2\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f() diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_2d_1.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_2d_1.sol index 3cffe84b3..bf9cd63fc 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_2d_1.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_2d_1.sol @@ -16,4 +16,4 @@ contract C { } } // ---- -// Warning 6328: (317-343): CHC: Assertion violation happens here. +// Warning 6328: (317-343): CHC: Assertion violation happens here.\nCounterexample:\nb = [[0], [0]]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f() diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_bytes.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_bytes.sol index a0e994f81..486470669 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_bytes.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_bytes.sol @@ -13,4 +13,4 @@ contract C { } } // ---- -// Warning 6328: (236-277): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f() +// Warning 6328: (236-277): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\nlength = 2\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f() diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol index f7be61ed4..68b51d0c0 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol @@ -19,4 +19,4 @@ contract C { } // ---- -// Warning 6328: (298-343): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g() +// Warning 6328: (298-343): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\none = 1\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g() diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes_2d.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes_2d.sol index 30200b31a..cde51ab91 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes_2d.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes_2d.sol @@ -23,4 +23,4 @@ contract C { } } // ---- -// Warning 6328: (468-541): CHC: Assertion violation happens here.\nCounterexample:\nc = [[2]]\n\nTransaction trace:\nC.constructor()\nState: c = []\nC.g() +// Warning 6328: (468-541): CHC: Assertion violation happens here.\nCounterexample:\nc = [[2]]\nval = 2\n\nTransaction trace:\nC.constructor()\nState: c = []\nC.g() diff --git a/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol b/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol index 80e640a0d..7020350ef 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol @@ -10,6 +10,6 @@ contract C { } } // ---- -// Warning 6328: (122-148): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l() -// Warning 6328: (202-218): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l() -// Warning 6328: (222-278): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l() +// Warning 6328: (122-148): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\nlast = 0\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l() +// Warning 6328: (202-218): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\nlast = 1\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l() +// Warning 6328: (222-278): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\nlast = 1\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l() diff --git a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol index cf40a5285..4a4484449 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol @@ -13,6 +13,6 @@ contract C { } } // ---- -// Warning 6368: (221-225): CHC: Out of bounds access happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f() -// Warning 6368: (221-228): CHC: Out of bounds access happens here.\nCounterexample:\na = [[], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15]]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f() -// Warning 6328: (214-235): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f() +// Warning 6368: (221-225): CHC: Out of bounds access happens here.\nCounterexample:\na = []\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f() +// Warning 6368: (221-228): CHC: Out of bounds access happens here.\nCounterexample:\na = [[], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15]]\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f() +// Warning 6328: (214-235): CHC: Assertion violation happens here.\nCounterexample:\n\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f() diff --git a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol index 0130bcfac..06635c232 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol @@ -30,9 +30,9 @@ contract C { // Warning 6368: (271-278): CHC: Out of bounds access might happen here. // Warning 6368: (271-281): CHC: Out of bounds access might happen here. // Warning 6368: (344-348): CHC: Out of bounds access happens here. -// Warning 6368: (376-380): CHC: Out of bounds access happens here.\nCounterexample:\na = [], d = [5, 5, 5, 5, 5, 5, 5, 5, 7, 5, 9, 5, 11, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n\nTransaction trace:\nC.constructor()\nState: a = [], c = [[[0]]], d = [0, 0]\nC.f() -// Warning 6328: (369-393): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nState: a = [], c = [[[0]]], d = [0, 0]\nC.f() -// Warning 6368: (546-550): CHC: Out of bounds access happens here.\nCounterexample:\nc = []\n\nTransaction trace:\nC.constructor()\nState: a = [], c = [[[0]]], d = [0, 0]\nC.f() -// Warning 6368: (546-553): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nState: a = [], c = [[[0]]], d = [0, 0]\nC.f() +// Warning 6368: (376-380): CHC: Out of bounds access happens here. +// Warning 6328: (369-393): CHC: Assertion violation happens here. +// Warning 6368: (546-550): CHC: Out of bounds access happens here. +// Warning 6368: (546-553): CHC: Out of bounds access happens here. // Warning 6368: (546-556): CHC: Out of bounds access happens here. // Warning 6328: (539-563): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol b/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol index 4cd94ef6c..2ca716b21 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol @@ -9,5 +9,7 @@ contract C { assert(address(this).balance > 500); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (199-234): CHC: Assertion violation happens here.\nCounterexample:\n\na = 21238\n\nTransaction trace:\nC.constructor()\nC.f(21238) +// Warning 6328: (199-234): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol index c12ccaa2b..cb2bc8703 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol @@ -20,5 +20,7 @@ contract C { assert(x == 6); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (365-379): CHC: Assertion violation happens here.\nCounterexample:\nx = 7\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n C.f() -- internal call +// Warning 6328: (365-379): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol index 8aa3c3a46..f41bf2860 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol @@ -44,5 +44,5 @@ contract C { } // ---- // Warning 6328: (288-302): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.test()\n C.reset_if_overflow() -- internal call -// Warning 6328: (535-552): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(1)\nState: x = 1\nC.test()\n C.reset_if_overflow() -- internal call +// Warning 6328: (535-552): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\noldx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(1)\nState: x = 1\nC.test()\n C.reset_if_overflow() -- internal call // Warning 6328: (648-662): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(10)\nState: x = 10\nC.test()\n C.reset_if_overflow() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/revert_complex_flow.sol b/test/libsolidity/smtCheckerTests/control_flow/revert_complex_flow.sol index e31ac958e..0d619fed4 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/revert_complex_flow.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/revert_complex_flow.sol @@ -14,5 +14,5 @@ contract C { } } // ---- -// Warning 6328: (183-197): CHC: Assertion violation happens here.\nCounterexample:\n\nb = false\na = 0\n\nTransaction trace:\nC.constructor()\nC.f(false, 0) +// Warning 6328: (183-197): CHC: Assertion violation happens here.\nCounterexample:\n\nb = false\na = 0\nc = 2\n\nTransaction trace:\nC.constructor()\nC.f(false, 0) // Warning 6838: (155-156): BMC: Condition is always false. diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol index 5e8910a6e..cbb43330f 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol @@ -15,4 +15,4 @@ contract c { } } // ---- -// Warning 6328: (227-236): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call +// Warning 6328: (227-236): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n = false\nb = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol index 5acc7d5cd..17339f4df 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol @@ -17,5 +17,5 @@ contract c { } } // ---- -// Warning 6328: (202-218): CHC: Assertion violation happens here.\nCounterexample:\nx = 101\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call -// Warning 6328: (242-252): CHC: Assertion violation happens here.\nCounterexample:\nx = 101\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call +// Warning 6328: (202-218): CHC: Assertion violation happens here.\nCounterexample:\nx = 101\n = false\nb = true\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call +// Warning 6328: (242-252): CHC: Assertion violation happens here.\nCounterexample:\nx = 101\n = false\nb = true\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol index 079bdc945..d15467246 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol @@ -15,4 +15,4 @@ contract c { } } // ---- -// Warning 6328: (225-235): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call +// Warning 6328: (225-235): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n = false\nb = true\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol index 0126551f0..149b1ae21 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol @@ -15,4 +15,4 @@ contract c { } } // ---- -// Warning 6328: (225-235): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call +// Warning 6328: (225-235): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n = false\nb = true\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol index 471b35a1e..5d3fc7d4a 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol @@ -24,4 +24,4 @@ contract c { } } // ---- -// Warning 6328: (360-370): CHC: Assertion violation happens here.\nCounterexample:\nx = 102\na = false\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g(false)\n c.f() -- internal call\n c.f() -- internal call +// Warning 6328: (360-370): CHC: Assertion violation happens here.\nCounterexample:\nx = 102\na = false\n = false\nb = true\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g(false)\n c.f() -- internal call\n c.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol index b6572a31a..7a5c8f2bf 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol @@ -15,4 +15,4 @@ contract c { } } // ---- -// Warning 6328: (225-235): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call +// Warning 6328: (225-235): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n = false\nb = true\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_1.sol b/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_1.sol index c79ccffff..ec3dadeb0 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_1.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_1.sol @@ -9,4 +9,4 @@ contract C { } } // ---- -// Warning 6328: (159-173): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 11\n\nTransaction trace:\nC.constructor()\nC.f(11) +// Warning 6328: (159-173): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 11\na = 4\n\nTransaction trace:\nC.constructor()\nC.f(11) diff --git a/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_2.sol b/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_2.sol index 460efa7d5..d1ba5b7f2 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_2.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_2.sol @@ -9,4 +9,4 @@ contract C { } } // ---- -// Warning 6328: (159-173): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 11\n\nTransaction trace:\nC.constructor()\nC.f(11) +// Warning 6328: (159-173): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 11\na = 4\n\nTransaction trace:\nC.constructor()\nC.f(11) diff --git a/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_3.sol b/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_3.sol index 792e41cb2..660181057 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_3.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_3.sol @@ -9,4 +9,4 @@ contract C { } } // ---- -// Warning 6328: (161-175): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 11\n\nTransaction trace:\nC.constructor()\nC.f(11) +// Warning 6328: (161-175): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 11\na = 5\n\nTransaction trace:\nC.constructor()\nC.f(11) diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol index 4680ba5a9..62afe07bf 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol @@ -28,5 +28,7 @@ contract C { return y; } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (299-313): CHC: Assertion violation happens here.\nCounterexample:\nowner = 0, y = 0, s = 0\n\nTransaction trace:\nC.constructor()\nState: owner = 0, y = 0, s = 0\nC.f()\n s.f() -- untrusted external call, synthesized as:\n C.f() -- reentrant call\n s.f() -- untrusted external call +// Warning 6328: (299-313): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol new file mode 100644 index 000000000..cab2a0801 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol @@ -0,0 +1,43 @@ +pragma experimental SMTChecker; + +contract State { + uint x; + C c; + function f() public returns (uint) { + return c.g(); + } +} + +contract C { + address owner; + uint y; + uint z; + State s; + bool insidef; + + constructor() { + owner = msg.sender; + } + + function zz() public { + require(insidef); + z = 3; + } + + function f() public { + require(!insidef); + address prevOwner = owner; + insidef = true; + s.f(); + assert(z == y); + assert(prevOwner == owner); + insidef = false; + } + + function g() public view returns (uint) { + return y; + } +} +// ---- +// Warning 2018: (66-121): Function state mutability can be restricted to view +// Warning 6328: (400-414): CHC: Assertion violation happens here.\nCounterexample:\nowner = 0, y = 0, z = 3, s = 0, insidef = true\nprevOwner = 0\n\nTransaction trace:\nC.constructor()\nState: owner = 0, y = 0, z = 0, s = 0, insidef = false\nC.f()\n s.f() -- untrusted external call, synthesized as:\n C.zz() -- reentrant call diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_3.sol new file mode 100644 index 000000000..70e276ce1 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_3.sol @@ -0,0 +1,42 @@ +pragma experimental SMTChecker; + +contract State { + uint x; + C c; + function f() public view returns (uint) { + return c.g(); + } +} + +contract C { + address owner; + uint y; + uint z; + State s; + bool insidef; + + constructor() { + owner = msg.sender; + } + + function zz() public { + require(insidef); + z = 3; + } + + function f() public { + require(!insidef); + address prevOwner = owner; + insidef = true; + // s.f() cannot call zz() because it is `view` + // and zz modifies the state. + s.f(); + assert(z == y); + assert(prevOwner == owner); + insidef = false; + } + + function g() public view returns (uint) { + return y; + } +} diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_local_vars.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_local_vars.sol index 349849fea..8365757b7 100644 --- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_local_vars.sol +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_local_vars.sol @@ -32,4 +32,4 @@ contract A is B { } // ---- // Warning 5667: (296-302): Unused function parameter. Remove or comment out the variable name to silence this warning. -// Warning 6328: (357-372): CHC: Assertion violation happens here.\nCounterexample:\na = 4\nx = 0\n\nTransaction trace:\nA.constructor(0) +// Warning 6328: (357-372): CHC: Assertion violation happens here.\nCounterexample:\na = 4\nx = 0\na1 = 4\na2 = 5\n\nTransaction trace:\nA.constructor(0) diff --git a/test/libsolidity/smtCheckerTests/functions/functions_bound_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_bound_1_fail.sol index f8e32e6d8..474b04f00 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_bound_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_bound_1_fail.sol @@ -18,4 +18,4 @@ contract C } } // ---- -// Warning 6328: (261-277): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f(1)\n L.add(1, 999) -- internal call +// Warning 6328: (261-277): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\ny = 1000\n\nTransaction trace:\nC.constructor()\nC.f(1)\n L.add(1, 999) -- internal call diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol index b5abe65fe..a3ee609e6 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol @@ -12,4 +12,4 @@ contract C } // ---- -// Warning 6328: (161-174): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.h(0) -- internal call +// Warning 6328: (161-174): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g()\n C.h(0) -- internal call diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol index 8f405a748..248ef85eb 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol @@ -16,4 +16,4 @@ contract C } // ---- -// Warning 6328: (229-242): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.h(0) -- internal call\n C.k(0) -- internal call +// Warning 6328: (229-242): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g()\n C.h(0) -- internal call\n C.k(0) -- internal call diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol index 49da35b7b..6e20f8be9 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol @@ -12,4 +12,4 @@ contract C } // ---- -// Warning 6328: (163-176): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.h(0) -- internal call +// Warning 6328: (163-176): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g()\n C.h(0) -- internal call diff --git a/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol index d2e887342..4efa80ca3 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol @@ -17,4 +17,4 @@ contract C } } // ---- -// Warning 6328: (245-261): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f(1)\n L.add(1, 999) -- internal call +// Warning 6328: (245-261): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\ny = 1000\n\nTransaction trace:\nC.constructor()\nC.f(1)\n L.add(1, 999) -- internal call diff --git a/test/libsolidity/smtCheckerTests/functions/getters/address.sol b/test/libsolidity/smtCheckerTests/functions/getters/address.sol index e4b629144..c65e49943 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/address.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/address.sol @@ -14,5 +14,5 @@ contract C { } } // ---- -// Warning 6328: (204-230): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.f() -// Warning 6328: (282-308): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.f() +// Warning 6328: (204-230): 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: (282-308): 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() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol index 4beb29475..552640367 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol @@ -15,4 +15,4 @@ contract C { } } // ---- -// Warning 6328: (220-234): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0, 0, 0]\n\nTransaction trace:\nC.constructor()\nState: a = [0, 0, 0, 0]\nC.f() +// Warning 6328: (220-234): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0, 0, 0]\ny = 0\n\nTransaction trace:\nC.constructor()\nState: a = [0, 0, 0, 0]\nC.f() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_2.sol index bb13caf9f..b17afda3a 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_2.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_2.sol @@ -19,4 +19,4 @@ contract D { } } // ---- -// Warning 6328: (300-314): CHC: Assertion violation happens here.\nCounterexample:\nitems = [{x: 42, y: 43}]\n\nTransaction trace:\nD.constructor()\nState: items = []\nD.test() +// Warning 6328: (300-314): CHC: Assertion violation happens here.\nCounterexample:\nitems = [{x: 42, y: 43}]\na = 42\nb = 43\n\nTransaction trace:\nD.constructor()\nState: items = []\nD.test() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_3.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_3.sol index 70875edf8..f2be2c4a6 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_3.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_3.sol @@ -21,4 +21,4 @@ contract D { } } // ---- -// Warning 6328: (355-369): CHC: Assertion violation happens here.\nCounterexample:\nitems = [{x: 42, y: 43, arr: [0]}]\n\nTransaction trace:\nD.constructor()\nState: items = []\nD.test() +// Warning 6328: (355-369): CHC: Assertion violation happens here.\nCounterexample:\nitems = [{x: 42, y: 43, arr: [0]}]\ntmp = [0]\na = 42\nb = 43\n\nTransaction trace:\nD.constructor()\nState: items = []\nD.test() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/contract.sol b/test/libsolidity/smtCheckerTests/functions/getters/contract.sol index 60891b273..d050dfb1c 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/contract.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/contract.sol @@ -12,4 +12,4 @@ contract C { } } // ---- -// Warning 6328: (156-191): CHC: Assertion violation happens here.\nCounterexample:\nd = 0\n\nTransaction trace:\nC.constructor()\nState: d = 0\nC.f() +// Warning 6328: (156-191): CHC: Assertion violation happens here.\nCounterexample:\nd = 0\ne = 0\n\nTransaction trace:\nC.constructor()\nState: d = 0\nC.f() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/double_access.sol b/test/libsolidity/smtCheckerTests/functions/getters/double_access.sol index 5944e42de..4e7963cb5 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/double_access.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/double_access.sol @@ -16,4 +16,4 @@ contract C { } } // ---- -// Warning 6328: (226-240): CHC: Assertion violation happens here.\nCounterexample:\ns = {u: 0}\n\nTransaction trace:\nC.constructor()\nState: s = {u: 0}\nC.f() +// Warning 6328: (226-240): CHC: Assertion violation happens here.\nCounterexample:\ns = {u: 0}\nu = 0\nv = 0\n\nTransaction trace:\nC.constructor()\nState: s = {u: 0}\nC.f() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/enum.sol b/test/libsolidity/smtCheckerTests/functions/getters/enum.sol index 147d1c4fa..ab9896862 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/enum.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/enum.sol @@ -12,4 +12,4 @@ contract C { } } // ---- -// Warning 6328: (243-278): CHC: Assertion violation happens here.\nCounterexample:\nchoice = 0\n\nTransaction trace:\nC.constructor()\nState: choice = 0\nC.f() +// Warning 6328: (243-278): CHC: Assertion violation happens here.\nCounterexample:\nchoice = 0\ne = 0\n\nTransaction trace:\nC.constructor()\nState: choice = 0\nC.f() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/fixed_bytes.sol b/test/libsolidity/smtCheckerTests/functions/getters/fixed_bytes.sol index fab3b177a..df4c866d4 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 { } } // ---- -// Warning 6328: (192-208): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.f() -// Warning 6328: (260-278): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.f() +// Warning 6328: (192-208): 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: (260-278): 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() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/function.sol b/test/libsolidity/smtCheckerTests/functions/getters/function.sol index ce90d2666..d6253ab69 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/function.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/function.sol @@ -15,5 +15,5 @@ contract C { } } // ---- -// Warning 6328: (185-203): CHC: Assertion violation happens here.\nCounterexample:\ng = 0\n\nTransaction trace:\nC.constructor()\nState: g = 0\nC.f() -// Warning 6328: (295-311): CHC: Assertion violation happens here.\nCounterexample:\ng = 0\n\nTransaction trace:\nC.constructor()\nState: g = 0\nC.f() +// Warning 6328: (185-203): CHC: Assertion violation happens here.\nCounterexample:\ng = 0\ne = 0\n\nTransaction trace:\nC.constructor()\nState: g = 0\nC.f() +// Warning 6328: (295-311): CHC: Assertion violation happens here.\nCounterexample:\ng = 0\ne = 0\n\nTransaction trace:\nC.constructor()\nState: g = 0\nC.f() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/mapping_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/mapping_1.sol index 5f6344a39..1d372d2cf 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/mapping_1.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/mapping_1.sol @@ -10,4 +10,4 @@ contract C { } } // ---- -// Warning 6328: (175-189): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (175-189): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/mapping_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/mapping_2.sol index 0fa098f27..95b82181a 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/mapping_2.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/mapping_2.sol @@ -10,4 +10,4 @@ contract C { } } // ---- -// Warning 6328: (199-213): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (199-213): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/mapping_with_cast.sol b/test/libsolidity/smtCheckerTests/functions/getters/mapping_with_cast.sol index 57cdd8ba8..11d6ee611 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/mapping_with_cast.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/mapping_with_cast.sol @@ -10,4 +10,4 @@ contract C { } } // ---- -// Warning 6328: (180-194): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (180-194): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_1.sol index 2f4de2de6..a28db46af 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_1.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_1.sol @@ -16,4 +16,4 @@ contract C { } } // ---- -// Warning 6328: (243-257): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (243-257): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 42\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_7.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_7.sol index 0b68c9840..4ca1894d1 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_7.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_7.sol @@ -15,4 +15,4 @@ contract C { } } // ---- -// Warning 6328: (225-239): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (225-239): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 42\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_8.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_8.sol index c39b9a207..7185956b0 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_8.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_8.sol @@ -17,4 +17,4 @@ contract C { } } // ---- -// Warning 6328: (265-279): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (265-279): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 42\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_9.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_9.sol index 003a02772..8002639e0 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_9.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_9.sol @@ -15,4 +15,4 @@ contract C { } } // ---- -// Warning 6328: (251-265): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (251-265): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 42\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_1.sol index 5c623d941..910870cf0 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/struct_1.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/struct_1.sol @@ -26,4 +26,4 @@ contract C { } } // ---- -// Warning 6328: (370-387): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 0, t: {t: 0}, b: false, a: []}\n\nTransaction trace:\nC.constructor()\nState: s = {x: 0, t: {t: 0}, b: false, a: []}\nC.f() +// Warning 6328: (370-387): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 0, t: {t: 0}, b: false, a: []}\ny = 0\nc = false\nt = {t: 0}\n\nTransaction trace:\nC.constructor()\nState: s = {x: 0, t: {t: 0}, b: false, a: []}\nC.f() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_2.sol index 01e24edda..239aa206f 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/struct_2.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/struct_2.sol @@ -16,4 +16,4 @@ contract C { } } // ---- -// Warning 6328: (207-221): CHC: Assertion violation happens here.\nCounterexample:\ns = {a: [0, 0], u: 0}\n\nTransaction trace:\nC.constructor()\nState: s = {a: [0, 0], u: 0}\nC.f() +// Warning 6328: (207-221): CHC: Assertion violation happens here.\nCounterexample:\ns = {a: [0, 0], u: 0}\nu = 0\n\nTransaction trace:\nC.constructor()\nState: s = {a: [0, 0], u: 0}\nC.f() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_4.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_4.sol index 21dbbfafd..ac79475b4 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/struct_4.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/struct_4.sol @@ -19,4 +19,4 @@ contract C { } // ---- // Warning 2072: (179-216): Unused local variable. -// Warning 6328: (267-302): CHC: Assertion violation happens here.\nCounterexample:\ns = {d: 0, f: 0}\n\nTransaction trace:\nC.constructor()\nState: s = {d: 0, f: 0}\nC.test() +// Warning 6328: (267-302): CHC: Assertion violation happens here.\nCounterexample:\ns = {d: 0, f: 0}\nd = 0\nf = 0\n\nTransaction trace:\nC.constructor()\nState: s = {d: 0, f: 0}\nC.test() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_with_reassignment.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_with_reassignment.sol index e7c69f996..b14ec0212 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/struct_with_reassignment.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/struct_with_reassignment.sol @@ -28,5 +28,5 @@ contract C { } } // ---- -// Warning 6328: (288-305): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 1, b: false}\n\nTransaction trace:\nC.constructor()\nState: s = {x: 1, b: false}\nC.f() -// Warning 6328: (410-424): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 42, b: false}\n\nTransaction trace:\nC.constructor()\nState: s = {x: 1, b: false}\nC.f() +// Warning 6328: (288-305): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 1, b: false}\nx = 1\nb = false\ny = 0\nc = false\n\nTransaction trace:\nC.constructor()\nState: s = {x: 1, b: false}\nC.f() +// Warning 6328: (410-424): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 42, b: false}\nx = 1\nb = false\ny = 42\nc = false\n\nTransaction trace:\nC.constructor()\nState: s = {x: 1, b: false}\nC.f() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/uint.sol b/test/libsolidity/smtCheckerTests/functions/getters/uint.sol index 4fbe435c3..1643ab44d 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/uint.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/uint.sol @@ -10,4 +10,4 @@ contract C { } } // ---- -// Warning 6328: (147-161): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f() +// Warning 6328: (147-161): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f() diff --git a/test/libsolidity/smtCheckerTests/imports/import_library.sol b/test/libsolidity/smtCheckerTests/imports/import_library.sol index ddbc5b244..0649c02e1 100644 --- a/test/libsolidity/smtCheckerTests/imports/import_library.sol +++ b/test/libsolidity/smtCheckerTests/imports/import_library.sol @@ -15,4 +15,4 @@ library L { } } // ---- -// Warning 6328: (c:113-126): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n L.f() -- internal call +// Warning 6328: (c:113-126): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 1\n\nTransaction trace:\nC.constructor()\nC.g(0)\n L.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol index 23452fdf2..b68857c73 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol @@ -15,4 +15,4 @@ contract C is B { } } // ---- -// Warning 6328: (85-99): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 1\n\nTransaction trace:\nC.constructor()\nState: y = 0, x = 0\nC.g()\n B.f() -- internal call\nState: y = 0, x = 1\nB.f() +// Warning 6328: (85-99): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/fallback_receive.sol b/test/libsolidity/smtCheckerTests/inheritance/fallback_receive.sol index ddf0119b3..8daf3ad69 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/fallback_receive.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/fallback_receive.sol @@ -23,4 +23,4 @@ contract B is A { // ---- // Warning 6328: (114-128): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.fallback() // Warning 6328: (163-177): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.g() -// Warning 6328: (289-303): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 0\n\nTransaction trace:\nB.constructor()\nState: y = 0, x = 0\nB.receive(){ value: 21238 } +// Warning 6328: (289-303): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 0\n\nTransaction trace:\nB.constructor()\nState: y = 0, x = 0\nB.receive(){ value: 10450 } diff --git a/test/libsolidity/smtCheckerTests/inheritance/overriden_function_static_call_parent.sol b/test/libsolidity/smtCheckerTests/inheritance/overriden_function_static_call_parent.sol index 81f32a009..b2f129351 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/overriden_function_static_call_parent.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/overriden_function_static_call_parent.sol @@ -16,6 +16,8 @@ contract Child is Base { assert(x == d); // should fail } } +// ==== +// SMTIgnoreCex: yes // ---- // Warning 5667: (84-90): Unused function parameter. Remove or comment out the variable name to silence this warning. -// Warning 6328: (314-328): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\nc = 0\nd = 1\n\nTransaction trace:\nChild.constructor()\nState: x = 0\nChild.bInit(0, 1)\n BaseBase.init(0, 1) -- internal call +// Warning 6328: (314-328): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/receive.sol b/test/libsolidity/smtCheckerTests/inheritance/receive.sol index 9edbead72..e503e3bd0 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/receive.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/receive.sol @@ -21,6 +21,6 @@ contract B is A { } } // ---- -// Warning 6328: (128-142): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.receive(){ value: 21238 } +// Warning 6328: (128-142): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.receive() // Warning 6328: (177-191): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.g() -// Warning 6328: (300-314): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 0\n\nTransaction trace:\nB.constructor()\nState: y = 0, x = 0\nB.receive(){ value: 21238 } +// Warning 6328: (300-314): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 0\n\nTransaction trace:\nB.constructor()\nState: y = 0, x = 0\nB.receive() diff --git a/test/libsolidity/smtCheckerTests/inheritance/receive_fallback.sol b/test/libsolidity/smtCheckerTests/inheritance/receive_fallback.sol index ae0aa1fe9..c09b5d1ea 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 { } } // ---- -// Warning 6328: (120-134): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.receive(){ value: 21238 } +// Warning 6328: (120-134): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.receive() // Warning 6328: (169-183): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.g() // Warning 6328: (288-302): 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/inline_assembly/assembly_2.sol b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_2.sol index 60c4a7e0c..850331a52 100644 --- a/test/libsolidity/smtCheckerTests/inline_assembly/assembly_2.sol +++ b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_2.sol @@ -12,5 +12,5 @@ contract C { } // ---- // Warning 7737: (115-134): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). -// Warning 6328: (171-180): CHC: Assertion violation happens here.\nCounterexample:\n\n = false\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (171-180): CHC: Assertion violation happens here.\nCounterexample:\n\n = false\nb = false\nx = 42\n\nTransaction trace:\nC.constructor()\nC.f() // Warning 7737: (115-134): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). diff --git a/test/libsolidity/smtCheckerTests/inline_assembly/assembly_3.sol b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_3.sol index 37a616b67..528ac99e1 100644 --- a/test/libsolidity/smtCheckerTests/inline_assembly/assembly_3.sol +++ b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_3.sol @@ -12,5 +12,5 @@ contract C { } // ---- // Warning 7737: (139-158): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). -// Warning 6328: (236-245): CHC: Assertion violation happens here.\nCounterexample:\n\n = false\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (236-245): CHC: Assertion violation happens here.\nCounterexample:\n\n = false\nb = false\nc = true\n\nTransaction trace:\nC.constructor()\nC.f() // Warning 7737: (139-158): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). diff --git a/test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_access_inside_function.sol b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_access_inside_function.sol index 88cc84dd2..2b166adf3 100644 --- a/test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_access_inside_function.sol +++ b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_access_inside_function.sol @@ -19,6 +19,6 @@ contract C { } // ---- // Warning 7737: (116-182): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). -// Warning 6328: (185-200): CHC: Assertion violation happens here.\nCounterexample:\nz = 43\n\nTransaction trace:\nC.constructor()\nState: z = 0\nC.f() -// Warning 6328: (219-233): CHC: Assertion violation happens here.\nCounterexample:\nz = 0\n\nTransaction trace:\nC.constructor()\nState: z = 0\nC.f() +// Warning 6328: (185-200): CHC: Assertion violation happens here.\nCounterexample:\nz = 0\ni = 32\n\nTransaction trace:\nC.constructor()\nState: z = 0\nC.f() +// Warning 6328: (219-233): CHC: Assertion violation happens here.\nCounterexample:\nz = 43\ni = 32\n\nTransaction trace:\nC.constructor()\nState: z = 0\nC.f() // Warning 7737: (116-182): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). diff --git a/test/libsolidity/smtCheckerTests/inline_assembly/assembly_memory_write.sol b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_memory_write.sol index 8467b5084..cb900efa0 100644 --- a/test/libsolidity/smtCheckerTests/inline_assembly/assembly_memory_write.sol +++ b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_memory_write.sol @@ -21,8 +21,10 @@ contract C { assert(i == 7); // should hold, not changed by the assembly } } +// ==== +// SMTIgnoreCex: yes // ---- // Warning 7737: (189-220): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). -// Warning 6328: (223-241): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 42}\n\nTransaction trace:\nC.constructor()\nState: s = {x: 0}\nC.f() -// Warning 6328: (260-277): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 42}\n\nTransaction trace:\nC.constructor()\nState: s = {x: 0}\nC.f() +// Warning 6328: (223-241): CHC: Assertion violation happens here. +// Warning 6328: (260-277): CHC: Assertion violation happens here. // Warning 7737: (189-220): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_break_2_fail.sol b/test/libsolidity/smtCheckerTests/loops/do_while_break_2_fail.sol index 23ebf8daa..37763c0a7 100644 --- a/test/libsolidity/smtCheckerTests/loops/do_while_break_2_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/do_while_break_2_fail.sol @@ -19,4 +19,4 @@ contract C { // ---- // Warning 5740: (128-133): Unreachable code. // Warning 5740: (147-151): Unreachable code. -// Warning 6328: (180-194): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (180-194): CHC: Assertion violation happens here.\nCounterexample:\n\na = 1\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_break_fail.sol b/test/libsolidity/smtCheckerTests/loops/do_while_break_fail.sol index 00d137500..3f91ea19f 100644 --- a/test/libsolidity/smtCheckerTests/loops/do_while_break_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/do_while_break_fail.sol @@ -15,4 +15,4 @@ contract C { // ---- // Warning 5740: (104-109): Unreachable code. // Warning 5740: (122-128): Unreachable code. -// Warning 6328: (133-147): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (133-147): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_4.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_4.sol index da0e54054..a7aaa5b33 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_4.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_4.sol @@ -9,4 +9,4 @@ contract C { // ==== // SMTSolvers: z3 // ---- -// Warning 6328: (136-150): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f(0) +// Warning 6328: (136-150): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 3\n\nTransaction trace:\nC.constructor()\nC.f(0) diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol index 0e84f5375..ac8e1064b 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol @@ -11,4 +11,4 @@ contract C { // ==== // SMTSolvers: z3 // ---- -// Warning 6328: (167-181): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 10\n\nTransaction trace:\nC.constructor()\nC.f(10) +// Warning 6328: (167-181): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 10\ny = 2\n\nTransaction trace:\nC.constructor()\nC.f(10) diff --git a/test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol index b4d17d235..e1a83a62a 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol @@ -13,6 +13,7 @@ contract C } // ==== // SMTSolvers: z3 +// SMTIgnoreCex: yes // ---- // Warning 5740: (120-123): Unreachable code. -// Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\n\nTransaction trace:\nC.constructor()\nC.f(3) +// Warning 6328: (131-145): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol index f3d4984a8..6316a87d3 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol @@ -8,12 +8,15 @@ contract LoopFor2 { b[0] = 900; uint[] memory a = b; uint i; + // Disabled because of Spacer's nondeterminism. + /* while (i < n) { // Accesses are safe but oob is reported due to potential aliasing after c's assignment. b[i] = i + 1; c[i] = b[i]; ++i; } + */ // Removed because current Spacer seg faults in cex generation. //assert(b[0] == c[0]); // Removed because current Spacer seg faults in cex generation. @@ -27,6 +30,4 @@ contract LoopFor2 { // SMTSolvers: z3 // ---- // Warning 2072: (235-250): Unused local variable. -// Warning 6368: (379-383): CHC: Out of bounds access happens here. -// Warning 6368: (403-407): CHC: Out of bounds access happens here. -// Warning 6368: (396-400): CHC: Out of bounds access happens here. +// Warning 2072: (258-264): Unused local variable. diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol index aef020449..5fa667a86 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol @@ -28,6 +28,6 @@ contract LoopFor2 { // Warning 6368: (321-325): CHC: Out of bounds access might happen here. // Warning 6368: (345-349): CHC: Out of bounds access might happen here. // Warning 6368: (338-342): CHC: Out of bounds access might happen here. -// Warning 6368: (444-448): CHC: Out of bounds access happens here.\nCounterexample:\nb = [1, 0], c = [1, 0]\nn = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1) -// Warning 6328: (437-456): CHC: Assertion violation happens here.\nCounterexample:\nb = [1, 0], c = [1, 0]\nn = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1) -// Warning 6328: (460-479): CHC: Assertion violation happens here.\nCounterexample:\nb = [1, 0], c = [1, 0]\nn = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1) +// Warning 6368: (444-448): CHC: Out of bounds access happens here.\nCounterexample:\nb = [1, 0], c = [1, 0]\nn = 1\na = []\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1) +// Warning 6328: (437-456): CHC: Assertion violation happens here.\nCounterexample:\nb = [1, 0], c = [1, 0]\nn = 1\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1) +// Warning 6328: (460-479): CHC: Assertion violation happens here.\nCounterexample:\nb = [1, 0], c = [1, 0]\nn = 1\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1) diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol index 80d48e45e..03f7464f5 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol @@ -9,5 +9,6 @@ contract C { } // ==== // SMTSolvers: z3 +// SMTIgnoreCex: yes // ---- -// Warning 6328: (187-201): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\n\nTransaction trace:\nC.constructor()\nC.f(3) +// Warning 6328: (187-201): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/math/addmod_1.sol b/test/libsolidity/smtCheckerTests/math/addmod_1.sol index 1cf35547b..5f4eb14b4 100644 --- a/test/libsolidity/smtCheckerTests/math/addmod_1.sol +++ b/test/libsolidity/smtCheckerTests/math/addmod_1.sol @@ -12,6 +12,6 @@ contract C { } } // ---- -// Warning 4281: (141-166): CHC: Division by zero happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (170-184): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 4281: (141-166): CHC: Division by zero happens here.\nCounterexample:\n\ny = 0\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (170-184): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 0\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f() // Warning 4281: (263-278): CHC: Division by zero happens here.\nCounterexample:\n\nx = 0\ny = 0\nk = 0\n = 0\n\nTransaction trace:\nC.constructor()\nC.g(0, 0, 0) diff --git a/test/libsolidity/smtCheckerTests/math/addmod_mulmod_zero.sol b/test/libsolidity/smtCheckerTests/math/addmod_mulmod_zero.sol index 37308ef0c..fb3df8b80 100644 --- a/test/libsolidity/smtCheckerTests/math/addmod_mulmod_zero.sol +++ b/test/libsolidity/smtCheckerTests/math/addmod_mulmod_zero.sol @@ -22,7 +22,7 @@ contract C { } // ---- // Warning 6321: (253-260): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. -// Warning 4281: (94-109): CHC: Division by zero happens here.\nCounterexample:\n\nd = 0\n\nTransaction trace:\nC.constructor()\nC.f(0) -// Warning 6328: (113-126): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0\n\nTransaction trace:\nC.constructor()\nC.f(0) -// Warning 4281: (180-195): CHC: Division by zero happens here.\nCounterexample:\n\nd = 0\n\nTransaction trace:\nC.constructor()\nC.g(0) -// Warning 6328: (199-212): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0\n\nTransaction trace:\nC.constructor()\nC.g(0) +// Warning 4281: (94-109): CHC: Division by zero happens here.\nCounterexample:\n\nd = 0\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f(0) +// Warning 6328: (113-126): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f(0) +// Warning 4281: (180-195): CHC: Division by zero happens here.\nCounterexample:\n\nd = 0\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g(0) +// Warning 6328: (199-212): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g(0) diff --git a/test/libsolidity/smtCheckerTests/math/mulmod_1.sol b/test/libsolidity/smtCheckerTests/math/mulmod_1.sol index 5d9931c41..a42919a8d 100644 --- a/test/libsolidity/smtCheckerTests/math/mulmod_1.sol +++ b/test/libsolidity/smtCheckerTests/math/mulmod_1.sol @@ -12,6 +12,6 @@ contract C { } } // ---- -// Warning 4281: (141-166): CHC: Division by zero happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (170-184): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 4281: (141-166): CHC: Division by zero happens here.\nCounterexample:\n\ny = 0\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (170-184): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 0\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f() // Warning 4281: (263-278): CHC: Division by zero happens here.\nCounterexample:\n\nx = 0\ny = 0\nk = 0\n = 0\n\nTransaction trace:\nC.constructor()\nC.g(0, 0, 0) diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions.sol index e4ee540d8..c998261bb 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions.sol @@ -22,4 +22,4 @@ contract C } } // ---- -// Warning 6328: (311-324): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f(1)\n C.g(1, 0) -- internal call +// Warning 6328: (311-324): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\na = 1\nb = 0\n\nTransaction trace:\nC.constructor()\nC.f(1)\n C.g(1, 0) -- internal call diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_parameters.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_parameters.sol index 5dc13bfb2..8149a9ec9 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_parameters.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_parameters.sol @@ -13,4 +13,4 @@ contract C } } // ---- -// Warning 6328: (164-177): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f(1) +// Warning 6328: (164-177): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\na = 1\nb = 0\n\nTransaction trace:\nC.constructor()\nC.f(1) diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_1.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_1.sol index 6c5b88f4b..ff9286c0a 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_1.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_1.sol @@ -20,4 +20,4 @@ contract B is A { } } // ---- -// Warning 6328: (242-256): CHC: Assertion violation happens here.\nCounterexample:\ns = 42\n\nTransaction trace:\nB.constructor()\nState: s = 0\nB.set(42)\nState: s = 42\nA.f() +// Warning 6328: (242-256): CHC: Assertion violation happens here.\nCounterexample:\ns = 42\nx = 42\n\nTransaction trace:\nB.constructor()\nState: s = 0\nB.set(42)\nState: s = 42\nA.f() diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_3.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_3.sol index c69fee5ba..4398f0ae3 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_3.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_3.sol @@ -19,4 +19,4 @@ contract B is A { } // ---- // Warning 5740: (95-156): Unreachable code. -// Warning 6328: (127-137): CHC: Assertion violation happens here.\nCounterexample:\ns = true\n\nTransaction trace:\nB.constructor()\nState: s = false\nA.f() +// Warning 6328: (127-137): CHC: Assertion violation happens here.\nCounterexample:\ns = true\nx = true\n\nTransaction trace:\nB.constructor()\nState: s = false\nA.f() diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_parameter_copy.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_parameter_copy.sol index 526d97918..7502273a9 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_parameter_copy.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_parameter_copy.sol @@ -12,4 +12,4 @@ contract C } } // ---- -// Warning 6328: (128-142): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f(0) +// Warning 6328: (128-142): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f(0) diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_same_local_variables.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_same_local_variables.sol index fbc67b6cc..7142acba3 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_same_local_variables.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_same_local_variables.sol @@ -12,4 +12,4 @@ contract C } } // ---- -// Warning 6328: (121-135): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f(0) +// Warning 6328: (121-135): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\nx = 2\n\nTransaction trace:\nC.constructor()\nC.f(3) diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array_3.sol b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array_3.sol index 3f52d7c4e..61fba7c7b 100644 --- a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array_3.sol +++ b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array_3.sol @@ -25,7 +25,7 @@ contract A { } } // ---- -// Warning 6368: (350-354): CHC: Out of bounds access happens here.\nCounterexample:\na = [0, 0]\n\nTransaction trace:\nA.constructor()\nState: a = [1]\nA.f() -// Warning 6328: (343-360): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0]\n\nTransaction trace:\nA.constructor()\nState: a = [1]\nA.f() -// Warning 6368: (454-458): CHC: Out of bounds access happens here.\nCounterexample:\na = [0, 0]\n\nTransaction trace:\nA.constructor()\nState: a = [1]\nA.f() -// Warning 6328: (447-464): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0]\n\nTransaction trace:\nA.constructor()\nState: a = [1]\nA.f() +// Warning 6368: (350-354): CHC: Out of bounds access happens here.\nCounterexample:\na = [0, 0]\nu = []\nb = [0, 0]\n\nTransaction trace:\nA.constructor()\nState: a = [1]\nA.f() +// Warning 6328: (343-360): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0]\nb = [0, 0]\n\nTransaction trace:\nA.constructor()\nState: a = [1]\nA.f() +// Warning 6368: (454-458): CHC: Out of bounds access happens here.\nCounterexample:\na = [0, 0]\nu = []\nb = [0, 0]\n\nTransaction trace:\nA.constructor()\nState: a = [1]\nA.f() +// Warning 6328: (447-464): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0]\nb = [0, 0]\n\nTransaction trace:\nA.constructor()\nState: a = [1]\nA.f() diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_and_int.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_and_int.sol index 710e95da0..ca870a1ec 100644 --- a/test/libsolidity/smtCheckerTests/operators/bitwise_and_int.sol +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_and_int.sol @@ -15,4 +15,4 @@ contract C { } } // ---- -// Warning 6328: (104-122): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (104-122): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\ny = 0\nz = 0\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_and_uint.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_and_uint.sol index 06d9c96ae..86ab29a16 100644 --- a/test/libsolidity/smtCheckerTests/operators/bitwise_and_uint.sol +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_and_uint.sol @@ -13,6 +13,6 @@ contract C { } } // ---- -// Warning 6328: (107-125): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (180-203): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (207-230): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (107-125): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (180-203): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 255\ny = 65535\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (207-230): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 255\ny = 65535\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol index 8aa35fa81..dcb64d999 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 { } } // ---- -// Warning 6328: (133-156): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (133-156): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 65535\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_not_int.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_not_int.sol index f7dfad12d..e95eee8e6 100644 --- a/test/libsolidity/smtCheckerTests/operators/bitwise_not_int.sol +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_not_int.sol @@ -15,7 +15,7 @@ contract C { } } // ---- -// Warning 6328: (91-106): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (122-137): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (153-171): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (185-200): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (91-106): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (122-137): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 255\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (153-171): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 15\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (185-200): CHC: Assertion violation happens here.\nCounterexample:\n\nx = (- 1)\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_not_uint.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_not_uint.sol index ef31ecbdb..a27b26f9b 100644 --- a/test/libsolidity/smtCheckerTests/operators/bitwise_not_uint.sol +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_not_uint.sol @@ -11,5 +11,5 @@ contract C { } } // ---- -// Warning 6328: (159-179): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (183-203): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (159-179): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 255\ny = 65280\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (183-203): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 255\ny = 65280\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 9481b0979..1ca17f25f 100644 --- a/test/libsolidity/smtCheckerTests/operators/bitwise_or_fixed_bytes.sol +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_or_fixed_bytes.sol @@ -8,4 +8,4 @@ contract C { } } // ---- -// Warning 6328: (182-207): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (182-207): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0\nb = 255\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_or_int.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_or_int.sol index 01a58e36b..94eb7c869 100644 --- a/test/libsolidity/smtCheckerTests/operators/bitwise_or_int.sol +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_or_int.sol @@ -17,5 +17,5 @@ contract C { } } // ---- -// Warning 6328: (144-162): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (267-286): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (144-162): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 0\nz = 0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (267-286): CHC: Assertion violation happens here.\nCounterexample:\n\nx = (- 1)\ny = 200\nz = 255\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_or_uint.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_or_uint.sol index 765679b36..ec09770dc 100644 --- a/test/libsolidity/smtCheckerTests/operators/bitwise_or_uint.sol +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_or_uint.sol @@ -13,5 +13,5 @@ contract C { } } // ---- -// Warning 6328: (155-176): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (207-230): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (155-176): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 255\ny = 65280\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (207-230): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 255\ny = 65280\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_rational_2.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_rational_2.sol index f1e40ff9a..c289f494f 100644 --- a/test/libsolidity/smtCheckerTests/operators/bitwise_rational_2.sol +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_rational_2.sol @@ -12,4 +12,4 @@ contract C { } } // ---- -// Warning 6328: (181-194): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (181-194): CHC: Assertion violation happens here.\nCounterexample:\n\nx = (- 2)\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_xor_int.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_xor_int.sol index cbccabcad..5adbd7095 100644 --- a/test/libsolidity/smtCheckerTests/operators/bitwise_xor_int.sol +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_xor_int.sol @@ -15,5 +15,5 @@ contract C { } } // ---- -// Warning 6328: (189-206): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (247-264): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (189-206): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\ny = 0\nz = (- 1)\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (247-264): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 7\ny = 3\nz = (- 1)\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_xor_uint.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_xor_uint.sol index ed4ddc87a..25414a97d 100644 --- a/test/libsolidity/smtCheckerTests/operators/bitwise_xor_uint.sol +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_xor_uint.sol @@ -13,5 +13,5 @@ contract C { } } // ---- -// Warning 6328: (155-176): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (207-230): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (155-176): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 255\ny = 65280\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (207-230): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 255\ny = 65280\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 5f0e3cd06..ccc27a0ac 100644 --- a/test/libsolidity/smtCheckerTests/operators/bytes_new.sol +++ b/test/libsolidity/smtCheckerTests/operators/bytes_new.sol @@ -34,5 +34,5 @@ contract C { } } // ---- -// Warning 6368: (501-505): CHC: Out of bounds access happens here. -// Warning 6368: (523-527): CHC: Out of bounds access happens here. +// Warning 6368: (501-505): CHC: Out of bounds access happens here.\nCounterexample:\n\nx = [18, 52, 0]\n\nTransaction trace:\nC.constructor()\nC.h() +// Warning 6368: (523-527): CHC: Out of bounds access happens here.\nCounterexample:\n\nx = [18, 52, 0]\n\nTransaction trace:\nC.constructor()\nC.h() diff --git a/test/libsolidity/smtCheckerTests/operators/compound_add.sol b/test/libsolidity/smtCheckerTests/operators/compound_add.sol index 406fa256e..377849b54 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_add.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_add.sol @@ -11,4 +11,4 @@ contract C } } // ---- -// Warning 6328: (151-166): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f(0) +// Warning 6328: (151-166): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 200\n\nTransaction trace:\nC.constructor()\nC.f(0) diff --git a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_1.sol index 35f8ffc7b..e91e0b840 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_1.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_1.sol @@ -9,4 +9,4 @@ contract C { } } // ---- -// Warning 6328: (147-161): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\n\nTransaction trace:\nC.constructor()\nC.f(2) +// Warning 6328: (147-161): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\ny = 2\n\nTransaction trace:\nC.constructor()\nC.f(2) 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 7764ec484..10f0a574b 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_fixed_bytes.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_fixed_bytes.sol @@ -12,4 +12,4 @@ contract C { } // ---- // Warning 6321: (83-89): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. -// Warning 6328: (209-223): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (209-223): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0\na = 0\nb = 240\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_int.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_int.sol index 32b2f05d2..a2638b806 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_int.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_int.sol @@ -18,4 +18,4 @@ contract C { } } // ---- -// Warning 6328: (114-128): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (114-128): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_uint.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_uint.sol index 990937fa7..06aab80c0 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_uint.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_uint.sol @@ -28,6 +28,6 @@ contract C { } } // ---- -// Warning 6328: (177-191): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (380-399): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (506-523): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (177-191): CHC: Assertion violation happens here.\nCounterexample:\n\nv = 3\nc = 0\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (380-399): CHC: Assertion violation happens here.\nCounterexample:\n\nv = 3\nc = 0\nx = 255\ny = 255\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (506-523): CHC: Assertion violation happens here.\nCounterexample:\n\nv = 3\nc = 0\nx = 255\ny = 65535\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 e1e24c206..eac0b393e 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_fixed_bytes.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_fixed_bytes.sol @@ -12,4 +12,4 @@ contract C { } // ---- // Warning 6321: (83-89): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. -// Warning 6328: (209-223): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (209-223): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0\na = 255\nb = 255\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int.sol index 628d9de9b..7a8d33575 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int.sol @@ -18,4 +18,4 @@ contract C { } } // ---- -// Warning 6328: (114-128): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (114-128): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint.sol index 3994dccfa..d7d9308ce 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint.sol @@ -24,6 +24,6 @@ contract C { } } // ---- -// Warning 6328: (121-135): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (298-315): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (424-443): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (121-135): CHC: Assertion violation happens here.\nCounterexample:\n\nv = 7\nc = 0\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (298-315): CHC: Assertion violation happens here.\nCounterexample:\n\nv = 7\nc = 7\nx = 255\ny = 65535\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (424-443): CHC: Assertion violation happens here.\nCounterexample:\n\nv = 7\nc = 7\nx = 65280\ny = 61951\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 c676d4af7..855fb3952 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 { } } // ---- -// Warning 6328: (180-198): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (180-198): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 6579559\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 c2d71b95a..2d0b48412 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 { } } // ---- -// Warning 6328: (262-309): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (427-470): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (262-309): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 43595849750559157961410616371195012376776328331498503227444818324475146035296\nz = 43595849750559157961410616371195012376776328331498503227444818324475146035296\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (427-470): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 44959890247538927454655645290332771782915717053340361485195502024921998844258\nz = 44959890247538927454655645290332771782915717053340361485195502024921998844258\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 47f58cbf0..7b5b6d171 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_fixed_bytes.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_fixed_bytes.sol @@ -12,4 +12,4 @@ contract C { } // ---- // Warning 6321: (83-89): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. -// Warning 6328: (210-227): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (210-227): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0\na = 255\nb = 240\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_int.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_int.sol index 099112017..148d84065 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_int.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_int.sol @@ -15,4 +15,4 @@ contract C { } } // ---- -// Warning 6328: (114-128): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (114-128): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_uint.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_uint.sol index feb5e8bdf..a665a8e7b 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_uint.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_uint.sol @@ -24,6 +24,6 @@ contract C { } } // ---- -// Warning 6328: (121-135): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (298-315): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (422-441): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (121-135): CHC: Assertion violation happens here.\nCounterexample:\n\nv = 4\nc = 0\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (298-315): CHC: Assertion violation happens here.\nCounterexample:\n\nv = 4\nc = 4\nx = 255\ny = 65280\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (422-441): CHC: Assertion violation happens here.\nCounterexample:\n\nv = 4\nc = 4\nx = 65280\ny = 65280\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/compound_mul.sol b/test/libsolidity/smtCheckerTests/operators/compound_mul.sol index 5617a2fc0..edf7a565b 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_mul.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_mul.sol @@ -11,4 +11,4 @@ contract C } } // ---- -// Warning 6328: (150-164): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f(0) +// Warning 6328: (150-164): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 100\n\nTransaction trace:\nC.constructor()\nC.f(0) diff --git a/test/libsolidity/smtCheckerTests/operators/compound_sub.sol b/test/libsolidity/smtCheckerTests/operators/compound_sub.sol index 79f6c38ab..ac625fce0 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_sub.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_sub.sol @@ -11,4 +11,4 @@ contract C } } // ---- -// Warning 6328: (150-164): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 90\n\nTransaction trace:\nC.constructor()\nC.f(90) +// Warning 6328: (150-164): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 90\ny = 90\n\nTransaction trace:\nC.constructor()\nC.f(90) diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_1.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_1.sol index feac721ab..c2be2e47c 100644 --- a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_1.sol +++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_1.sol @@ -7,4 +7,4 @@ contract C { } } // ---- -// Warning 6328: (104-117): CHC: Assertion violation happens here.\nCounterexample:\n\nb = true\n\nTransaction trace:\nC.constructor()\nC.f(true) +// Warning 6328: (104-117): CHC: Assertion violation happens here.\nCounterexample:\n\nb = true\na = 2\n\nTransaction trace:\nC.constructor()\nC.f(true) diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_2.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_2.sol index 54fe7b0df..7a9c56c2d 100644 --- a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_2.sol +++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_2.sol @@ -7,5 +7,7 @@ contract C { assert(c == 0); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (132-146): CHC: Assertion violation happens here.\nCounterexample:\n\nb = 1\n\nTransaction trace:\nC.constructor()\nC.f(0) +// Warning 6328: (132-146): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_always_true.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_always_true.sol index 3f260a366..dfdc200da 100644 --- a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_always_true.sol +++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_always_true.sol @@ -8,5 +8,5 @@ contract C { } } // ---- -// Warning 6328: (118-131): CHC: Assertion violation happens here.\nCounterexample:\n\nb = true\n\nTransaction trace:\nC.constructor()\nC.f(true) +// Warning 6328: (118-131): CHC: Assertion violation happens here.\nCounterexample:\n\nb = true\nc = 5\n\nTransaction trace:\nC.constructor()\nC.f(true) // Warning 6838: (105-106): BMC: Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_function_1.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_function_1.sol index e37f001ad..12b915080 100644 --- a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_function_1.sol +++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_function_1.sol @@ -10,4 +10,4 @@ contract C { } } // ---- -// Warning 6328: (203-216): CHC: Assertion violation happens here.\nCounterexample:\n\na = 6\n\nTransaction trace:\nC.constructor()\nC.g(6)\n C.f(6) -- internal call +// Warning 6328: (203-216): CHC: Assertion violation happens here.\nCounterexample:\n\na = 6\nc = 3\n\nTransaction trace:\nC.constructor()\nC.g(6)\n C.f(6) -- internal call diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_nested_unsafe.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_nested_unsafe.sol index 0bac40ed8..00cf0d9af 100644 --- a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_nested_unsafe.sol +++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_nested_unsafe.sol @@ -7,4 +7,4 @@ contract C { } } // ---- -// Warning 6328: (141-154): CHC: Assertion violation happens here.\nCounterexample:\n\nb1 = false\nb2 = false\n\nTransaction trace:\nC.constructor()\nC.f(false, false) +// Warning 6328: (141-154): CHC: Assertion violation happens here.\nCounterexample:\n\nb1 = false\nb2 = false\nc = 1\n\nTransaction trace:\nC.constructor()\nC.f(false, false) diff --git a/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol b/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol index 7b5960a15..ad9540acf 100644 --- a/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol +++ b/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol @@ -17,7 +17,6 @@ contract C } function f(bool b) public { a[1][1] = 512; - a[2][1] = 4; if (b) delete a; else @@ -32,13 +31,11 @@ contract C // ---- // Warning 6368: (247-251): CHC: Out of bounds access might happen here. // Warning 6368: (247-254): CHC: Out of bounds access might happen here. -// Warning 6368: (264-268): CHC: Out of bounds access might happen here. -// Warning 6368: (264-271): CHC: Out of bounds access might happen here. -// Warning 6368: (316-320): CHC: Out of bounds access might happen here. -// Warning 6368: (341-345): CHC: Out of bounds access might happen here. -// Warning 6368: (341-348): CHC: Out of bounds access might happen here. -// Warning 6328: (334-354): CHC: Assertion violation might happen here. -// Warning 6368: (365-369): CHC: Out of bounds access might happen here. -// Warning 6368: (365-372): CHC: Out of bounds access might happen here. -// Warning 6328: (358-378): CHC: Assertion violation might happen here. -// Warning 4661: (358-378): BMC: Assertion violation happens here. +// Warning 6368: (301-305): CHC: Out of bounds access might happen here. +// Warning 6368: (326-330): CHC: Out of bounds access might happen here. +// Warning 6368: (326-333): CHC: Out of bounds access might happen here. +// Warning 6328: (319-339): CHC: Assertion violation might happen here. +// Warning 6368: (350-354): CHC: Out of bounds access might happen here. +// Warning 6368: (350-357): CHC: Out of bounds access might happen here. +// Warning 6328: (343-363): CHC: Assertion violation might happen here. +// Warning 4661: (343-363): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/delete_array_push.sol b/test/libsolidity/smtCheckerTests/operators/delete_array_push.sol index b1f55540f..ce3813345 100644 --- a/test/libsolidity/smtCheckerTests/operators/delete_array_push.sol +++ b/test/libsolidity/smtCheckerTests/operators/delete_array_push.sol @@ -15,5 +15,5 @@ contract C { } } // ---- -// Warning 6328: (175-222): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[]]\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.s() -// Warning 6328: (395-440): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[], [0]]\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.s() +// Warning 6328: (175-222): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[]]\nlength = 0\nlength2 = 0\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.s() +// Warning 6328: (395-440): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[], [0]]\nlength = 2\nlength2 = 1\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.s() diff --git a/test/libsolidity/smtCheckerTests/operators/division_6.sol b/test/libsolidity/smtCheckerTests/operators/division_6.sol index 41db7f320..c129a0c60 100644 --- a/test/libsolidity/smtCheckerTests/operators/division_6.sol +++ b/test/libsolidity/smtCheckerTests/operators/division_6.sol @@ -10,5 +10,5 @@ contract C { } } // ---- -// Warning 4984: (152-157): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\n\na = 128\nb = 2\n = 0\n\nTransaction trace:\nC.constructor()\nC.mul(128, 2) +// Warning 4984: (152-157): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\n\na = 128\nb = 2\n = 0\nc = 0\n\nTransaction trace:\nC.constructor()\nC.mul(128, 2) // Warning 6838: (169-179): BMC: Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/operators/function_call_named_arguments.sol b/test/libsolidity/smtCheckerTests/operators/function_call_named_arguments.sol index a223845e7..f26ef0238 100644 --- a/test/libsolidity/smtCheckerTests/operators/function_call_named_arguments.sol +++ b/test/libsolidity/smtCheckerTests/operators/function_call_named_arguments.sol @@ -29,4 +29,4 @@ contract C { } } // ---- -// Warning 6328: (507-521): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.call()\n L.l(2, 3) -- internal call\n L.l(3, 3) -- internal call\n C.f(1, 2, true) -- internal call\n C.f(1, 2, false) -- internal call +// Warning 6328: (507-521): CHC: Assertion violation happens here.\nCounterexample:\n\na = 2\nb = 2\n\nTransaction trace:\nC.constructor()\nC.call()\n L.l(2, 3) -- internal call\n L.l(3, 3) -- internal call\n C.f(1, 2, true) -- internal call\n C.f(1, 2, false) -- internal call diff --git a/test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol b/test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol index 0f97262f6..849da3173 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 { } } // ---- -// Warning 6328: (185-206): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (185-206): CHC: Assertion violation happens here.\nCounterexample:\n\nx = [0, 17, 34, 51]\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/integer_new.sol b/test/libsolidity/smtCheckerTests/operators/integer_new.sol index 612d33e63..e68e39dcf 100644 --- a/test/libsolidity/smtCheckerTests/operators/integer_new.sol +++ b/test/libsolidity/smtCheckerTests/operators/integer_new.sol @@ -34,5 +34,5 @@ contract C { } } // ---- -// Warning 6368: (507-511): CHC: Out of bounds access happens here. -// Warning 6368: (529-533): CHC: Out of bounds access happens here. +// Warning 6368: (507-511): CHC: Out of bounds access happens here.\nCounterexample:\n\nx = [18, 52, 0]\n\nTransaction trace:\nC.constructor()\nC.h() +// Warning 6368: (529-533): CHC: Out of bounds access happens here.\nCounterexample:\n\nx = [18, 52, 0]\n\nTransaction trace:\nC.constructor()\nC.h() diff --git a/test/libsolidity/smtCheckerTests/operators/shifts/shift_left_larger_type.sol b/test/libsolidity/smtCheckerTests/operators/shifts/shift_left_larger_type.sol index 4f93d8765..998efd6bf 100644 --- a/test/libsolidity/smtCheckerTests/operators/shifts/shift_left_larger_type.sol +++ b/test/libsolidity/smtCheckerTests/operators/shifts/shift_left_larger_type.sol @@ -11,4 +11,4 @@ contract C { } } // ---- -// Warning 6328: (171-191): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (171-191): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0\nx = 254\ny = 1\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/unary_add.sol b/test/libsolidity/smtCheckerTests/operators/unary_add.sol index e1a9581a2..3ea8d5566 100644 --- a/test/libsolidity/smtCheckerTests/operators/unary_add.sol +++ b/test/libsolidity/smtCheckerTests/operators/unary_add.sol @@ -14,4 +14,4 @@ contract C } } // ---- -// Warning 6328: (194-207): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (194-207): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 4\na = 3\nb = 3\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/unary_add_overflows_correctly.sol b/test/libsolidity/smtCheckerTests/operators/unary_add_overflows_correctly.sol index 0b992b1e9..2e4ebf64f 100644 --- a/test/libsolidity/smtCheckerTests/operators/unary_add_overflows_correctly.sol +++ b/test/libsolidity/smtCheckerTests/operators/unary_add_overflows_correctly.sol @@ -13,4 +13,4 @@ contract C { } } // ---- -// Warning 4984: (94-97): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\nx = 255\n\nTransaction trace:\nC.constructor()\nState: x = 254\nC.inc_pre()\nState: x = 255\nC.inc_pre() +// Warning 4984: (94-97): CHC: Overflow (resulting value larger than 255) happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/unary_add_overflows_correctly_struct.sol b/test/libsolidity/smtCheckerTests/operators/unary_add_overflows_correctly_struct.sol index 3c449bfde..7e1791776 100644 --- a/test/libsolidity/smtCheckerTests/operators/unary_add_overflows_correctly_struct.sol +++ b/test/libsolidity/smtCheckerTests/operators/unary_add_overflows_correctly_struct.sol @@ -21,4 +21,4 @@ contract C { } } // ---- -// Warning 4984: (145-150): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\ns = {x: 255}\n\nTransaction trace:\nC.constructor()\nState: s = {x: 254}\nC.inc_pre()\nState: s = {x: 255}\nC.inc_pre() +// Warning 4984: (145-150): CHC: Overflow (resulting value larger than 255) happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/unary_operators_tuple_3.sol b/test/libsolidity/smtCheckerTests/operators/unary_operators_tuple_3.sol index a7aa7e81b..59fa83a08 100644 --- a/test/libsolidity/smtCheckerTests/operators/unary_operators_tuple_3.sol +++ b/test/libsolidity/smtCheckerTests/operators/unary_operators_tuple_3.sol @@ -9,4 +9,4 @@ contract C { } } // ---- -// Warning 6328: (140-150): CHC: Assertion violation happens here.\nCounterexample:\n\nb = true\n\nTransaction trace:\nC.constructor()\nC.f(true) +// Warning 6328: (140-150): CHC: Assertion violation happens here.\nCounterexample:\n\nb = true\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f(true) diff --git a/test/libsolidity/smtCheckerTests/operators/unary_sub.sol b/test/libsolidity/smtCheckerTests/operators/unary_sub.sol index b90186faf..614e7d272 100644 --- a/test/libsolidity/smtCheckerTests/operators/unary_sub.sol +++ b/test/libsolidity/smtCheckerTests/operators/unary_sub.sol @@ -14,4 +14,4 @@ contract C } } // ---- -// Warning 6328: (194-207): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (194-207): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\na = 4\nb = 4\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol b/test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol index 2fc3020eb..2f109534e 100644 --- a/test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol +++ b/test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol @@ -21,6 +21,6 @@ contract C { // ---- // Warning 4984: (145-148): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 3944: (214-217): CHC: Underflow (resulting value less than 0) might happen here. -// Warning 6368: (292-296): CHC: Out of bounds access happens here.\nCounterexample:\na = [0], l = 1\n = 0\n\nTransaction trace:\nC.constructor()\nState: a = [], l = 0\nC.p()\nState: a = [0], l = 1\nC.r() +// Warning 6368: (292-296): CHC: Out of bounds access happens here. // Warning 2661: (145-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 4144: (214-217): BMC: Underflow (resulting value less than 0) happens here. diff --git a/test/libsolidity/smtCheckerTests/out_of_bounds/array_2d_4.sol b/test/libsolidity/smtCheckerTests/out_of_bounds/array_2d_4.sol index 88af3d3dd..6baaaee2e 100644 --- a/test/libsolidity/smtCheckerTests/out_of_bounds/array_2d_4.sol +++ b/test/libsolidity/smtCheckerTests/out_of_bounds/array_2d_4.sol @@ -15,9 +15,11 @@ contract C { } // ---- // Warning 4984: (217-230): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. -// Warning 6368: (261-265): CHC: Out of bounds access happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.r() +// Warning 6368: (261-265): CHC: Out of bounds access happens here.\nCounterexample:\na = []\ni = 0\nj = 0\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.r() // Warning 4984: (261-277): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. -// Warning 6368: (288-292): CHC: Out of bounds access happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.r() -// Warning 6368: (288-295): CHC: Out of bounds access happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.r() +// Warning 6368: (288-292): CHC: Out of bounds access happens here.\nCounterexample:\na = []\ni = 0\nj = 0\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.r() +// Warning 6368: (288-295): CHC: Out of bounds access happens here.\nCounterexample:\na = []\ni = 0\nj = 0\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.r() +// Warning 4984: (279-282): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. +// Warning 4984: (232-235): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 2661: (217-230): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 2661: (261-277): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/overflow/overflow_constant_bound.sol b/test/libsolidity/smtCheckerTests/overflow/overflow_constant_bound.sol index d084fab5d..4fcc079aa 100644 --- a/test/libsolidity/smtCheckerTests/overflow/overflow_constant_bound.sol +++ b/test/libsolidity/smtCheckerTests/overflow/overflow_constant_bound.sol @@ -13,5 +13,6 @@ contract DepositContract { } } // ---- +// Warning 1218: (289-310): CHC: Error trying to invoke SMT solver. // Warning 4984: (289-310): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 2661: (289-310): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/overflow/overflow_mul.sol b/test/libsolidity/smtCheckerTests/overflow/overflow_mul.sol index 3cd50dc8f..542defb12 100644 --- a/test/libsolidity/smtCheckerTests/overflow/overflow_mul.sol +++ b/test/libsolidity/smtCheckerTests/overflow/overflow_mul.sol @@ -13,4 +13,4 @@ contract C } } // ---- -// Warning 4984: (120-125): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\n\nx = 100\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(0) +// Warning 4984: (120-125): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\n\nx = 100\n = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(0) diff --git a/test/libsolidity/smtCheckerTests/overflow/overflow_mul_cex_with_array.sol b/test/libsolidity/smtCheckerTests/overflow/overflow_mul_cex_with_array.sol index 3f9785aad..5f0e2bb2e 100644 --- a/test/libsolidity/smtCheckerTests/overflow/overflow_mul_cex_with_array.sol +++ b/test/libsolidity/smtCheckerTests/overflow/overflow_mul_cex_with_array.sol @@ -7,6 +7,8 @@ contract C { x[8][5*y]; } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 4984: (144-147): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = [38, 38, 38, 38, 38, 38, 9, 38, 38, 38, 13]\ny = 23158417847463239084714197001737581570653996933128112807891516801582625927988\n\nTransaction trace:\nC.constructor()\nC.f([38, 38, 38, 38, 38, 38, 9, 38, 38, 38, 13], 23158417847463239084714197001737581570653996933128112807891516801582625927988) -// Warning 6368: (139-148): CHC: Out of bounds access happens here.\nCounterexample:\n\nx = [38, 38, 38, 38, 38, 38, 38, 9, 38, 38, 38]\ny = 1\n\nTransaction trace:\nC.constructor()\nC.f([38, 38, 38, 38, 38, 38, 38, 9, 38, 38, 38], 1) +// Warning 4984: (144-147): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 6368: (139-148): CHC: Out of bounds access happens here. diff --git a/test/libsolidity/smtCheckerTests/overflow/overflow_mul_signed.sol b/test/libsolidity/smtCheckerTests/overflow/overflow_mul_signed.sol index 65dbe1aa7..b2df23fff 100644 --- a/test/libsolidity/smtCheckerTests/overflow/overflow_mul_signed.sol +++ b/test/libsolidity/smtCheckerTests/overflow/overflow_mul_signed.sol @@ -13,4 +13,4 @@ contract C } } // ---- -// Warning 4984: (169-176): CHC: Overflow (resulting value larger than 127) happens here.\nCounterexample:\n\nx = 100\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(0) +// Warning 4984: (169-176): CHC: Overflow (resulting value larger than 127) happens here.\nCounterexample:\n\nx = 100\n = 0\ny = (- 56)\n\nTransaction trace:\nC.constructor()\nC.f(0) diff --git a/test/libsolidity/smtCheckerTests/overflow/overflow_sum.sol b/test/libsolidity/smtCheckerTests/overflow/overflow_sum.sol index 5651a8dc4..787a851b3 100644 --- a/test/libsolidity/smtCheckerTests/overflow/overflow_sum.sol +++ b/test/libsolidity/smtCheckerTests/overflow/overflow_sum.sol @@ -15,4 +15,4 @@ contract C } } // ---- -// Warning 4984: (218-225): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\n\nx = 255\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(0) +// Warning 4984: (218-225): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\n\nx = 255\n = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(0) diff --git a/test/libsolidity/smtCheckerTests/overflow/signed_guard_sum_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/signed_guard_sum_overflow.sol index 88cc32d07..685392026 100644 --- a/test/libsolidity/smtCheckerTests/overflow/signed_guard_sum_overflow.sol +++ b/test/libsolidity/smtCheckerTests/overflow/signed_guard_sum_overflow.sol @@ -6,6 +6,8 @@ contract C { return x + y; } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 3944: (111-116): CHC: Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here.\nCounterexample:\n\nx = (- 1)\ny = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f((- 1), (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)) -// Warning 4984: (111-116): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = 1\ny = 57896044618658097711785492504343953926634992332820282019728792003956564819967\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(1, 57896044618658097711785492504343953926634992332820282019728792003956564819967) +// Warning 3944: (111-116): CHC: Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here. +// Warning 4984: (111-116): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/overflow/signed_sub_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/signed_sub_overflow.sol index ffa00f92c..824f81193 100644 --- a/test/libsolidity/smtCheckerTests/overflow/signed_sub_overflow.sol +++ b/test/libsolidity/smtCheckerTests/overflow/signed_sub_overflow.sol @@ -5,6 +5,8 @@ contract C { return x - y; } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 3944: (110-115): CHC: Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here.\nCounterexample:\n\nx = (- 2)\ny = 57896044618658097711785492504343953926634992332820282019728792003956564819967\n = 0\n\nTransaction trace:\nC.constructor()\nC.f((- 2), 57896044618658097711785492504343953926634992332820282019728792003956564819967) -// Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = 0\ny = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)) +// Warning 3944: (110-115): CHC: Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here. +// Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/overflow/signed_sum_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/signed_sum_overflow.sol index 5186f81f1..efc719169 100644 --- a/test/libsolidity/smtCheckerTests/overflow/signed_sum_overflow.sol +++ b/test/libsolidity/smtCheckerTests/overflow/signed_sum_overflow.sol @@ -5,6 +5,8 @@ contract C { return x + y; } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 3944: (110-115): CHC: Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here.\nCounterexample:\n\nx = (- 1)\ny = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f((- 1), (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)) -// Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = 1\ny = 57896044618658097711785492504343953926634992332820282019728792003956564819967\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(1, 57896044618658097711785492504343953926634992332820282019728792003956564819967) +// Warning 3944: (110-115): CHC: Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here. +// Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/overflow/unsigned_guard_sum_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/unsigned_guard_sum_overflow.sol index 06d9884b7..e512f6b56 100644 --- a/test/libsolidity/smtCheckerTests/overflow/unsigned_guard_sum_overflow.sol +++ b/test/libsolidity/smtCheckerTests/overflow/unsigned_guard_sum_overflow.sol @@ -5,5 +5,7 @@ contract C { return x + y; } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 4984: (113-118): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 1\ny = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935) +// Warning 4984: (113-118): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/overflow/unsigned_mul_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/unsigned_mul_overflow.sol index f888f5b07..9e9b6605a 100644 --- a/test/libsolidity/smtCheckerTests/overflow/unsigned_mul_overflow.sol +++ b/test/libsolidity/smtCheckerTests/overflow/unsigned_mul_overflow.sol @@ -6,4 +6,4 @@ contract C { } } // ---- -// Warning 4984: (113-118): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 57896044618658097711785492504343953926634992332820282019728792003956564819968\ny = 2\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(57896044618658097711785492504343953926634992332820282019728792003956564819968, 2) +// Warning 4984: (113-118): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 2\ny = 57896044618658097711785492504343953926634992332820282019728792003956564819968\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(2, 57896044618658097711785492504343953926634992332820282019728792003956564819968) diff --git a/test/libsolidity/smtCheckerTests/overflow/unsigned_sum_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/unsigned_sum_overflow.sol index 06d9884b7..e512f6b56 100644 --- a/test/libsolidity/smtCheckerTests/overflow/unsigned_sum_overflow.sol +++ b/test/libsolidity/smtCheckerTests/overflow/unsigned_sum_overflow.sol @@ -5,5 +5,7 @@ contract C { return x + y; } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 4984: (113-118): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 1\ny = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935) +// Warning 4984: (113-118): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol index bfbe68e85..7be611742 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol @@ -14,6 +14,6 @@ contract C { // Warning 2072: (184-188): Unused local variable. // Warning 8364: (155-156): Assertion checker does not yet implement type type(contract C) // Warning 8364: (225-226): Assertion checker does not yet implement type type(contract C) -// Warning 6328: (252-268): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 13, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10]\n\nTransaction trace:\nC.constructor()\nC.f([10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 13, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10]) +// Warning 6328: (252-268): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 13, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10]\na1 = 7719\nb1 = 5\nc1 = 6\na2 = 7719\nb2 = 5\nc2 = 6\n\nTransaction trace:\nC.constructor()\nC.f([10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 13, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10]) // Warning 8364: (155-156): Assertion checker does not yet implement type type(contract C) // Warning 8364: (225-226): Assertion checker does not yet implement type type(contract C) diff --git a/test/libsolidity/smtCheckerTests/special/blockhash.sol b/test/libsolidity/smtCheckerTests/special/blockhash.sol index 346f52fc7..a8f339687 100644 --- a/test/libsolidity/smtCheckerTests/special/blockhash.sol +++ b/test/libsolidity/smtCheckerTests/special/blockhash.sol @@ -10,5 +10,5 @@ contract C } } // ---- -// Warning 6328: (85-109): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 7719 } -// Warning 6328: (113-137): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 21238 } +// Warning 6328: (85-109): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 8365 } +// Warning 6328: (113-137): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 32285 } diff --git a/test/libsolidity/smtCheckerTests/special/difficulty.sol b/test/libsolidity/smtCheckerTests/special/difficulty.sol index d3ca19baf..f76a8d0c5 100644 --- a/test/libsolidity/smtCheckerTests/special/difficulty.sol +++ b/test/libsolidity/smtCheckerTests/special/difficulty.sol @@ -6,5 +6,7 @@ contract C assert(block.difficulty == difficulty); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (91-129): CHC: Assertion violation happens here.\nCounterexample:\n\ndifficulty = 39\n\nTransaction trace:\nC.constructor()\nC.f(39) +// Warning 6328: (91-129): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/special/event.sol b/test/libsolidity/smtCheckerTests/special/event.sol index 21a63fc05..824baa751 100644 --- a/test/libsolidity/smtCheckerTests/special/event.sol +++ b/test/libsolidity/smtCheckerTests/special/event.sol @@ -27,4 +27,4 @@ contract C { // ---- // Warning 6321: (280-284): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. // Warning 6321: (430-434): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. -// Warning 6328: (440-449): CHC: Assertion violation happens here.\nCounterexample:\nx = false\n\nTransaction trace:\nC.constructor()\nState: x = true\nC.h()\n C.h_data() -- internal call +// Warning 6328: (440-449): CHC: Assertion violation happens here.\nCounterexample:\nx = false\n\nTransaction trace:\nC.constructor()\nState: x = true\nC.h()\n C.h_data() -- internal call\n C.h_data() -- internal call diff --git a/test/libsolidity/smtCheckerTests/special/gasleft.sol b/test/libsolidity/smtCheckerTests/special/gasleft.sol index 61638b241..65ae240a6 100644 --- a/test/libsolidity/smtCheckerTests/special/gasleft.sol +++ b/test/libsolidity/smtCheckerTests/special/gasleft.sol @@ -10,5 +10,5 @@ contract C } } // ---- -// Warning 6328: (76-97): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (123-144): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (76-97): CHC: Assertion violation happens here.\nCounterexample:\n\ng = 0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (123-144): CHC: Assertion violation happens here.\nCounterexample:\n\ng = 0\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol b/test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol index 14d4ac950..0f5f88394 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol @@ -9,5 +9,7 @@ contract C assert(c == msg.sender); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (155-178): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 39\n\nTransaction trace:\nC.constructor()\nC.f(39) +// Warning 6328: (155-178): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/special/this.sol b/test/libsolidity/smtCheckerTests/special/this.sol index 56826fe64..178b4e512 100644 --- a/test/libsolidity/smtCheckerTests/special/this.sol +++ b/test/libsolidity/smtCheckerTests/special/this.sol @@ -6,5 +6,7 @@ contract C assert(a == address(this)); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (85-111): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\n\nTransaction trace:\nC.constructor()\nC.f(0) +// Warning 6328: (85-111): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_1.sol b/test/libsolidity/smtCheckerTests/try_catch/try_1.sol index c27fa8494..903c94346 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_1.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_1.sol @@ -19,4 +19,4 @@ contract C { } // ---- // Warning 5667: (195-209): Unused try/catch parameter. Remove or comment out the variable name to silence this warning. -// Warning 6328: (253-268): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f() +// Warning 6328: (253-268): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\nsuccess = false\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_3.sol b/test/libsolidity/smtCheckerTests/try_catch/try_3.sol index d21deaed2..d5318f0e4 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_3.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_3.sol @@ -22,4 +22,4 @@ contract C { } // ---- // Warning 5667: (291-305): Unused try/catch parameter. Remove or comment out the variable name to silence this warning. -// Warning 6328: (312-326): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()\n C.postinc() -- internal call +// Warning 6328: (312-326): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\ns = []\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()\n C.postinc() -- internal call diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses.sol b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses.sol index c33006f9a..93c2fb936 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses.sol @@ -22,4 +22,4 @@ contract C { } } // ---- -// Warning 6328: (447-462): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f() +// Warning 6328: (447-462): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\nsuccess = false\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol index 1d01f803f..6cc283e47 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol @@ -19,4 +19,4 @@ contract C { } } // ---- -// Warning 6328: (338-352): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (338-352): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\nsuccess = false\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values.sol b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values.sol index c5ee0e83c..d57e447d8 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values.sol @@ -22,6 +22,6 @@ contract C { } // ---- // Warning 2519: (197-203): This declaration shadows an existing declaration. -// Warning 6328: (218-232): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()\n d.d() -- untrusted external call -// Warning 6328: (306-316): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()\n d.d() -- untrusted external call +// Warning 6328: (218-232): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\nx = 1\nc = false\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()\n d.d() -- untrusted external call +// Warning 6328: (306-316): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\nx = 1\nc = true\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()\n d.d() -- untrusted external call // Warning 6328: (426-440): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values_with_tuple.sol b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values_with_tuple.sol index 652ed7913..c6db557ea 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values_with_tuple.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values_with_tuple.sol @@ -23,4 +23,4 @@ contract C { } } // ---- -// Warning 6328: (353-368): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (353-368): CHC: Assertion violation happens here.\nCounterexample:\n\nsuccess = false\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_nested_1.sol b/test/libsolidity/smtCheckerTests/try_catch/try_nested_1.sol index 9c9548e78..2b05f39ff 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_nested_1.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_nested_1.sol @@ -17,5 +17,7 @@ contract C { assert(y == 42); // should fail } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (312-327): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f() +// Warning 6328: (312-327): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_nested_2.sol b/test/libsolidity/smtCheckerTests/try_catch/try_nested_2.sol index dbd8dc09e..509cda911 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_nested_2.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_nested_2.sol @@ -19,4 +19,4 @@ contract C { } } // ---- -// Warning 6328: (374-394): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (374-394): CHC: Assertion violation happens here.\nCounterexample:\n\nchoice = 3\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_nested_3.sol b/test/libsolidity/smtCheckerTests/try_catch/try_nested_3.sol index 88c6e8648..7c24db882 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_nested_3.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_nested_3.sol @@ -19,4 +19,4 @@ contract C { } } // ---- -// Warning 6328: (355-375): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (355-375): CHC: Assertion violation happens here.\nCounterexample:\n\nchoice = 3\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/typecast/address_literal.sol b/test/libsolidity/smtCheckerTests/typecast/address_literal.sol index e2be56508..42a09c49f 100644 --- a/test/libsolidity/smtCheckerTests/typecast/address_literal.sol +++ b/test/libsolidity/smtCheckerTests/typecast/address_literal.sol @@ -22,4 +22,4 @@ contract C { } } // ---- -// Warning 6328: (487-501): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g() +// Warning 6328: (487-501): 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() diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_larger_2_fail.sol b/test/libsolidity/smtCheckerTests/typecast/cast_larger_2_fail.sol index 519fedab9..bf85dc82f 100644 --- a/test/libsolidity/smtCheckerTests/typecast/cast_larger_2_fail.sol +++ b/test/libsolidity/smtCheckerTests/typecast/cast_larger_2_fail.sol @@ -9,4 +9,4 @@ contract C } } // ---- -// Warning 6328: (149-163): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (149-163): CHC: Assertion violation happens here.\nCounterexample:\n\na = 4660\nb = 4660\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 32bdee5cd..cc9855984 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 } } // ---- -// Warning 6328: (273-287): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (273-287): CHC: Assertion violation happens here.\nCounterexample:\n\na = 4660\nb = 305397760\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 25865fd33..e8b43ae7e 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 { function g(bytes1 b) internal pure {} } // ---- -// Warning 6328: (186-207): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()\n C.g(0) -- internal call +// Warning 6328: (186-207): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\nb = 0\n\nTransaction trace:\nC.constructor()\nC.f()\n C.g(0) -- 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 590063826..0477e690a 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 { } } // ---- -// Warning 6328: (206-240): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (206-240): CHC: Assertion violation happens here.\nCounterexample:\n\nb = [255, 255]\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 2044386ec..dc839d5a1 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 @@ -8,4 +8,4 @@ contract B { } } // ---- -// Warning 6328: (152-174): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nB.constructor()\nB.f() +// Warning 6328: (152-174): CHC: Assertion violation happens here.\nCounterexample:\n\na = 13564890559296822\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 e7b5c702e..4940c1238 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 @@ -12,4 +12,4 @@ contract C { } } // ---- -// Warning 6328: (442-461): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.a()\n C.f2() -- internal call\n C.h() -- internal call +// Warning 6328: (442-461): 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 diff --git a/test/libsolidity/smtCheckerTests/types/address_balance.sol b/test/libsolidity/smtCheckerTests/types/address_balance.sol index 64c84675f..9b2352ba9 100644 --- a/test/libsolidity/smtCheckerTests/types/address_balance.sol +++ b/test/libsolidity/smtCheckerTests/types/address_balance.sol @@ -9,5 +9,5 @@ contract C } // ---- // Warning 2072: (96-102): Unused local variable. -// Warning 4984: (105-127): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\na = 0\nb = 38\n\nTransaction trace:\nC.constructor()\nC.f(0, 38) -// Warning 6328: (131-160): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7719\nb = 38\n\nTransaction trace:\nC.constructor()\nC.f(7719, 38) +// Warning 4984: (105-127): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\na = 0\nb = 38\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 38) +// Warning 6328: (131-160): CHC: Assertion violation happens here.\nCounterexample:\n\na = 21238\nb = 7719\nx = 1000000000000000000038\n\nTransaction trace:\nC.constructor()\nC.f(21238, 7719) diff --git a/test/libsolidity/smtCheckerTests/types/address_call.sol b/test/libsolidity/smtCheckerTests/types/address_call.sol index 3960956a0..b6f1bcbfe 100644 --- a/test/libsolidity/smtCheckerTests/types/address_call.sol +++ b/test/libsolidity/smtCheckerTests/types/address_call.sol @@ -17,11 +17,12 @@ contract C } // ==== // EVMVersion: >spuriousDragon +// SMTIgnoreCex: yes // ---- // Warning 2072: (224-240): Unused local variable. // Warning 4588: (244-256): Assertion checker does not yet implement this type of function call. -// Warning 6328: (260-275): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data) -// Warning 6328: (279-293): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data) -// Warning 6328: (297-316): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data) -// Warning 6328: (320-344): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data) +// Warning 6328: (260-275): CHC: Assertion violation happens here. +// Warning 6328: (279-293): CHC: Assertion violation happens here. +// Warning 6328: (297-316): CHC: Assertion violation happens here. +// Warning 6328: (320-344): CHC: Assertion violation happens here. // Warning 4588: (244-256): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/types/address_delegatecall.sol b/test/libsolidity/smtCheckerTests/types/address_delegatecall.sol index c61691e6c..6d67a9e66 100644 --- a/test/libsolidity/smtCheckerTests/types/address_delegatecall.sol +++ b/test/libsolidity/smtCheckerTests/types/address_delegatecall.sol @@ -17,11 +17,12 @@ contract C } // ==== // EVMVersion: >spuriousDragon +// SMTIgnoreCex: yes // ---- // Warning 2072: (224-240): Unused local variable. // Warning 4588: (244-264): Assertion checker does not yet implement this type of function call. -// Warning 6328: (268-283): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data) -// Warning 6328: (287-301): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data) -// Warning 6328: (305-324): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data) -// Warning 6328: (328-352): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data) +// Warning 6328: (268-283): CHC: Assertion violation happens here. +// Warning 6328: (287-301): CHC: Assertion violation happens here. +// Warning 6328: (305-324): CHC: Assertion violation happens here. +// Warning 6328: (328-352): CHC: Assertion violation happens here. // Warning 4588: (244-264): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer.sol b/test/libsolidity/smtCheckerTests/types/address_transfer.sol index c641f74e0..555aa8007 100644 --- a/test/libsolidity/smtCheckerTests/types/address_transfer.sol +++ b/test/libsolidity/smtCheckerTests/types/address_transfer.sol @@ -11,5 +11,5 @@ contract C } } // ---- -// Warning 6328: (195-219): CHC: Assertion violation happens here.\nCounterexample:\n\na = 38\n\nTransaction trace:\nC.constructor()\nC.f(38) +// Warning 6328: (195-219): CHC: Assertion violation happens here.\nCounterexample:\n\na = 38\nx = 100\n\nTransaction trace:\nC.constructor()\nC.f(38) // Warning 1236: (131-146): BMC: Insufficient funds happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_1.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_1.sol index 5a77c35f2..51748c1a9 100644 --- a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_1.sol +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_1.sol @@ -50,5 +50,7 @@ contract C //f(array2d[a], array2d[b], array4d[c][c], tinyArray3d[d], array4d[e]); } } +// ==== +// SMTIgnoreCex: yes // ---- // Warning 2018: (990-1362): Function state mutability can be restricted to view diff --git a/test/libsolidity/smtCheckerTests/types/array_dynamic_parameter_1_fail.sol b/test/libsolidity/smtCheckerTests/types/array_dynamic_parameter_1_fail.sol index e0a4e58af..4b187f12e 100644 --- a/test/libsolidity/smtCheckerTests/types/array_dynamic_parameter_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/types/array_dynamic_parameter_1_fail.sol @@ -10,4 +10,4 @@ contract C } } // ---- -// Warning 6328: (177-199): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 7719\ny = 7719\n\nTransaction trace:\nC.constructor()\nC.f(array, 7719, 7719) +// Warning 6328: (177-199): CHC: Assertion violation happens here.\nCounterexample:\n\narray = [9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 12, 9, 9, 9, 9, 9, 9, 9, 9, 21, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 200]\nx = 38\ny = 38\n\nTransaction trace:\nC.constructor()\nC.f([9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 12, 9, 9, 9, 9, 9, 9, 9, 9, 21, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 199], 38, 38) diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_2.sol b/test/libsolidity/smtCheckerTests/types/array_literal_2.sol index 3d38b2ca9..826c85461 100644 --- a/test/libsolidity/smtCheckerTests/types/array_literal_2.sol +++ b/test/libsolidity/smtCheckerTests/types/array_literal_2.sol @@ -11,4 +11,4 @@ contract C } } // ---- -// Warning 6328: (200-220): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (200-220): CHC: Assertion violation happens here.\nCounterexample:\n\na = [1, 2, 3]\nb = [1, 2, 4]\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_3.sol b/test/libsolidity/smtCheckerTests/types/array_literal_3.sol index 5bb99490f..6d25027b7 100644 --- a/test/libsolidity/smtCheckerTests/types/array_literal_3.sol +++ b/test/libsolidity/smtCheckerTests/types/array_literal_3.sol @@ -10,4 +10,4 @@ contract C } } // ---- -// Warning 6328: (201-221): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (201-221): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_5.sol b/test/libsolidity/smtCheckerTests/types/array_literal_5.sol index db8634d53..1a73de324 100644 --- a/test/libsolidity/smtCheckerTests/types/array_literal_5.sol +++ b/test/libsolidity/smtCheckerTests/types/array_literal_5.sol @@ -13,4 +13,4 @@ contract C } } // ---- -// Warning 6328: (209-229): CHC: Assertion violation happens here.\nCounterexample:\ns = [1, 2, 3]\n\nTransaction trace:\nC.constructor()\nState: s = []\nC.f() +// Warning 6328: (209-229): CHC: Assertion violation happens here.\nCounterexample:\ns = [1, 2, 3]\na = [1, 2, 3]\n\nTransaction trace:\nC.constructor()\nState: s = []\nC.f() diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_6.sol b/test/libsolidity/smtCheckerTests/types/array_literal_6.sol index 31d4706a7..4b36a1395 100644 --- a/test/libsolidity/smtCheckerTests/types/array_literal_6.sol +++ b/test/libsolidity/smtCheckerTests/types/array_literal_6.sol @@ -14,5 +14,5 @@ contract C } } // ---- -// Warning 6328: (179-207): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (268-288): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (179-207): CHC: Assertion violation happens here.\nCounterexample:\n\na = [1, 2, 3]\nb = [1, 2, 4, 3]\nc = [1, 2, 4, 3]\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (268-288): CHC: Assertion violation happens here.\nCounterexample:\n\na = [1, 2, 3]\nb = [1, 2, 4, 3]\nc = [1, 2, 4, 3]\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_7.sol b/test/libsolidity/smtCheckerTests/types/array_literal_7.sol index dcb84ca36..f9401a56c 100644 --- a/test/libsolidity/smtCheckerTests/types/array_literal_7.sol +++ b/test/libsolidity/smtCheckerTests/types/array_literal_7.sol @@ -19,5 +19,5 @@ contract C } } // ---- -// Warning 6328: (259-287): CHC: Assertion violation happens here.\nCounterexample:\ns = [1, 2, 3]\n\nTransaction trace:\nC.constructor()\nState: s = []\nC.f() -// Warning 6328: (348-368): CHC: Assertion violation happens here.\nCounterexample:\ns = [1, 2, 3]\n\nTransaction trace:\nC.constructor()\nState: s = []\nC.f() +// Warning 6328: (259-287): CHC: Assertion violation happens here.\nCounterexample:\ns = [1, 2, 3]\na = [1, 2, 3]\nb = [1, 2, 4, 3]\nc = [1, 2, 4, 3]\n\nTransaction trace:\nC.constructor()\nState: s = []\nC.f() +// Warning 6328: (348-368): CHC: Assertion violation happens here.\nCounterexample:\ns = [1, 2, 3]\na = [1, 2, 3]\nb = [1, 2, 4, 3]\nc = [1, 2, 4, 3]\n\nTransaction trace:\nC.constructor()\nState: s = []\nC.f() diff --git a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol index b18fffe9f..93bb86d25 100644 --- a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol +++ b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol @@ -28,6 +28,8 @@ contract C f(severalMaps3d[x][0]); } } +// ==== +// SMTIgnoreCex: yes // ---- // Warning 6368: (347-361): CHC: Out of bounds access happens here. // Warning 6368: (400-416): CHC: Out of bounds access happens here. diff --git a/test/libsolidity/smtCheckerTests/types/contract_address_conversion.sol b/test/libsolidity/smtCheckerTests/types/contract_address_conversion.sol index f3396bfd4..32092ff37 100644 --- a/test/libsolidity/smtCheckerTests/types/contract_address_conversion.sol +++ b/test/libsolidity/smtCheckerTests/types/contract_address_conversion.sol @@ -6,5 +6,7 @@ contract C assert(address(c) == a); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (90-113): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 1\na = 0\n\nTransaction trace:\nC.constructor()\nC.f(1, 0) +// Warning 6328: (90-113): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_4.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_4.sol index f3a669805..c6fdb936b 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 { } } // ---- -// Warning 6328: (264-285): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (264-285): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 450552876409790643671482431940419874915447411150352389258589821042463539455\nz = 0\no = 255\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 6302fe72f..75069d37f 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 { } } // ---- -// Warning 6328: (120-137): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (171-188): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (201-218): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (120-137): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 16909060\nb = 2\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (171-188): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 16909060\nb = 2\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (201-218): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 16909060\nb = 2\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 a57b8ed31..9d47088e6 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 { } } // ---- -// Warning 6368: (132-136): CHC: Out of bounds access happens here.\nCounterexample:\n\ni = 4\n\nTransaction trace:\nC.constructor()\nC.f(4) -// Warning 6328: (125-145): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 4\n\nTransaction trace:\nC.constructor()\nC.f(4) +// Warning 6368: (132-136): CHC: Out of bounds access happens here.\nCounterexample:\n\ni = 4\nx = 16909060\n\nTransaction trace:\nC.constructor()\nC.f(4) +// Warning 6328: (125-145): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 4\nx = 16909060\n\nTransaction trace:\nC.constructor()\nC.f(4) diff --git a/test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol b/test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol index 86bdf1569..76c34fe51 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol @@ -11,5 +11,7 @@ contract c { assert(x[a] == b); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (289-306): CHC: Assertion violation happens here.\nCounterexample:\n\na = 38\nb = 21238\n\nTransaction trace:\nc.constructor()\nc.g(38, 21238)\n c.f(map, 38, 21238) -- internal call +// Warning 6328: (289-306): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol b/test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol index 53b8e5941..7c9e79b2c 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol @@ -9,4 +9,4 @@ contract C } } // ---- -// Warning 6328: (119-133): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(1, 0) +// Warning 6328: (119-133): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 1\n\nTransaction trace:\nC.constructor()\nC.f(0, 1) diff --git a/test/libsolidity/smtCheckerTests/types/rational_large_1.sol b/test/libsolidity/smtCheckerTests/types/rational_large_1.sol index 6e24e43a3..b80ee66cb 100644 --- a/test/libsolidity/smtCheckerTests/types/rational_large_1.sol +++ b/test/libsolidity/smtCheckerTests/types/rational_large_1.sol @@ -8,4 +8,4 @@ contract c { } // ---- // Warning 6321: (80-84): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. -// Warning 6328: (128-142): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0\n\nTransaction trace:\nc.constructor()\nc.f() +// Warning 6328: (128-142): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0\nx = 8\n\nTransaction trace:\nc.constructor()\nc.f() diff --git a/test/libsolidity/smtCheckerTests/types/string_1.sol b/test/libsolidity/smtCheckerTests/types/string_1.sol index e85dc1d29..8b2ad44b0 100644 --- a/test/libsolidity/smtCheckerTests/types/string_1.sol +++ b/test/libsolidity/smtCheckerTests/types/string_1.sol @@ -7,4 +7,4 @@ contract C } } // ---- -// Warning 6328: (110-154): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(s1, s2) +// Warning 6328: (110-154): CHC: Assertion violation happens here.\nCounterexample:\n\ns1 = [26, 26, 26, 26, 26, 26, 26, 9, 26, 26, 26, 26, 26, 14, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26]\ns2 = [18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 15, 18, 18, 18, 18, 18, 22, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18]\n\nTransaction trace:\nC.constructor()\nC.f([26, 26, 26, 26, 26, 26, 26, 9, 26, 26, 26, 26, 26, 14, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26], [18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 15, 18, 18, 18, 18, 18, 22, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18]) diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_1.sol b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_1.sol index 428e12fbb..25ca88489 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 { } } // ---- -// Warning 6328: (175-190): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293568\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293568) +// Warning 6328: (175-190): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293568\ny = 52647538817385212172903286807934654968315727694643370704309751478220717293568\nz = 154717211199090701642289212291190620160\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293568) diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_2.sol b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_2.sol index 9bffe8cb5..555f1228f 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 { } } // ---- -// Warning 6328: (176-191): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293568\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293568) +// Warning 6328: (176-191): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293568\ny = 52647538817385212172903286807934654968315727694643370704309751478220717293568\nz = 154717211199090701642289212291190620160\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293568) diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_3.sol b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_3.sol index ac018261b..d940e6063 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 { } } // ---- -// Warning 6328: (186-201): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293568\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293568) +// Warning 6328: (186-201): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293568\ny = 52647538817385212172903286807934654968315727694643370704309751478220717293568\nz = 154717211199090701642289212291190620160\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293568) diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_4.sol b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_4.sol index 766e73c8a..c96863e12 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 { } } // ---- -// Warning 6328: (261-276): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293568\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293568)\n C.g() -- internal call +// Warning 6328: (261-276): 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 diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_5.sol b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_5.sol index 39f7a4758..e32c28613 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 { } } // ---- -// Warning 6328: (251-266): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293568\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293568)\n C.g() -- internal call +// Warning 6328: (251-266): 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 diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_comparison_1.sol b/test/libsolidity/smtCheckerTests/types/string_literal_comparison_1.sol index e9e829fdc..62f84f0f5 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 { } } // ---- -// Warning 6328: (170-190): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293568\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293568) +// Warning 6328: (170-190): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293568\ny = 52647538817385212172903286807934654968315727694643370704309751478220717293568\nz = 52647538817385212172903286807934654968315727694643370704309751478220717293568\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293568) diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_comparison_2.sol b/test/libsolidity/smtCheckerTests/types/string_literal_comparison_2.sol index 849b69c4f..8c9b23539 100644 --- a/test/libsolidity/smtCheckerTests/types/string_literal_comparison_2.sol +++ b/test/libsolidity/smtCheckerTests/types/string_literal_comparison_2.sol @@ -10,5 +10,5 @@ contract C { } } // ---- -// Warning 6328: (147-166): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293569\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293569) -// Warning 6328: (170-190): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538830022687173130149211684818290356179572910782152375644828738034597888\n\nTransaction trace:\nC.constructor()\nC.f(52647538830022687173130149211684818290356179572910782152375644828738034597888) +// Warning 6328: (147-166): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 0\ny = 0\nz = 0\n\nTransaction trace:\nC.constructor()\nC.f(0) +// Warning 6328: (170-190): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538830022687173130149211684818290356179572910782152375644828738034597888\ny = 52647538830022687173130149211684818290356179572910782152375644828738034597888\nz = 52647538830022687173130149211684818290356179572910782152375644828738034597888\n\nTransaction trace:\nC.constructor()\nC.f(52647538830022687173130149211684818290356179572910782152375644828738034597888) diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_storage.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_storage.sol index dd1ad831a..5191e9daf 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_storage.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_storage.sol @@ -26,4 +26,4 @@ contract C { } } // ---- -// Warning 6328: (402-438): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 0, a: []}, s2 = {x: 0, a: []}\nb = false\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, a: []}, s2 = {x: 0, a: []}\nC.f(false) +// Warning 6328: (402-438): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 0, a: []}, s2 = {x: 0, a: []}\nb = false\ns3 = {x: 42, a: []}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, a: []}, s2 = {x: 0, a: []}\nC.f(false) diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_1.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_1.sol index 10065f557..2f3a523b2 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_1.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_1.sol @@ -30,8 +30,8 @@ contract C { } } // ---- -// Warning 6328: (228-245): CHC: Assertion violation happens here. -// Warning 6328: (263-282): CHC: Assertion violation happens here. -// Warning 6328: (325-345): CHC: Assertion violation happens here. -// Warning 6328: (389-412): CHC: Assertion violation happens here. -// Warning 6328: (467-493): CHC: Assertion violation happens here. +// Warning 6328: (228-245): CHC: Assertion violation happens here.\nCounterexample:\n\ns1 = {x: 2, t: {y: 0, a: []}, a: [], ts: []}\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (263-282): CHC: Assertion violation happens here.\nCounterexample:\n\ns1 = {x: 2, t: {y: 3, a: []}, a: [], ts: []}\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (325-345): CHC: Assertion violation happens here.\nCounterexample:\n\ns1 = {x: 2, t: {y: 3, a: []}, a: [0, 0, 4], ts: []}\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (389-412): CHC: Assertion violation happens here.\nCounterexample:\n\ns1 = {x: 2, t: {y: 3, a: []}, a: [0, 0, 4], ts: [{y: 0, a: []}, {y: 0, a: []}, {y: 0, a: []}, {y: 5, a: []}, {y: 0, a: []}, {y: 0, a: []}]}\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (467-493): CHC: Assertion violation happens here.\nCounterexample:\n\ns1 = {x: 2, t: {y: 3, a: []}, a: [0, 0, 4], ts: [{y: 0, a: []}, {y: 0, a: []}, {y: 0, a: []}, {y: 5, a: []}, {y: 0, a: [0, 0, 0, 0, 0, 6]}, {y: 0, a: []}]}\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol index eaadd0bd0..f9cccd2c7 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol @@ -41,7 +41,7 @@ contract C { } } // ---- -// Warning 6328: (181-198): CHC: Assertion violation happens here. +// Warning 6328: (181-198): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 2, t: {y: 0, a: []}, a: [], ts: []}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, t: {y: 0, a: []}, a: [], ts: []}\nC.f() // Warning 6328: (216-235): CHC: Assertion violation happens here. // Warning 6328: (299-319): CHC: Assertion violation happens here. // Warning 6328: (437-460): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_named_args.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_named_args.sol index 1b4a6b176..fd2ba18e7 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_named_args.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_named_args.sol @@ -20,4 +20,4 @@ contract C { } } // ---- -// Warning 6328: (265-288): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.test() +// Warning 6328: (265-288): CHC: Assertion violation happens here.\nCounterexample:\n\ninner = {x: 43}\nouter = {s: {x: 43}, y: 512}\n\nTransaction trace:\nC.constructor()\nC.test() diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_named_args_2.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_named_args_2.sol index e8e217f50..9ec7425b1 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_named_args_2.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_named_args_2.sol @@ -17,4 +17,4 @@ contract C { } } // ---- -// Warning 6328: (224-264): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.test() +// Warning 6328: (224-264): CHC: Assertion violation happens here.\nCounterexample:\n\ns = {x: 3, y: 2, z: 1}\n\nTransaction trace:\nC.constructor()\nC.test() diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_nested_constructor.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_nested_constructor.sol index e2e7d5573..18ec523f7 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_nested_constructor.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_nested_constructor.sol @@ -20,4 +20,4 @@ contract C { } } // ---- -// Warning 6328: (252-275): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.test() +// Warning 6328: (252-275): CHC: Assertion violation happens here.\nCounterexample:\n\ninner = {x: 43}\nouter = {s: {x: 43}, y: 512}\n\nTransaction trace:\nC.constructor()\nC.test() diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_return.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_return.sol index 917f5d9a4..e9e8311ea 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_return.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_return.sol @@ -18,4 +18,4 @@ contract C { } } // ---- -// Warning 6328: (289-310): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()\n C.s() -- internal call +// Warning 6328: (289-310): CHC: Assertion violation happens here.\nCounterexample:\n\ns2 = {x: 42, a: [0, 0, 43, 0, 0]}\n\nTransaction trace:\nC.constructor()\nC.f()\n C.s() -- internal call diff --git a/test/libsolidity/smtCheckerTests/types/tuple_assignment_compound.sol b/test/libsolidity/smtCheckerTests/types/tuple_assignment_compound.sol index 4f7d6cd4a..6f1016268 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_assignment_compound.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_assignment_compound.sol @@ -10,4 +10,4 @@ contract C } } // ---- -// Warning 6328: (122-136): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (122-136): CHC: Assertion violation happens here.\nCounterexample:\n\na = 4\nb = 3\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/types/tuple_assignment_empty.sol b/test/libsolidity/smtCheckerTests/types/tuple_assignment_empty.sol index cb856e451..c1652dcc9 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_assignment_empty.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_assignment_empty.sol @@ -11,4 +11,4 @@ contract C } } // ---- -// Warning 6328: (132-146): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g() +// Warning 6328: (132-146): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\ny = 0\n\nTransaction trace:\nC.constructor()\nC.g() diff --git a/test/libsolidity/smtCheckerTests/types/tuple_declarations_function_empty.sol b/test/libsolidity/smtCheckerTests/types/tuple_declarations_function_empty.sol index 2954f1e13..1efc84d13 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_declarations_function_empty.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_declarations_function_empty.sol @@ -14,4 +14,4 @@ contract C } } // ---- -// Warning 6328: (224-234): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call +// Warning 6328: (224-234): CHC: Assertion violation happens here.\nCounterexample:\n\nb = true\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/types/tuple_different_count_assignment_1.sol b/test/libsolidity/smtCheckerTests/types/tuple_different_count_assignment_1.sol index 8cf16bac9..1826982b9 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_different_count_assignment_1.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_different_count_assignment_1.sol @@ -9,4 +9,4 @@ contract C { } // ---- // Warning 6321: (79-82): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. -// Warning 6328: (157-171): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (157-171): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0\na = 2\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/types/tuple_different_count_assignment_2.sol b/test/libsolidity/smtCheckerTests/types/tuple_different_count_assignment_2.sol index d2cb5143f..b1b0cc9ba 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_different_count_assignment_2.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_different_count_assignment_2.sol @@ -9,4 +9,4 @@ contract C { } // ---- // Warning 6321: (79-82): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. -// Warning 6328: (159-173): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (159-173): CHC: Assertion violation happens here.\nCounterexample:\n\n = 0\na = 2\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/types/tuple_function.sol b/test/libsolidity/smtCheckerTests/types/tuple_function.sol index 3b03eb313..32868ab75 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_function.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_function.sol @@ -14,5 +14,5 @@ contract C } } // ---- -// Warning 6328: (182-196): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call -// Warning 6328: (200-214): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call +// Warning 6328: (182-196): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\ny = 3\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call +// Warning 6328: (200-214): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\ny = 3\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/types/tuple_function_2.sol b/test/libsolidity/smtCheckerTests/types/tuple_function_2.sol index 3c6f57014..cdf4c103f 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_function_2.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_function_2.sol @@ -14,4 +14,4 @@ contract C } } // ---- -// Warning 6328: (199-213): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call +// Warning 6328: (199-213): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\ny = 0\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/types/tuple_function_3.sol b/test/libsolidity/smtCheckerTests/types/tuple_function_3.sol index 620fbed94..f68ed1330 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_function_3.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_function_3.sol @@ -16,5 +16,5 @@ contract C } } // ---- -// Warning 6328: (205-219): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call -// Warning 6328: (223-237): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call +// Warning 6328: (205-219): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 0\nb = false\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call +// Warning 6328: (223-237): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 0\nb = false\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/unchecked/checked_modifier_called_by_unchecked.sol b/test/libsolidity/smtCheckerTests/unchecked/checked_modifier_called_by_unchecked.sol index 33c2daed6..2a47fbeed 100644 --- a/test/libsolidity/smtCheckerTests/unchecked/checked_modifier_called_by_unchecked.sol +++ b/test/libsolidity/smtCheckerTests/unchecked/checked_modifier_called_by_unchecked.sol @@ -11,4 +11,4 @@ contract C { } } // ---- -// Warning 4984: (258-263): CHC: Overflow (resulting value larger than 65535) happens here.\nCounterexample:\n\na = 65535\nb = 1\nc = 65535\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(65535, 1, 65535) +// Warning 4984: (258-263): CHC: Overflow (resulting value larger than 65535) happens here.\nCounterexample:\n\na = 65535\nb = 1\nc = 65535\n = 0\na = 65535\nb = 1\n\nTransaction trace:\nC.constructor()\nC.f(65535, 1, 65535) diff --git a/test/libsolidity/smtCheckerTests/unchecked/flipping_sign_tests.sol b/test/libsolidity/smtCheckerTests/unchecked/flipping_sign_tests.sol index 29a64f641..4aaaf82e6 100644 --- a/test/libsolidity/smtCheckerTests/unchecked/flipping_sign_tests.sol +++ b/test/libsolidity/smtCheckerTests/unchecked/flipping_sign_tests.sol @@ -9,4 +9,4 @@ contract test { } } // ---- -// Warning 6328: (143-158): CHC: Assertion violation happens here.\nCounterexample:\n\n = false\n\nTransaction trace:\ntest.constructor()\ntest.f() +// Warning 6328: (143-158): CHC: Assertion violation happens here.\nCounterexample:\n\n = false\nx = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\n\nTransaction trace:\ntest.constructor()\ntest.f() diff --git a/test/libsolidity/smtCheckerTests/unchecked/signed_mod.sol b/test/libsolidity/smtCheckerTests/unchecked/signed_mod.sol index 37ab36686..c85f3e120 100644 --- a/test/libsolidity/smtCheckerTests/unchecked/signed_mod.sol +++ b/test/libsolidity/smtCheckerTests/unchecked/signed_mod.sol @@ -15,4 +15,4 @@ contract C { } // ---- // Warning 4281: (118-123): CHC: Division by zero happens here.\nCounterexample:\n\na = 0\nb = 0\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0) -// Warning 4984: (275-281): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\n_check = true\n = 0\n\nTransaction trace:\nC.constructor()\nC.g(true) +// Warning 4984: (275-281): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\n_check = true\n = 0\nx = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\n\nTransaction trace:\nC.constructor()\nC.g(true) diff --git a/test/libsolidity/smtCheckerTests/unchecked/unchecked_function_call_with_unchecked_block.sol b/test/libsolidity/smtCheckerTests/unchecked/unchecked_function_call_with_unchecked_block.sol index 9211c8bd6..e6a087fa0 100644 --- a/test/libsolidity/smtCheckerTests/unchecked/unchecked_function_call_with_unchecked_block.sol +++ b/test/libsolidity/smtCheckerTests/unchecked/unchecked_function_call_with_unchecked_block.sol @@ -11,4 +11,4 @@ contract C { } } // ---- -// Warning 6328: (117-130): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n C.f(0) -- internal call +// Warning 6328: (117-130): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\nTransaction trace:\nC.constructor()\nC.g(0)\n C.f(0) -- internal call