cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

[SMTChecker] Add note about not inlining external function calls

Browse Source
This commit is contained in:
Leonardo Alt 2019-04-17 16:14:07 +02:00
parent 4509e8efbb
commit 03d18f1b98
2 changed files with 9 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
libsolidity/formal/SMTChecker.cpp
View File

@ -121,6 +121,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
initializeLocalVariables(_function); initializeLocalVariables(_function);
m_loopExecutionHappened = false; m_loopExecutionHappened = false;
m_arrayAssignmentHappened = false; m_arrayAssignmentHappened = false;
m_externalFunctionCallHappened = false;
} }
_function.parameterList().accept(*this); _function.parameterList().accept(*this);
if (_function.returnParameterList()) if (_function.returnParameterList())
@ -607,6 +608,7 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
popCallStack(); popCallStack();
break; break;
case FunctionType::Kind::External: case FunctionType::Kind::External:
m_externalFunctionCallHappened = true;
resetStateVariables(); resetStateVariables();
resetStorageReferences(); resetStorageReferences();
break; break;
@ -1295,6 +1297,12 @@ void SMTChecker::checkCondition(
" therefore all mapping information is erased after" " therefore all mapping information is erased after"
" a mapping local variable/parameter is assigned.\n" " a mapping local variable/parameter is assigned.\n"
"You can re-introduce information using require()."; "You can re-introduce information using require().";
if (m_externalFunctionCallHappened)
extraComment +=
"\nNote that external function calls are not inlined,"
" even if the source code of the function is available."
" This is due to the possibility that the actual called contract"
" has the same ABI but implements the function differently.";
SecondarySourceLocation secondaryLocation{}; SecondarySourceLocation secondaryLocation{};
secondaryLocation.append(extraComment, SourceLocation{}); secondaryLocation.append(extraComment, SourceLocation{});

1
libsolidity/formal/SMTChecker.h
View File

@ -277,6 +277,7 @@ private:
VariableUsage m_variableUsage; VariableUsage m_variableUsage;
bool m_loopExecutionHappened = false; bool m_loopExecutionHappened = false;
bool m_arrayAssignmentHappened = false; bool m_arrayAssignmentHappened = false;
bool m_externalFunctionCallHappened = false;
// True if the "No SMT solver available" warning was already created. // True if the "No SMT solver available" warning was already created.
bool m_noSolverWarning = false; bool m_noSolverWarning = false;
/// An Expression may have multiple smt::Expression due to /// An Expression may have multiple smt::Expression due to