aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/Why3Translator.h
diff options
context:
space:
mode:
authorchriseth <c@ethdev.com>2015-11-11 22:20:53 +0800
committerchriseth <c@ethdev.com>2015-11-11 22:21:01 +0800
commit34829ae7648066341dd7905e43c478ead9fbca62 (patch)
treee7143f2e5b97022c48a38776120c7a37ec44fc98 /libsolidity/formal/Why3Translator.h
parent94ea61cbb5fb8a1007438c1bfea3fc7e253f1ea6 (diff)
downloaddexon-solidity-34829ae7648066341dd7905e43c478ead9fbca62.tar.gz
dexon-solidity-34829ae7648066341dd7905e43c478ead9fbca62.tar.zst
dexon-solidity-34829ae7648066341dd7905e43c478ead9fbca62.zip
Fix problems with statement blocks.
Diffstat (limited to 'libsolidity/formal/Why3Translator.h')
-rw-r--r--libsolidity/formal/Why3Translator.h9
1 files changed, 6 insertions, 3 deletions
diff --git a/libsolidity/formal/Why3Translator.h b/libsolidity/formal/Why3Translator.h
index 21ead977..1aa46424 100644
--- a/libsolidity/formal/Why3Translator.h
+++ b/libsolidity/formal/Why3Translator.h
@@ -64,7 +64,7 @@ private:
/// if the type is not supported.
std::string toFormalType(Type const& _type) const;
- void indent() { m_indentation++; }
+ void indent() { newLine(); m_indentation++; }
void unindent();
void addLine(std::string const& _line);
void add(std::string const& _str);
@@ -74,13 +74,11 @@ private:
virtual bool visit(ContractDefinition const& _contract) override;
virtual bool visit(FunctionDefinition const& _function) override;
virtual bool visit(Block const&) override;
- virtual void endVisit(Block const&) override { unindent(); addLine("end;"); }
virtual bool visit(IfStatement const& _node) override;
virtual bool visit(WhileStatement const& _node) override;
virtual bool visit(Return const& _node) override;
virtual bool visit(VariableDeclarationStatement const& _node) override;
virtual bool visit(ExpressionStatement const&) override;
- virtual void endVisit(ExpressionStatement const&) override { add(";"); newLine(); }
virtual bool visit(Assignment const& _node) override;
virtual bool visit(TupleExpression const& _node) override;
virtual void endVisit(TupleExpression const&) override { add(")"); }
@@ -98,8 +96,13 @@ private:
return false;
}
+ /// Visits the givin statement and indents it unless it is a block
+ /// (which does its own indentation).
+ void visitIndentedUnlessBlock(Statement const& _statement);
+
void addSourceFromDocStrings(DocumentedAnnotation const& _annotation);
+ size_t m_indentationAtLineStart = 0;
size_t m_indentation = 0;
std::string m_currentLine;
/// True if we have already seen a contract. For now, only a single contract