From 4524ad08701939cc22d28494c57dda1cdfba9e10 Mon Sep 17 00:00:00 2001
From: Rhett Aultman <roadriverrail@gmail.com>
Date: Sat, 30 Jul 2016 00:13:05 -0700
Subject: Add support for do/while loops

This commit adds support for a standard do <statement> while <expr>;
form of statement.  While loops were already being supported; supporting
a do/while loop mostly involves reusing code from while loops but putting
the conditional checking last.
---
 libsolidity/formal/Why3Translator.cpp | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'libsolidity/formal')

diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp
index 813fa3ab..5934d593 100644
--- a/libsolidity/formal/Why3Translator.cpp
+++ b/libsolidity/formal/Why3Translator.cpp
@@ -410,6 +410,16 @@ bool Why3Translator::visit(WhileStatement const& _node)
 {
 	addSourceFromDocStrings(_node.annotation());
 
+	// Why3 does not appear to support do-while loops,
+	// so we will simulate them by performing a while
+	// loop with the body prepended once.
+
+	if (_node.isDoWhile())
+	{
+		visitIndentedUnlessBlock(_node.body());
+		newLine();
+	}
+
 	add("while ");
 	_node.condition().accept(*this);
 	newLine();
-- 
cgit v1.2.3