Outputs for C loop statement generation.
This is a product type introduced by fty::defprod.
The generated (loop) statement is stmt. We may actually split it into a test and body at some point.
We also return the test and body ACL2 terms.
We return two limit terms: one for just the body, and one for the whole loop.
