Exec-stmt-dowhile
Execute a do-while statement.
- Signature
(exec-stmt-dowhile body test compst fenv limit)
→
(mv sval new-compst)
- Arguments
- body — Guard (stmtp body).
- test — Guard (exprp test).
- compst — Guard (compustatep compst).
- fenv — Guard (fun-envp fenv).
- limit — Guard (natp limit).
- Returns
- sval — Type (stmt-value-resultp sval).
- new-compst — Type (compustatep new-compst).
First, we execute the body,
pushing and then popping a scope,
because the body forms a block [C17:6.8.5/5].
If the body terminates with a return,
we end the execution of the loop with the same result.
Otherwise, we execute the test.
If it yields a 0 scalar, the loop terminates execution,
with a statement value indicating non-return termination.
Otherwise, we re-execute the loop,
by calling this ACL2 function recursively.
