Exec-expr-call
Execution a function call.
- Signature
(exec-expr-call fun args compst fenv limit)
→
(mv result new-compst)
- Arguments
- fun — Guard (identp fun).
- args — Guard (expr-listp args).
- 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).
We return an optional value,
which is nil for a function that returns void.
