		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Exec-indir

Execute * on an expression value [C17:6.5.3.2/2] [C17:6.5.3.2/4].

Signature
(exec-indir arg compst) → eval
Arguments: arg — Guard (expr-valuep arg).; compst — Guard (compustatep compst).
Returns: eval — Type (expr-value-resultp eval).

First we perform array-to-pointer conversion [C17:5.3.2.1/3]. The value must be a pointer. If the pointer is not valid, it is an error. Otherwise, we read the object designated by the object designator, which is a value, and we return it as an expression value, taking the object designator from the pointer value.

Definitions and Theorems

Function: exec-indir

(defun exec-indir (arg compst)
 (declare (xargs :guard (and (expr-valuep arg)
                             (compustatep compst))))
 (let ((__function__ 'exec-indir))
  (declare (ignorable __function__))
  (b*
   ((arg (apconvert-expr-value arg))
    ((when (errorp arg)) arg)
    (val (expr-value->value arg))
    ((unless (value-case val :pointer))
     (error (list :non-pointer-dereference (expr-value-fix arg))))
    ((unless (value-pointer-validp val))
     (error
          (list :invalid-pointer-dereference (expr-value-fix arg))))
    (objdes (value-pointer->designator val))
    (*val (read-object objdes compst))
    ((when (errorp *val)) *val))
   (make-expr-value :value *val
                    :object objdes))))

Theorem: expr-value-resultp-of-exec-indir

(defthm expr-value-resultp-of-exec-indir
  (b* ((eval (exec-indir arg compst)))
    (expr-value-resultp eval))
  :rule-classes :rewrite)

Theorem: exec-indir-of-expr-value-fix-arg

(defthm exec-indir-of-expr-value-fix-arg
  (equal (exec-indir (expr-value-fix arg) compst)
         (exec-indir arg compst)))

Theorem: exec-indir-expr-value-equiv-congruence-on-arg

(defthm exec-indir-expr-value-equiv-congruence-on-arg
  (implies (expr-value-equiv arg arg-equiv)
           (equal (exec-indir arg compst)
                  (exec-indir arg-equiv compst)))
  :rule-classes :congruence)

Theorem: exec-indir-of-compustate-fix-compst

(defthm exec-indir-of-compustate-fix-compst
  (equal (exec-indir arg (compustate-fix compst))
         (exec-indir arg compst)))

Theorem: exec-indir-compustate-equiv-congruence-on-compst

(defthm exec-indir-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (exec-indir arg compst)
                  (exec-indir arg compst-equiv)))
  :rule-classes :congruence)