Exec-address
Execute & on an expression value [C17:6.5.3.2/1] [C17:6.5.3.2/3].
- Signature
(exec-address arg) → eval
- Arguments
- arg — Guard (expr-valuep arg).
- Returns
- eval — Type (expr-value-resultp eval).
The expression that the operator & is applied to
must be an lvalue [C17:6.5.3.2/1],
which in our formalization means that
we apply this operator to an expression value (returned by the lvalue).
The expression value must contain an object designator,
because otherwise the argument expression was not an lvalue.
We extract the object designator and we return a pointer value,
whose type is determined by the value in the expression value.
We return the value as an expression value without object designator,
for uniformity with other ACL2 functions for expression execution.
Here we formalize the actual application of &
to the expression value returned by an expression.
We do not formalize here the fact that &*E is the same as E
in the sense in that case neither * nor & are evaluated
[C17:6.5.3.2/4], whether the * is explicit or implied by [];
we formalize that elsewhere,
while here we assume that the argument expression of &
has been evaluated (because the special cases above do not hold),
and the resulting expression value is passed here.
We perform no array-to-pointer conversion,
because that conversion is not performed for the operand of &
[C17:6.3.2.1/3].
Definitions and Theorems
Function: exec-address
(defun exec-address (arg)
(declare (xargs :guard (expr-valuep arg)))
(let ((__function__ 'exec-address))
(declare (ignorable __function__))
(b* ((objdes (expr-value->object arg))
((unless objdes)
(error (list :not-lvalue-result (expr-value-fix arg))))
(type (type-of-value (expr-value->value arg))))
(make-expr-value
:value (make-value-pointer :core (pointer-valid objdes)
:reftype type)
:object nil))))
Theorem: expr-value-resultp-of-exec-address
(defthm expr-value-resultp-of-exec-address
(b* ((eval (exec-address arg)))
(expr-value-resultp eval))
:rule-classes :rewrite)
Theorem: exec-address-of-expr-value-fix-arg
(defthm exec-address-of-expr-value-fix-arg
(equal (exec-address (expr-value-fix arg))
(exec-address arg)))
Theorem: exec-address-expr-value-equiv-congruence-on-arg
(defthm exec-address-expr-value-equiv-congruence-on-arg
(implies (expr-value-equiv arg arg-equiv)
(equal (exec-address arg)
(exec-address arg-equiv)))
:rule-classes :congruence)
