		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-expr-call-or-asg

Check an expression that must be a function call or an assignment.

Signature
(check-expr-call-or-asg e funtab vartab tagenv) → wf?
Arguments: e — Guard (exprp e).; funtab — Guard (fun-tablep funtab).; vartab — Guard (var-tablep vartab).; tagenv — Guard (tag-envp tagenv).
Returns: wf? — Type (wellformed-resultp wf?).

If the expression is a function call, we check it as such. We also ensure that it returns void, because we apply these checks to expressions that form expression statements: while [C17] allows function calls that discard values, we are more restrictive here for now.

If the expression is not a function call, it must be an assignment expression, which we resort to check as such.

We retun no type here, because we apply these checks to expressions that form expression statements.

Definitions and Theorems

Function: check-expr-call-or-asg

(defun check-expr-call-or-asg (e funtab vartab tagenv)
 (declare (xargs :guard (and (exprp e)
                             (fun-tablep funtab)
                             (var-tablep vartab)
                             (tag-envp tagenv))))
 (let ((__function__ 'check-expr-call-or-asg))
  (declare (ignorable __function__))
  (if
   (expr-case e :call)
   (b*
    (((okf type)
      (check-expr-call (expr-call->fun e)
                       (expr-call->args e)
                       funtab vartab tagenv))
     ((unless (type-case type :void))
      (reserrf
           (list :nonvoid-function-result-discarded (expr-fix e)))))
    :wellformed)
   (check-expr-asg e funtab vartab tagenv))))

Theorem: wellformed-resultp-of-check-expr-call-or-asg

(defthm wellformed-resultp-of-check-expr-call-or-asg
  (b* ((wf? (check-expr-call-or-asg e funtab vartab tagenv)))
    (wellformed-resultp wf?))
  :rule-classes :rewrite)

Theorem: check-expr-call-or-asg-of-expr-fix-e

(defthm check-expr-call-or-asg-of-expr-fix-e
  (equal (check-expr-call-or-asg (expr-fix e)
                                 funtab vartab tagenv)
         (check-expr-call-or-asg e funtab vartab tagenv)))

Theorem: check-expr-call-or-asg-expr-equiv-congruence-on-e

(defthm check-expr-call-or-asg-expr-equiv-congruence-on-e
 (implies
      (expr-equiv e e-equiv)
      (equal (check-expr-call-or-asg e funtab vartab tagenv)
             (check-expr-call-or-asg e-equiv funtab vartab tagenv)))
 :rule-classes :congruence)

Theorem: check-expr-call-or-asg-of-fun-table-fix-funtab

(defthm check-expr-call-or-asg-of-fun-table-fix-funtab
  (equal (check-expr-call-or-asg e (fun-table-fix funtab)
                                 vartab tagenv)
         (check-expr-call-or-asg e funtab vartab tagenv)))

Theorem: check-expr-call-or-asg-fun-table-equiv-congruence-on-funtab

(defthm check-expr-call-or-asg-fun-table-equiv-congruence-on-funtab
 (implies
      (fun-table-equiv funtab funtab-equiv)
      (equal (check-expr-call-or-asg e funtab vartab tagenv)
             (check-expr-call-or-asg e funtab-equiv vartab tagenv)))
 :rule-classes :congruence)

Theorem: check-expr-call-or-asg-of-var-table-fix-vartab

(defthm check-expr-call-or-asg-of-var-table-fix-vartab
  (equal (check-expr-call-or-asg e funtab (var-table-fix vartab)
                                 tagenv)
         (check-expr-call-or-asg e funtab vartab tagenv)))

Theorem: check-expr-call-or-asg-var-table-equiv-congruence-on-vartab

(defthm check-expr-call-or-asg-var-table-equiv-congruence-on-vartab
 (implies
      (var-table-equiv vartab vartab-equiv)
      (equal (check-expr-call-or-asg e funtab vartab tagenv)
             (check-expr-call-or-asg e funtab vartab-equiv tagenv)))
 :rule-classes :congruence)

Theorem: check-expr-call-or-asg-of-tag-env-fix-tagenv

(defthm check-expr-call-or-asg-of-tag-env-fix-tagenv
  (equal
       (check-expr-call-or-asg e funtab vartab (tag-env-fix tagenv))
       (check-expr-call-or-asg e funtab vartab tagenv)))

Theorem: check-expr-call-or-asg-tag-env-equiv-congruence-on-tagenv

(defthm check-expr-call-or-asg-tag-env-equiv-congruence-on-tagenv
 (implies
      (tag-env-equiv tagenv tagenv-equiv)
      (equal (check-expr-call-or-asg e funtab vartab tagenv)
             (check-expr-call-or-asg e funtab vartab tagenv-equiv)))
 :rule-classes :congruence)