Again some why3 fixes with regards to separators in blocks.

libsolidity/formal/Why3Translator.cpp

@@ -21,6 +21,7 @@
  */
 
 #include <libsolidity/formal/Why3Translator.h>
+#include <boost/algorithm/string/predicate.hpp>
 
 using namespace std;
 using namespace dev;
@@ -30,8 +31,7 @@ bool Why3Translator::process(SourceUnit const& _source)
 {
 	try
 	{
-		m_indentation = 0;
+		if (m_lines.size() != 1 || !m_lines.back().contents.empty())
-		if (!m_result.empty())
 			fatalError(_source, "Multiple source units not yet supported");
 		appendPreface();
 		_source.accept(*this);
@@ -43,6 +43,14 @@ bool Why3Translator::process(SourceUnit const& _source)
 	return !m_errorOccured;
 }
 
+string Why3Translator::translation() const
+{
+	string result;
+	for (auto const& line: m_lines)
+		result += string(line.indentation, '\t') + line.contents + "\n";
+	return result;
+}
+
 void Why3Translator::error(ASTNode const& _node, string const& _description)
 {
 	auto err = make_shared<Error>(Error::Type::Why3TranslatorError);
@@ -61,7 +69,7 @@ void Why3Translator::fatalError(ASTNode const& _node, string const& _description
 
 void Why3Translator::appendPreface()
 {
-	m_result += R"(
+	m_lines.push_back(Line{R"(
 module UInt256
 	use import mach.int.Unsigned
 	type uint256
@@ -70,7 +78,7 @@ module UInt256
 		type t = uint256,
 		constant max = max_uint256
 end
-)";
+)", 0});
 }
 
 string Why3Translator::toFormalType(Type const& _type) const
@@ -100,28 +108,20 @@ void Why3Translator::addLine(string const& _line)
 
 void Why3Translator::add(string const& _str)
 {
-	if (m_currentLine.empty())
+	m_lines.back().contents += _str;
-		m_indentationAtLineStart = m_indentation;
-	m_currentLine += _str;
 }
 
 void Why3Translator::newLine()
 {
-	if (!m_currentLine.empty())
+	if (!m_lines.back().contents.empty())
-	{
+		m_lines.push_back({"", m_lines.back().indentation});
-		for (size_t i = 0; i < m_indentationAtLineStart; ++i)
-			m_result.push_back('\t');
-		m_result += m_currentLine;
-		m_result.push_back('\n');
-		m_currentLine.clear();
-	}
 }
 
 void Why3Translator::unindent()
 {
 	newLine();
-	solAssert(m_indentation > 0, "");
+	solAssert(m_lines.back().indentation > 0, "");
-	m_indentation--;
+	m_lines.back().indentation--;
 }
 
 bool Why3Translator::visit(ContractDefinition const& _contract)
@@ -289,8 +289,13 @@ bool Why3Translator::visit(Block const& _node)
 	for (size_t i = 0; i < _node.statements().size(); ++i)
 	{
 		_node.statements()[i]->accept(*this);
-		if (!m_currentLine.empty() && i != _node.statements().size() - 1)
+		if (i != _node.statements().size() - 1)
-			add(";");
+		{
+			auto it = m_lines.end() - 1;
+			while (it != m_lines.begin() && it->contents.empty()) --it;
+			if (!boost::algorithm::ends_with(it->contents, "begin"))
+				it->contents += ";";
+		}
 		newLine();
 	}
 	unindent();

libsolidity/formal/Why3Translator.h

@@ -43,13 +43,13 @@ class SourceUnit;
 class Why3Translator: private ASTConstVisitor
 {
 public:
-	Why3Translator(ErrorList& _errors): m_errors(_errors) {}
+	Why3Translator(ErrorList& _errors): m_lines{{std::string(), 0}}, m_errors(_errors) {}
 
 	/// Appends formalisation of the given source unit to the output.
 	/// @returns false on error.
 	bool process(SourceUnit const& _source);
 
-	std::string translation() const { return m_result; }
+	std::string translation() const;
 
 private:
 	/// Returns an error.
@@ -64,11 +64,12 @@ private:
 	/// if the type is not supported.
 	std::string toFormalType(Type const& _type) const;
 
-	void indent() { newLine(); m_indentation++; }
+	void indent() { newLine(); m_lines.back().indentation++; }
 	void unindent();
 	void addLine(std::string const& _line);
 	void add(std::string const& _str);
 	void newLine();
+	void appendSemicolon();
 
 	virtual bool visit(SourceUnit const&) override { return true; }
 	virtual bool visit(ContractDefinition const& _contract) override;
@@ -111,9 +112,6 @@ private:
 	/// Transforms substring like `#varName` and `#stateVarName` to code that evaluates to their value.
 	std::string transformVariableReferences(std::string 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
 	/// is supported.
 	bool m_seenContract = false;
@@ -122,7 +120,12 @@ private:
 	std::vector<ASTPointer<VariableDeclaration>> const* m_stateVariables = nullptr;
 	std::map<std::string, VariableDeclaration const*> m_localVariables;
 
-	std::string m_result;
+	struct Line
+	{
+		std::string contents;
+		unsigned indentation;
+	};
+	std::vector<Line> m_lines;
 	ErrorList& m_errors;
 };