		Search-engine friendly clone of the ACL2 documentation.

Exec-stmt

Execute a statement.

Signature
(exec-stmt s compst fenv limit) → (mv sval new-compst)
Arguments: s — Guard (stmtp s).; 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).

For now we only support the execution of certain statements.

Since an expression statement discards the value returned by the expression (if any), there is no need to perform array-to-pointer conversion [C23:6.3.3.1]. The fact that array-to-pointer conversion may return an error is just an artifact of our current model, which we plan to eliminate.

For a compound statement (i.e. a block), we enter a new (empty) scope prior to executing the block items, and we exit that scope after executing the block items.

An iteration statement forms a block [C17:6.8.5/5], so we must enter a new scope before it and exit the scope after it. We are currently not doing that for while loops, but we plan to do that; at the moment it does not make a difference, given how we use the dynamic semantics.