aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal
diff options
context:
space:
mode:
authorchriseth <chris@ethereum.org>2017-10-05 03:45:45 +0800
committerAlex Beregszaszi <alex@rtfs.hu>2017-11-22 10:35:34 +0800
commit19d5c424295df9638b32a657b31463abac9eb000 (patch)
tree49ef9a5d5971bf60d675c4a850ec31b2bc09af70 /libsolidity/formal
parent5e2c066778c2018b5ee627585c917dd2c92ae848 (diff)
downloaddexon-solidity-19d5c424295df9638b32a657b31463abac9eb000.tar.gz
dexon-solidity-19d5c424295df9638b32a657b31463abac9eb000.tar.zst
dexon-solidity-19d5c424295df9638b32a657b31463abac9eb000.zip
For loop.
Diffstat (limited to 'libsolidity/formal')
-rw-r--r--libsolidity/formal/SMTChecker.cpp42
-rw-r--r--libsolidity/formal/SMTChecker.h1
2 files changed, 43 insertions, 0 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 3ad9db92..6c4662ac 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -126,6 +126,48 @@ bool SMTChecker::visit(WhileStatement const& _node)
return false;
}
+bool SMTChecker::visit(ForStatement const& _node)
+{
+ if (_node.initializationExpression())
+ _node.initializationExpression()->accept(*this);
+
+ // Do not reset the init expression part.
+ auto touchedVariables =
+ m_variableUsage->touchedVariables(_node.body());
+ if (_node.condition())
+ touchedVariables += m_variableUsage->touchedVariables(*_node.condition());
+ if (_node.loopExpression())
+ touchedVariables += m_variableUsage->touchedVariables(*_node.loopExpression());
+ // Remove duplicates
+ std::sort(touchedVariables.begin(), touchedVariables.end());
+ touchedVariables.erase(std::unique(touchedVariables.begin(), touchedVariables.end()), touchedVariables.end());
+
+ resetVariables(touchedVariables);
+
+ if (_node.condition())
+ {
+ _node.condition()->accept(*this);
+ checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE.");
+ }
+
+ VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter;
+ m_interface->push();
+ if (_node.condition())
+ m_interface->addAssertion(expr(*_node.condition()));
+ _node.body().accept(*this);
+ if (_node.loopExpression())
+ _node.loopExpression()->accept(*this);
+
+ m_interface->pop();
+
+ m_conditionalExecutionHappened = true;
+ m_currentSequenceCounter = sequenceCountersStart;
+
+ resetVariables(touchedVariables);
+
+ return false;
+}
+
void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
{
if (_varDecl.declarations().size() != 1)
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 85a37f2c..54e3b22a 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -52,6 +52,7 @@ private:
virtual void endVisit(FunctionDefinition const& _node) override;
virtual bool visit(IfStatement const& _node) override;
virtual bool visit(WhileStatement const& _node) override;
+ virtual bool visit(ForStatement const& _node) override;
virtual void endVisit(VariableDeclarationStatement const& _node) override;
virtual void endVisit(ExpressionStatement const& _node) override;
virtual void endVisit(Assignment const& _node) override;