		Search-engine friendly clone of the ACL2 documentation.

Exec-stmt

Execute a statement.

Signature
(exec-stmt s compst fenv limit) → (mv result new-compst)
Arguments: s — Guard (stmtp s).; compst — Guard (compustatep compst).; fenv — Guard (fun-envp fenv).; limit — Guard (natp limit).
Returns: result — Type (value-option-resultp result).; new-compst — Type (compustatep new-compst).

For now we only support the execution of certain statements.

We only allow, and in fact require, assignment expressions in expression statements.

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.