diff options
Diffstat (limited to 'libsolidity/formal/SMTChecker.h')
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index f14d2ac0..a85933c8 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -86,6 +86,7 @@ private: void visitAssert(FunctionCall const& _funCall); void visitRequire(FunctionCall const& _funCall); void visitGasLeft(FunctionCall const& _funCall); + void visitTypeConversion(FunctionCall const& _funCall); /// Visits the FunctionDefinition of the called function /// if available and inlines the return value. void inlineFunctionCall(FunctionCall const& _funCall); @@ -146,8 +147,11 @@ private: void initializeLocalVariables(FunctionDefinition const& _function); void initializeFunctionCallParameters(FunctionDefinition const& _function, std::vector<smt::Expression> const& _callArgs); + void resetVariable(VariableDeclaration const& _variable); void resetStateVariables(); + void resetStorageReferences(); void resetVariables(std::vector<VariableDeclaration const*> _variables); + void resetVariables(std::function<bool(VariableDeclaration const&)> const& _filter); /// Given two different branches and the touched variables, /// merge the touched variables into after-branch ite variables /// using the branch condition as guard. |