		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-execution-rules

Atc-exec-expr-when-call-rules

Rules for executing function call expressions.

Definitions and Theorems

Theorem: exec-expr-when-call-value-open

(defthm exec-expr-when-call-value-open
  (implies
       (and (integerp limit)
            (>= limit
                (1+ (expr-list-pure-limit (expr-call->args expr))))
            (equal (expr-kind expr) :call)
            (expr-list-purep (expr-call->args expr))
            (equal vals
                   (exec-expr-pure-list (expr-call->args expr)
                                        compst))
            (value-listp vals)
            (equal val+compst1
                   (exec-fun (expr-call->fun expr)
                             vals compst fenv (1- limit)))
            (equal val (mv-nth 0 val+compst1))
            (equal compst1 (mv-nth 1 val+compst1))
            (valuep val))
       (equal (exec-expr expr compst fenv limit)
              (mv (expr-value val nil) compst1))))

Theorem: exec-expr-when-call-novalue-open

(defthm exec-expr-when-call-novalue-open
  (implies
       (and (integerp limit)
            (>= limit
                (1+ (expr-list-pure-limit (expr-call->args expr))))
            (equal (expr-kind expr) :call)
            (expr-list-purep (expr-call->args expr))
            (equal vals
                   (exec-expr-pure-list (expr-call->args expr)
                                        compst))
            (value-listp vals)
            (equal val+compst1
                   (exec-fun (expr-call->fun expr)
                             vals compst fenv (1- limit)))
            (equal val (mv-nth 0 val+compst1))
            (equal compst1 (mv-nth 1 val+compst1))
            (not val))
       (equal (exec-expr expr compst fenv limit)
              (mv nil compst1))))