Exec-stmt-while
Execute a while statement.
- Signature
(exec-stmt-while test body compst fenv limit)
→
(mv sval new-compst)
- Arguments
- test — Guard (exprp test).
- body — Guard (stmtp body).
- 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 test.
If it yields a 0 scalar, we return a nil value result,
because it means that the loop completes,
and execution can proceed with any code after the loop.
Otherwise, we recursively execute the body.
We should push and then pop a scope,
because the body of a loop forms a block [C17:6.8.5/5];
we plan to do that, but currently that makes no difference
given how we are using our dynamic semantics of C.
If the body terminates with a return,
we terminate the loop with the same result.
If the body does not terminate with a return,
we re-execute the loop,
by calling this ACL2 function recursively.
