		Search-engine friendly clone of the ACL2 documentation.

Pointer-operations

Value-pointer-danglingp

Check if a pointer is dangling.

Signature
(value-pointer-danglingp ptr) → yes/no
Arguments: ptr — Guard (valuep ptr).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: value-pointer-danglingp

(defun value-pointer-danglingp (ptr)
  (declare (xargs :guard (valuep ptr)))
  (declare (xargs :guard (value-case ptr :pointer)))
  (let ((__function__ 'value-pointer-danglingp))
    (declare (ignorable __function__))
    (pointer-case (value-pointer->core ptr)
                  :dangling)))

Theorem: booleanp-of-value-pointer-danglingp

(defthm booleanp-of-value-pointer-danglingp
  (b* ((yes/no (value-pointer-danglingp ptr)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: value-pointer-danglingp-of-value-pointer

(defthm value-pointer-danglingp-of-value-pointer
  (equal (value-pointer-danglingp (value-pointer core type))
         (pointer-case core :dangling)))

Theorem: value-pointer-danglingp-of-value-fix-ptr

(defthm value-pointer-danglingp-of-value-fix-ptr
  (equal (value-pointer-danglingp (value-fix ptr))
         (value-pointer-danglingp ptr)))

Theorem: value-pointer-danglingp-value-equiv-congruence-on-ptr

(defthm value-pointer-danglingp-value-equiv-congruence-on-ptr
  (implies (value-equiv ptr ptr-equiv)
           (equal (value-pointer-danglingp ptr)
                  (value-pointer-danglingp ptr-equiv)))
  :rule-classes :congruence)