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.h15
1 files changed, 4 insertions, 11 deletions
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index b57f0f96..7e7996cf 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -20,6 +20,8 @@
#include <libsolidity/formal/SolverInterface.h>
+#include <libsolidity/formal/SSAVariable.h>
+
#include <libsolidity/ast/ASTVisitor.h>
#include <libsolidity/interface/ReadFile.h>
@@ -76,7 +78,7 @@ private:
void assignment(Declaration const& _variable, smt::Expression const& _value, SourceLocation const& _location);
/// Maps a variable to an SSA index.
- using VariableSequenceCounters = std::map<Declaration const*, int>;
+ using VariableSequenceCounters = std::map<Declaration const*, SSAVariable>;
/// Visits the branch given by the statement, pushes and pops the current path conditions.
/// @param _condition if present, asserts that this condition is true within the branch.
@@ -118,7 +120,6 @@ private:
/// This fails if the type is not supported.
bool createVariable(VariableDeclaration const& _varDecl);
- static std::string uniqueSymbol(Declaration const& _decl);
static std::string uniqueSymbol(Expression const& _expr);
/// @returns true if _delc is a variable that is known at the current point, i.e.
@@ -139,18 +140,12 @@ private:
/// Resets the variable to an unknown value (in its range).
void setUnknownValue(Declaration const& decl);
- static smt::Expression minValue(IntegerType const& _t);
- static smt::Expression maxValue(IntegerType const& _t);
-
/// Returns the expression corresponding to the AST node. Throws if the expression does not exist.
smt::Expression expr(Expression const& _e);
/// Creates the expression (value can be arbitrary)
void createExpr(Expression const& _e);
/// Creates the expression and sets its value.
void defineExpr(Expression const& _e, smt::Expression _value);
- /// Returns the function declaration corresponding to the given variable.
- /// The function takes one argument which is the "sequence number".
- smt::Expression var(Declaration const& _decl);
/// Adds a new path condition
void pushPathCondition(smt::Expression const& _e);
@@ -166,10 +161,8 @@ private:
std::shared_ptr<smt::SolverInterface> m_interface;
std::shared_ptr<VariableUsage> m_variableUsage;
bool m_conditionalExecutionHappened = false;
- std::map<Declaration const*, int> m_currentSequenceCounter;
- std::map<Declaration const*, int> m_nextFreeSequenceCounter;
std::map<Expression const*, smt::Expression> m_expressions;
- std::map<Declaration const*, smt::Expression> m_variables;
+ std::map<Declaration const*, SSAVariable> m_variables;
std::vector<smt::Expression> m_pathConditions;
ErrorReporter& m_errorReporter;