		Search-engine friendly clone of the ACL2 documentation.

Pointer

Pointer-fix

Fixer for pointer.

Signature
(pointer-fix x) → fixed-x
Arguments: x — Guard (pointerp x).
Returns: fixed-x — Type (pointerp fixed-x).

Definitions and Theorems

Function: pointer-fix

(defun pointer-fix (x)
  (declare (xargs :guard (pointerp x)))
  (mbe :logic
       (if (pointerp x)
           x
         (new-pointer-raw nil))
       :exec x))

Theorem: pointerp-of-pointer-fix

(defthm pointerp-of-pointer-fix
  (b* ((fixed-x (pointer-fix x)))
    (pointerp fixed-x))
  :rule-classes :rewrite)

Theorem: pointer-fix-when-pointerp

(defthm pointer-fix-when-pointerp
  (implies (pointerp x)
           (equal (pointer-fix x) x)))