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.

1 files changed, 10 insertions, 0 deletions

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();