diff options
Diffstat (limited to 'libsolidity/formal/Why3Translator.cpp')
| -rw-r--r-- | libsolidity/formal/Why3Translator.cpp | 10 |
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(); |