diff options
| author | chriseth <c@ethdev.com> | 2015-11-11 22:20:53 +0800 |
|---|---|---|
| committer | chriseth <c@ethdev.com> | 2015-11-11 22:21:01 +0800 |
| commit | 34829ae7648066341dd7905e43c478ead9fbca62 (patch) | |
| tree | e7143f2e5b97022c48a38776120c7a37ec44fc98 /libsolidity/formal/Why3Translator.h | |
| parent | 94ea61cbb5fb8a1007438c1bfea3fc7e253f1ea6 (diff) | |
| download | dexon-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.h | 9 |
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 |