diff --git a/Changelog.md b/Changelog.md index f5698bf3b..b54755170 100644 --- a/Changelog.md +++ b/Changelog.md @@ -15,6 +15,7 @@ Bugfixes: * SMTChecker: Fix internal error when visiting state variable inherited from base class. * SMTChecker: Fix internal error in fixed point operations. * SMTChecker: Fix internal error in assignment to unsupported type. + * SMTChecker: Fix internal error in branching when inlining function calls that modify local variables. diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 4d73adae5..d70aa188a 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -103,25 +103,14 @@ bool SMTChecker::visit(ModifierDefinition const&) bool SMTChecker::visit(FunctionDefinition const& _function) { - m_functionPath.push_back(&_function); - m_modifierDepthStack.push_back(-1); - - if (_function.isConstructor()) - { - m_errorReporter.warning( - _function.location(), - "Assertion checker does not yet support constructors." - ); - return false; - } - // Not visited by a function call - if (isRootFunction()) + if (m_callStack.empty()) { m_interface->reset(); m_context.reset(); m_pathConditions.clear(); m_callStack.clear(); + pushCallStack({&_function, nullptr}); m_expressions.clear(); m_globalContext.clear(); m_uninterpretedTerms.clear(); @@ -132,20 +121,31 @@ bool SMTChecker::visit(FunctionDefinition const& _function) m_arrayAssignmentHappened = false; m_externalFunctionCallHappened = false; } - _function.parameterList().accept(*this); - if (_function.returnParameterList()) - _function.returnParameterList()->accept(*this); - visitFunctionOrModifier(); + m_modifierDepthStack.push_back(-1); + if (_function.isConstructor()) + { + m_errorReporter.warning( + _function.location(), + "Assertion checker does not yet support constructors." + ); + } + else + { + _function.parameterList().accept(*this); + if (_function.returnParameterList()) + _function.returnParameterList()->accept(*this); + visitFunctionOrModifier(); + } return false; } void SMTChecker::visitFunctionOrModifier() { - solAssert(!m_functionPath.empty(), ""); + solAssert(!m_callStack.empty(), ""); solAssert(!m_modifierDepthStack.empty(), ""); ++m_modifierDepthStack.back(); - FunctionDefinition const& function = *m_functionPath.back(); + FunctionDefinition const& function = dynamic_cast(*m_callStack.back().first); if (m_modifierDepthStack.back() == int(function.modifiers().size())) { @@ -166,7 +166,7 @@ void SMTChecker::visitFunctionOrModifier() for (auto arg: *modifierInvocation->arguments()) modifierArgsExpr.push_back(expr(*arg)); initializeFunctionCallParameters(modifierDef, modifierArgsExpr); - pushCallStack(modifierInvocation.get()); + pushCallStack({&modifierDef, modifierInvocation.get()}); modifierDef.body().accept(*this); popCallStack(); } @@ -176,8 +176,8 @@ void SMTChecker::visitFunctionOrModifier() bool SMTChecker::visit(PlaceholderStatement const&) { - solAssert(!m_functionPath.empty(), ""); - ASTNode const* lastCall = popCallStack(); + solAssert(!m_callStack.empty(), ""); + auto lastCall = popCallStack(); visitFunctionOrModifier(); pushCallStack(lastCall); return true; @@ -185,20 +185,20 @@ bool SMTChecker::visit(PlaceholderStatement const&) void SMTChecker::endVisit(FunctionDefinition const&) { + m_callStack.pop_back(); + solAssert(m_modifierDepthStack.back() == -1, ""); + m_modifierDepthStack.pop_back(); // If _function was visited from a function call we don't remove // the local variables just yet, since we might need them for // future calls. // Otherwise we remove any local variables from the context and // keep the state variables. - if (isRootFunction()) + if (m_callStack.empty()) { checkUnderOverflow(); removeLocalVariables(); solAssert(m_callStack.empty(), ""); } - m_functionPath.pop_back(); - solAssert(m_modifierDepthStack.back() == -1, ""); - m_modifierDepthStack.pop_back(); } bool SMTChecker::visit(InlineAssembly const& _inlineAsm) @@ -391,7 +391,7 @@ void SMTChecker::endVisit(Assignment const& _assignment) vector rightArguments; if (_assignment.rightHandSide().annotation().type->category() == Type::Category::Tuple) { - auto const& symbTuple = dynamic_pointer_cast(m_expressions[&_assignment.rightHandSide()]); + auto symbTuple = dynamic_pointer_cast(m_expressions[&_assignment.rightHandSide()]); solAssert(symbTuple, ""); for (auto const& component: symbTuple->components()) { @@ -666,9 +666,7 @@ void SMTChecker::endVisit(FunctionCall const& _funCall) visitGasLeft(_funCall); break; case FunctionType::Kind::Internal: - pushCallStack(&_funCall); inlineFunctionCall(_funCall); - popCallStack(); break; case FunctionType::Kind::External: case FunctionType::Kind::DelegateCall: @@ -756,10 +754,8 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall) _funCall.location(), "Assertion checker does not yet implement this type of function call." ); - return; } - - if (visitedFunction(funDef)) + else if (visitedFunction(funDef)) m_errorReporter.warning( _funCall.location(), "Assertion checker does not support recursive function calls.", @@ -783,7 +779,12 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall) funArgs.push_back(expr(*arg)); initializeFunctionCallParameters(*funDef, funArgs); + // The reason why we need to pushCallStack here instead of visit(FunctionDefinition) + // is that there we don't have `_funCall`. + pushCallStack({funDef, &_funCall}); funDef->accept(*this); + // The callstack entry is popped only in endVisit(FunctionDefinition) instead of here + // as well to avoid code duplication (not all entries are from inlined function calls). createExpr(_funCall); auto const& returnParams = funDef->returnParameters(); @@ -920,7 +921,7 @@ void SMTChecker::endVisit(Return const& _return) { if (_return.expression() && knownExpr(*_return.expression())) { - auto returnParams = m_functionPath.back()->returnParameters(); + auto returnParams = m_callStack.back().first->returnParameters(); if (returnParams.size() > 1) { auto tuple = dynamic_cast(_return.expression()); @@ -1423,7 +1424,7 @@ void SMTChecker::checkCondition( vector expressionsToEvaluate; vector expressionNames; - if (m_functionPath.size()) + if (m_callStack.size()) { solAssert(m_scanner, ""); if (_additionalValue) @@ -1491,7 +1492,7 @@ void SMTChecker::checkCondition( { std::ostringstream message; message << _description << " happens here"; - if (m_functionPath.size()) + if (m_callStack.size()) { std::ostringstream modelMessage; modelMessage << " for:\n"; @@ -1864,25 +1865,27 @@ smt::Expression SMTChecker::currentPathConditions() SecondarySourceLocation SMTChecker::currentCallStack() { SecondarySourceLocation callStackLocation; - if (m_callStack.empty()) - return callStackLocation; + solAssert(!m_callStack.empty(), ""); callStackLocation.append("Callstack: ", SourceLocation()); for (auto const& call: m_callStack | boost::adaptors::reversed) - callStackLocation.append("", call->location()); + if (call.second) + callStackLocation.append("", call.second->location()); + // The first function in the tx has no FunctionCall. + solAssert(m_callStack.front().second == nullptr, ""); return callStackLocation; } -ASTNode const* SMTChecker::popCallStack() +pair SMTChecker::popCallStack() { solAssert(!m_callStack.empty(), ""); - ASTNode const* lastCalled = m_callStack.back(); + auto lastCalled = m_callStack.back(); m_callStack.pop_back(); return lastCalled; } -void SMTChecker::pushCallStack(ASTNode const* _node) +void SMTChecker::pushCallStack(CallStackEntry _entry) { - m_callStack.push_back(_node); + m_callStack.push_back(_entry); } void SMTChecker::addPathConjoinedExpression(smt::Expression const& _e) @@ -1897,12 +1900,15 @@ void SMTChecker::addPathImpliedExpression(smt::Expression const& _e) bool SMTChecker::isRootFunction() { - return m_functionPath.size() == 1; + return m_callStack.size() == 1; } bool SMTChecker::visitedFunction(FunctionDefinition const* _funDef) { - return contains(m_functionPath, _funDef); + for (auto const& call: m_callStack) + if (call.first == _funDef) + return true; + return false; } SMTChecker::VariableIndices SMTChecker::copyVariableIndices() @@ -1950,8 +1956,11 @@ FunctionDefinition const* SMTChecker::inlinedFunctionCallToDefinition(FunctionCa set SMTChecker::touchedVariables(ASTNode const& _node) { - solAssert(!m_functionPath.empty(), ""); - return m_variableUsage.touchedVariables(_node, m_functionPath); + solAssert(!m_callStack.empty(), ""); + vector callStack; + for (auto const& call: m_callStack) + callStack.push_back(call.first); + return m_variableUsage.touchedVariables(_node, callStack); } VariableDeclaration const* SMTChecker::identifierToVariable(Expression const& _expr) diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 9d66675df..d83fc9232 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -173,6 +173,8 @@ private: std::string const& _description ); + using CallStackEntry = std::pair; + struct OverflowTarget { enum class Type { Underflow, Overflow, All } type; @@ -180,9 +182,9 @@ private: smt::Expression value; smt::Expression path; langutil::SourceLocation const& location; - std::vector callStack; + std::vector callStack; - OverflowTarget(Type _type, TypePointer _intType, smt::Expression _value, smt::Expression _path, langutil::SourceLocation const& _location, std::vector _callStack): + OverflowTarget(Type _type, TypePointer _intType, smt::Expression _value, smt::Expression _path, langutil::SourceLocation const& _location, std::vector _callStack): type(_type), intType(_intType), value(_value), @@ -266,9 +268,9 @@ private: /// Returns the current callstack. Used for models. langutil::SecondarySourceLocation currentCallStack(); /// Copies and pops the last called node. - ASTNode const* popCallStack(); - /// Adds @param _node to the callstack. - void pushCallStack(ASTNode const* _node); + CallStackEntry popCallStack(); + /// Adds (_definition, _node) to the callstack. + void pushCallStack(CallStackEntry _entry); /// Conjoin the current path conditions with the given parameter and add to the solver void addPathConjoinedExpression(smt::Expression const& _e); /// Add to the solver: the given expression implied by the current path conditions @@ -315,10 +317,8 @@ private: langutil::ErrorList m_smtErrors; std::shared_ptr m_scanner; - /// Stores the current path of function calls. - std::vector m_functionPath; - /// Stores the current call/invocation path. - std::vector m_callStack; + /// Stores the current function/modifier call/invocation path. + std::vector m_callStack; /// Returns true if the current function was not visited by /// a function call. bool isRootFunction(); diff --git a/libsolidity/formal/VariableUsage.cpp b/libsolidity/formal/VariableUsage.cpp index 9f0575072..6d63e2980 100644 --- a/libsolidity/formal/VariableUsage.cpp +++ b/libsolidity/formal/VariableUsage.cpp @@ -31,26 +31,30 @@ void VariableUsage::endVisit(Identifier const& _identifier) solAssert(declaration, ""); if (VariableDeclaration const* varDecl = dynamic_cast(declaration)) if (_identifier.annotation().lValueRequested) - m_touchedVariables.insert(varDecl); + { + solAssert(m_lastCall, ""); + if (!varDecl->isLocalVariable() || varDecl->functionOrModifierDefinition() == m_lastCall) + m_touchedVariables.insert(varDecl); + } } void VariableUsage::endVisit(FunctionCall const& _funCall) { if (auto const& funDef = SMTChecker::inlinedFunctionCallToDefinition(_funCall)) - if (find(m_functionPath.begin(), m_functionPath.end(), funDef) == m_functionPath.end()) + if (find(m_callStack.begin(), m_callStack.end(), funDef) == m_callStack.end()) funDef->accept(*this); } bool VariableUsage::visit(FunctionDefinition const& _function) { - m_functionPath.push_back(&_function); + m_callStack.push_back(&_function); return true; } void VariableUsage::endVisit(FunctionDefinition const&) { - solAssert(!m_functionPath.empty(), ""); - m_functionPath.pop_back(); + solAssert(!m_callStack.empty(), ""); + m_callStack.pop_back(); } void VariableUsage::endVisit(ModifierInvocation const& _modifierInv) @@ -62,18 +66,21 @@ void VariableUsage::endVisit(ModifierInvocation const& _modifierInv) void VariableUsage::endVisit(PlaceholderStatement const&) { - solAssert(!m_functionPath.empty(), ""); - FunctionDefinition const* function = m_functionPath.back(); - solAssert(function, ""); - if (function->isImplemented()) - function->body().accept(*this); + solAssert(!m_callStack.empty(), ""); + FunctionDefinition const* funDef = nullptr; + for (auto it = m_callStack.rbegin(); it != m_callStack.rend() && !funDef; ++it) + funDef = dynamic_cast(*it); + solAssert(funDef, ""); + if (funDef->isImplemented()) + funDef->body().accept(*this); } -set VariableUsage::touchedVariables(ASTNode const& _node, vector const& _outerCallstack) +set VariableUsage::touchedVariables(ASTNode const& _node, vector const& _outerCallstack) { m_touchedVariables.clear(); - m_functionPath.clear(); - m_functionPath += _outerCallstack; + m_callStack.clear(); + m_callStack += _outerCallstack; + m_lastCall = m_callStack.back(); _node.accept(*this); return m_touchedVariables; } diff --git a/libsolidity/formal/VariableUsage.h b/libsolidity/formal/VariableUsage.h index c824eae62..b5e067c79 100644 --- a/libsolidity/formal/VariableUsage.h +++ b/libsolidity/formal/VariableUsage.h @@ -34,7 +34,7 @@ class VariableUsage: private ASTConstVisitor { public: /// @param _outerCallstack the current callstack in the callers context. - std::set touchedVariables(ASTNode const& _node, std::vector const& _outerCallstack); + std::set touchedVariables(ASTNode const& _node, std::vector const& _outerCallstack); private: void endVisit(Identifier const& _node) override; @@ -45,7 +45,8 @@ private: void endVisit(PlaceholderStatement const& _node) override; std::set m_touchedVariables; - std::vector m_functionPath; + std::vector m_callStack; + CallableDeclaration const* m_lastCall = nullptr; }; } diff --git a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol new file mode 100644 index 000000000..cc7e50461 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol @@ -0,0 +1,96 @@ +pragma experimental SMTChecker; + +contract ContractWithFunctionCalled { + function funcCalled() external { + uint256 i = 0; + } +} + +contract ContractWithFunctionCalledSuper is ContractWithFunctionCalled { + function callWithSuper() public { + uint256 i = 0; + } +} + +contract ContractWithFunctionNotCalled { + + function funcNotCalled3() public { + + } + + function funcNotCalled2() public { + + } + + function funcNotCalled() public { + + } + + function my_func() internal returns(bool){ + return true; + } + +} + +contract ContractWithFunctionNotCalled2 is ContractWithFunctionCalledSuper { + function funcNotCalled() public { + uint256 i = 0; + address three = address(new ContractWithFunctionNotCalled()); + three.call(abi.encode(bytes4(keccak256("helloTwo()")))); + super.callWithSuper(); + ContractWithFunctionCalled c = new ContractWithFunctionCalled(); + c.funcCalled(); + } +} + +contract InternalCall { + + function() returns(uint) ptr; + + function set_test1() external{ + ptr = test1; + } + + function set_test2() external{ + ptr = test2; + } + + function test1() public returns(uint){ + return 1; + } + + function test2() public returns(uint){ + return 2; + } + + function test3() public returns(uint){ + return 3; + } + + function exec() external returns(uint){ + return ptr(); + } + +} +// ---- +// Warning: (760-815): Return value of low-level calls not used. +// Warning: (117-126): Unused local variable. +// Warning: (260-269): Unused local variable. +// Warning: (667-676): Unused local variable. +// Warning: (75-137): Function state mutability can be restricted to pure +// Warning: (218-280): Function state mutability can be restricted to pure +// Warning: (470-539): Function state mutability can be restricted to pure +// Warning: (1144-1206): Function state mutability can be restricted to pure +// Warning: (1212-1274): Function state mutability can be restricted to pure +// Warning: (1280-1342): Function state mutability can be restricted to pure +// Warning: (714-749): Internal error: Expression undefined for SMT solver. +// Warning: (799-811): Assertion checker does not yet support the type of this literal (literal_string "helloTwo()"). +// Warning: (782-813): Type conversion is not yet fully supported and might yield false positives. +// Warning: (771-814): Assertion checker does not yet implement this type of function call. +// Warning: (825-830): Assertion checker does not yet support the type of this variable. +// Warning: (887-919): Internal error: Expression undefined for SMT solver. +// Warning: (690-750): Underflow (resulting value less than 0) happens here +// Warning: (690-750): Overflow (resulting value larger than 2**160 - 1) happens here +// Warning: (1057-1068): Assertion checker does not yet implement type function () returns (uint256) +// Warning: (1120-1131): Assertion checker does not yet implement type function () returns (uint256) +// Warning: (1403-1408): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch.sol b/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch.sol new file mode 100644 index 000000000..70596bf0e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch.sol @@ -0,0 +1,20 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public pure { + if (true) { + address a = g(); + assert(a == address(0)); + } + } + function g() public pure returns (address) { + address a; + a = address(0); + return a; + } +} +// ---- +// Warning: (208-218): Type conversion is not yet fully supported and might yield false positives. +// Warning: (123-133): Type conversion is not yet fully supported and might yield false positives. +// Warning: (208-218): Type conversion is not yet fully supported and might yield false positives. diff --git a/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_2.sol b/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_2.sol new file mode 100644 index 000000000..fe49493f8 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_2.sol @@ -0,0 +1,27 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public pure { + if (true) { + address a = g(); + assert(a == address(0)); + } + else + { + address b = g(); + assert(b == address(0)); + } + } + function g() public pure returns (address) { + address a; + a = address(0); + return a; + } +} +// ---- +// Warning: (271-281): Type conversion is not yet fully supported and might yield false positives. +// Warning: (123-133): Type conversion is not yet fully supported and might yield false positives. +// Warning: (271-281): Type conversion is not yet fully supported and might yield false positives. +// Warning: (186-196): Type conversion is not yet fully supported and might yield false positives. +// Warning: (271-281): Type conversion is not yet fully supported and might yield false positives. diff --git a/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_3.sol b/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_3.sol new file mode 100644 index 000000000..9ccbbd932 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_3.sol @@ -0,0 +1,27 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public pure { + if (true) { + address a = g(); + assert(a == address(0)); + } + if (true) { + address a = g(); + assert(a == address(0)); + } + + } + function g() public pure returns (address) { + address a; + a = address(0); + return a; + } +} +// ---- +// Warning: (275-285): Type conversion is not yet fully supported and might yield false positives. +// Warning: (123-133): Type conversion is not yet fully supported and might yield false positives. +// Warning: (275-285): Type conversion is not yet fully supported and might yield false positives. +// Warning: (189-199): Type conversion is not yet fully supported and might yield false positives. +// Warning: (275-285): Type conversion is not yet fully supported and might yield false positives. diff --git a/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_4.sol b/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_4.sol new file mode 100644 index 000000000..f0b31dbe7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_4.sol @@ -0,0 +1,31 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public pure { + if (true) { + address a = g(); + assert(a == address(0)); + } + if (true) { + address a = h(); + assert(a == address(0)); + } + + } + function g() public pure returns (address) { + address a; + a = address(0); + return a; + } + function h() public pure returns (address) { + address a; + return a; + } + +} +// ---- +// Warning: (275-285): Type conversion is not yet fully supported and might yield false positives. +// Warning: (123-133): Type conversion is not yet fully supported and might yield false positives. +// Warning: (189-199): Type conversion is not yet fully supported and might yield false positives. +// Warning: (275-285): Type conversion is not yet fully supported and might yield false positives. diff --git a/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_else_branch.sol b/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_else_branch.sol new file mode 100644 index 000000000..258d95a10 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_else_branch.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public pure { + if (true) { + } else { + address a = g(); + assert(a == address(0)); + } + } + function g() public pure returns (address) { + address x; + x = address(0); + return x; + } +} +// ---- +// Warning: (219-229): Type conversion is not yet fully supported and might yield false positives. +// Warning: (134-144): Type conversion is not yet fully supported and might yield false positives. +// Warning: (219-229): Type conversion is not yet fully supported and might yield false positives. diff --git a/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_modifier_branch.sol b/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_modifier_branch.sol new file mode 100644 index 000000000..8bbc685cd --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_modifier_branch.sol @@ -0,0 +1,24 @@ +pragma experimental SMTChecker; + +contract C +{ + modifier m(address a) { + if (true) { + a = g(); + _; + assert(a == address(0)); + } + } + + function f(address a) m(a) public pure { + } + function g() public pure returns (address) { + address a; + a = address(0); + return a; + } +} +// ---- +// Warning: (249-259): Type conversion is not yet fully supported and might yield false positives. +// Warning: (118-128): Type conversion is not yet fully supported and might yield false positives. +// Warning: (249-259): Type conversion is not yet fully supported and might yield false positives. diff --git a/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_placeholder_inside_modifier_branch.sol b/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_placeholder_inside_modifier_branch.sol new file mode 100644 index 000000000..43c42c94b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/function_call_inside_placeholder_inside_modifier_branch.sol @@ -0,0 +1,25 @@ +pragma experimental SMTChecker; + +contract C +{ + modifier m { + if (true) + _; + } + + function f(address a) m public pure { + if (true) { + a = g(); + assert(a == address(0)); + } + } + function g() public pure returns (address) { + address a; + a = address(0); + return a; + } +} +// ---- +// Warning: (247-257): Type conversion is not yet fully supported and might yield false positives. +// Warning: (162-172): Type conversion is not yet fully supported and might yield false positives. +// Warning: (247-257): Type conversion is not yet fully supported and might yield false positives. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_4.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_4.sol new file mode 100644 index 000000000..c25f2f02b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_external_4.sol @@ -0,0 +1,20 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint _x) public pure returns (uint) { + return _x; + } +} + +contract D +{ + C c; + function g(uint _y) public view { + uint z = c.f(_y); + assert(z == _y); + } +} +// ---- +// Warning: (180-187): Internal error: Expression undefined for SMT solver. +// Warning: (191-206): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_inline_function_inside_branch.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_inline_function_inside_branch.sol new file mode 100644 index 000000000..7871a8a8c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_inline_function_inside_branch.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract C +{ + address owner; + modifier m { + if (true) + owner = g(); + _; + } + function f() m public { + } + function g() public pure returns (address) { + address a; + a = address(0); + return a; + } +} +// ---- +// Warning: (205-215): Type conversion is not yet fully supported and might yield false positives. +// Warning: (205-215): Type conversion is not yet fully supported and might yield false positives. diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions.sol index 903d4f91c..0ad3ed238 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions.sol @@ -22,5 +22,4 @@ contract C } } // ---- -// Warning: (86-93): Condition is always true. // Warning: (311-324): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_parameters.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_parameters.sol index 90eab0afd..35a0f399e 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_parameters.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_parameters.sol @@ -15,4 +15,3 @@ contract C } } // ---- -// Warning: (127-132): Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_return.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_return.sol index 2681b896f..78fcdc9d3 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_return.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_return.sol @@ -18,4 +18,3 @@ contract C } } // ---- -// Warning: (138-144): Condition is always false. diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_two_invocations.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_two_invocations.sol index f954cf7ca..8d79f6a89 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_two_invocations.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_two_invocations.sol @@ -17,5 +17,3 @@ contract C } } // ---- -// Warning: (137-142): Condition is always true. -// Warning: (155-164): Condition is always true.