		Search-engine friendly clone of the ACL2 documentation.

Pointer-operations

Value-pointer-validp

Check if a pointer is valid, i.e. it can be dereferenced.

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

Currently this just means that the pointer is not null. However, when (as planned) we extend our model with dangling pointers, this predicate will also exclude dangling pointers.

Using `valid' for this notion is perhaps not ideal because null pointers are perfectly ``valid''values (in the sense of being legitimate values usable in correct and well-written code), even though they cannot be dereferenced. Perhaps we might change the name of this predicate in the future.

Definitions and Theorems

Function: value-pointer-validp

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

Theorem: booleanp-of-value-pointer-validp

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

Theorem: value-pointer-validp-of-value-pointer

(defthm value-pointer-validp-of-value-pointer
  (iff (value-pointer-validp (value-pointer core type))
       (pointer-case core :valid)))

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

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

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

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