cerc-io/solidity
16
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] Allow FunctionSort to be created via sort and not type

Browse Source
This commit is contained in:
Leonardo Alt 2019-07-03 16:16:42 +02:00
parent 3b2ebba472
commit 4aebdcc442
2 changed files with 23 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
libsolidity/formal/SymbolicVariables.cpp
View File

@ -68,6 +68,11 @@ Expression SymbolicVariable::valueAtIndex(int _index) const
return m_context.newVariable(uniqueSymbol(_index), m_sort);
}
string SymbolicVariable::nameAtIndex(int _index) const
{
return uniqueSymbol(_index);
}
string SymbolicVariable::uniqueSymbol(unsigned _index) const
{
return m_uniqueName + "_" + to_string(_index);
@ -127,6 +132,17 @@ SymbolicFunctionVariable::SymbolicFunctionVariable(
solAssert(m_type->category() == solidity::Type::Category::Function, "");
}
SymbolicFunctionVariable::SymbolicFunctionVariable(
SortPointer _sort,
string _uniqueName,
EncodingContext& _context
):
SymbolicVariable(move(_sort), move(_uniqueName), _context),
m_declaration(m_context.newVariable(currentName(), m_sort))
{
solAssert(m_sort->kind == Kind::Function, "");
}
void SymbolicFunctionVariable::resetDeclaration()
{
m_declaration = m_context.newVariable(currentName(), m_sort);

7
libsolidity/formal/SymbolicVariables.h
View File

@ -54,6 +54,7 @@ public:
Expression currentValue() const;
std::string currentName() const;
virtual Expression valueAtIndex(int _index) const;
virtual std::string nameAtIndex(int _index) const;
virtual Expression increaseIndex();
virtual Expression operator()(std::vector<Expression> /*_arguments*/) const
{
@ -63,6 +64,7 @@ public:
unsigned index() const { return m_ssa->index(); }
unsigned& index() { return m_ssa->index(); }
SortPointer const& sort() const { return m_sort; }
solidity::TypePointer const& type() const { return m_type; }
protected:
@ -139,6 +141,11 @@ public:
std::string _uniqueName,
EncodingContext& _context
);
SymbolicFunctionVariable(
SortPointer _sort,
std::string _uniqueName,
EncodingContext& _context
);
Expression increaseIndex();
Expression operator()(std::vector<Expression> _arguments) const;