		Search-engine friendly clone of the ACL2 documentation.

Evaluation

Exec-call

Execute a call of a function on a list of arguments.

Signature
(exec-call function arguments program) → outcome
Arguments: function — Guard (symbol-valuep function).; arguments — Guard (value-listp arguments).; program — Guard (programp program).
Returns: outcome — Type (exec-outcome-p outcome).

We create an initial state with the function (symbol) and the arguments, and we attempt to exhaustively perform execution steps. We return the execution outcome.

This function is not executable.

Definitions and Theorems

Function: exec-call

(defun exec-call (function arguments program)
  (declare (xargs :guard (and (symbol-valuep function)
                              (value-listp arguments)
                              (programp program))))
  (let ((__function__ 'exec-call))
    (declare (ignorable __function__))
    (b* ((start-estate (eval-state-init function arguments)))
      (step* start-estate program))))

Theorem: exec-outcome-p-of-exec-call

(defthm exec-outcome-p-of-exec-call
  (b* ((outcome (exec-call function arguments program)))
    (exec-outcome-p outcome))
  :rule-classes :rewrite)