The reason for this is to allow one to write the statement foo(...); with a semicolon afterward; if one did instead define foo(...) {...} then the semicolon would have the wrong semantics.
It might be easy and useful to recognize this pattern in Floyd and automatically do a program transformation (perhaps using our Hoare-logic inversion rules) to convert do {S} while (0) into simply S. One problem with that approach is that break and continue within S would have the wrong semantics, so it would only work for statements that don't (syntactically) contain any break or continue.
Perhaps it's worth investigating whether this is easy or hard.
Thanks to @roconnor-blockstream for pointing out this pain point.
A standard idiom in C macros is,
The reason for this is to allow one to write the statement
foo(...);with a semicolon afterward; if one did insteaddefine foo(...) {...}then the semicolon would have the wrong semantics.It might be easy and useful to recognize this pattern in Floyd and automatically do a program transformation (perhaps using our Hoare-logic inversion rules) to convert
do {S} while (0)into simply S. One problem with that approach is thatbreakandcontinuewithin S would have the wrong semantics, so it would only work for statements that don't (syntactically) contain any break or continue.Perhaps it's worth investigating whether this is easy or hard.
Thanks to @roconnor-blockstream for pointing out this pain point.