		Search-engine friendly clone of the ACL2 documentation.

Exec

Exec-function

Execution a function on some values.

Signature
(exec-function fun args cstate funenv limit) → outcome
Arguments: fun — Guard (identifierp fun).; args — Guard (value-listp args).; cstate — Guard (cstatep cstate).; funenv — Guard (funenvp funenv).; limit — Guard (natp limit).
Returns: outcome — Type (eoutcome-resultp outcome).

The code in this ACL2 function could be inlined into exec-funcall, but it seems useful to have a separate ACL2 function that takes values directly as arguments, in case we want to formally talk about function calls.

We find the function in the function environment, also obtaining the (generally smaller) function environment for executing the function. We initialize the local state with the function's inputs and outputs. We run the function body on the resulting computation state and on the function environment for executing the function. We read the final values of the function output variables and return them as result. We also restore the local state prior to the function call.

As a defensive check, we ensure that the function's body terminates regularly or via leave, not via break or continue.