		Search-engine friendly clone of the ACL2 documentation.

Validation-information

Const-expr-null-pointer-constp

Check whether a constant expression of a given type is potentially a null pointer constant [C17:6.3.2.3/3].

Signature
(const-expr-null-pointer-constp const-expr type) → yes/no
Arguments: const-expr — Guard (const-exprp const-expr).; type — Guard (typep type).
Returns: yes/no — Type (booleanp yes/no).

See expr-null-pointer-constp.

Definitions and Theorems

Function: const-expr-null-pointer-constp

(defun const-expr-null-pointer-constp (const-expr type)
  (declare (xargs :guard (and (const-exprp const-expr)
                              (typep type))))
  (b* (((const-expr const-expr) const-expr))
    (expr-null-pointer-constp const-expr.expr type)))

Theorem: booleanp-of-const-expr-null-pointer-constp

(defthm booleanp-of-const-expr-null-pointer-constp
  (b* ((yes/no (const-expr-null-pointer-constp const-expr type)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: const-expr-null-pointer-constp-of-const-expr-fix-const-expr

(defthm const-expr-null-pointer-constp-of-const-expr-fix-const-expr
  (equal (const-expr-null-pointer-constp (const-expr-fix const-expr)
                                         type)
         (const-expr-null-pointer-constp const-expr type)))

Theorem: const-expr-null-pointer-constp-const-expr-equiv-congruence-on-const-expr

(defthm
 const-expr-null-pointer-constp-const-expr-equiv-congruence-on-const-expr
 (implies
     (const-expr-equiv const-expr const-expr-equiv)
     (equal (const-expr-null-pointer-constp const-expr type)
            (const-expr-null-pointer-constp const-expr-equiv type)))
 :rule-classes :congruence)

Theorem: const-expr-null-pointer-constp-of-type-fix-type

(defthm const-expr-null-pointer-constp-of-type-fix-type
  (equal (const-expr-null-pointer-constp const-expr (type-fix type))
         (const-expr-null-pointer-constp const-expr type)))

Theorem: const-expr-null-pointer-constp-type-equiv-congruence-on-type

(defthm const-expr-null-pointer-constp-type-equiv-congruence-on-type
 (implies
     (type-equiv type type-equiv)
     (equal (const-expr-null-pointer-constp const-expr type)
            (const-expr-null-pointer-constp const-expr type-equiv)))
 :rule-classes :congruence)