		Search-engine friendly clone of the ACL2 documentation.

Pointer-operations

Value-pointer-dangling

Danling pointer for a given referenced type.

Signature
(value-pointer-dangling reftype) → ptr
Arguments: reftype — Guard (typep reftype).
Returns: ptr — Type (valuep ptr).

Definitions and Theorems

Function: value-pointer-dangling

(defun value-pointer-dangling (reftype)
  (declare (xargs :guard (typep reftype)))
  (let ((__function__ 'value-pointer-dangling))
    (declare (ignorable __function__))
    (make-value-pointer :core (pointer-dangling)
                        :reftype reftype)))

Theorem: valuep-of-value-pointer-dangling

(defthm valuep-of-value-pointer-dangling
  (b* ((ptr (value-pointer-dangling reftype)))
    (valuep ptr))
  :rule-classes :rewrite)

Theorem: value-kind-of-value-pointer-dangling

(defthm value-kind-of-value-pointer-dangling
  (b* ((?ptr (value-pointer-dangling reftype)))
    (equal (value-kind ptr) :pointer)))

Theorem: value-pointer-dangling-of-type-fix-reftype

(defthm value-pointer-dangling-of-type-fix-reftype
  (equal (value-pointer-dangling (type-fix reftype))
         (value-pointer-dangling reftype)))

Theorem: value-pointer-dangling-type-equiv-congruence-on-reftype

(defthm value-pointer-dangling-type-equiv-congruence-on-reftype
  (implies (type-equiv reftype reftype-equiv)
           (equal (value-pointer-dangling reftype)
                  (value-pointer-dangling reftype-equiv)))
  :rule-classes :congruence)