		Search-engine friendly clone of the ACL2 documentation.

Exec-expr-call-or-pure

Execute a function call or a pure expression.

Signature
(exec-expr-call-or-pure e compst fenv limit) → (mv result new-compst)
Arguments: e — Guard (exprp e).; 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).

This is only used for expressions that must be either function calls or pure. If the expression is a call, we use exec-expr-call. Otherwise, we resort to exec-expr-pure, we perform an array-to-pointer conversion (which is appropriate because, in our C subset, this ACL2 function is always used where such a conversion is needed), and we peform an lvalue conversion to return a value and not an expression value (which is appropriate because, in our C subset, this ACL2 function is always used where such a conversion is needed).

We return an optional value (if there is no error), which is nil for a function that returns void.