|
|
|---|
|
|
|
|---|
Check if a function definition is safe.
(check-safe-fundef fundef funtab) → _
This ACL2 function takes as input less contextual information than its mutually recursive companions. The reason is that such contextual information is always set when a funtion definition is checked. In particular, there is no variable table to pass.
This ACL2 function does not need to return anything. Any variable table internal to the function's body does not surface outside the function's body. Also recall that the function definition itself is added to the function table prior to checking it; see add-funtypes.
To check the function definition, we construct an initial variable table
from the inputs and outputs of the function.
Note that the construction will detect and reject any duplicates.
Then we check the function's body,
ensuring that it does not end with