aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SMTChecker.h
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal/SMTChecker.h')
-rw-r--r--libsolidity/formal/SMTChecker.h3
1 files changed, 3 insertions, 0 deletions
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index caa83764..a85933c8 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -147,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.