cerc-io/solidity
11
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

Add variable type to smt unique name

Browse Source
This commit is contained in:
Leo Alt 2022-06-22 16:12:38 +02:00
parent 02fdcb3623
commit a3c386191e
3 changed files with 31 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
libsolidity/ast/AST.cpp
View File

@ -685,6 +685,23 @@ bool VariableDeclaration::isLocalOrReturn() const
return isReturnParameter() || (isLocalVariable() && !isCallableOrCatchParameter());
}
bool VariableDeclaration::isInputParameter() const
{
vector<ASTPointer<VariableDeclaration>> const* parameters = nullptr;
if (auto const* funTypeName = dynamic_cast<FunctionTypeName const*>(scope()))
parameters = &funTypeName->parameterTypes();
else if (auto const* callable = dynamic_cast<CallableDeclaration const*>(scope()))
parameters = &callable->parameters();
if (parameters)
for (auto const& variable: *parameters)
if (variable.get() == this)
return true;
return false;
}
bool VariableDeclaration::isReturnParameter() const
{
vector<ASTPointer<VariableDeclaration>> const* returnParameters = nullptr;

1
libsolidity/ast/AST.h
View File

@ -1052,6 +1052,7 @@ public:
bool isCallableOrCatchParameter() const;
/// @returns true if this variable is a return parameter of a function.
bool isReturnParameter() const;
bool isInputParameter() const;
/// @returns true if this variable is a parameter of the success or failure clausse
/// of a try/catch statement.
bool isTryCatchParameter() const;

14
libsolidity/formal/EncodingContext.cpp
View File

@ -61,7 +61,19 @@ bool EncodingContext::createVariable(frontend::VariableDeclaration const& _varDe
{
solAssert(!knownVariable(_varDecl), "");
auto const& type = _varDecl.type();
auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *this);
unsigned varType;
if (_varDecl.isStateVariable())
varType = 0;
else if (_varDecl.isInputParameter())
varType = 1;
else if (_varDecl.isReturnParameter())
varType = 2;
else
{
solAssert(_varDecl.isLocalVariable());
varType = 3;
}
auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()) + "_" + to_string(varType), *this);
m_variables.emplace(&_varDecl, result.second);
return result.first;
}