		Search-engine friendly clone of the ACL2 documentation.

Validation-information

Expr-null-pointer-constp

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

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

Due to the approximate representation of types and our lack of constant expression evaluation, this recognizer is highly overappoximating. It will recognize any unknown, void/unknown pointer, or integer type.

Definitions and Theorems

Function: expr-null-pointer-constp

(defun expr-null-pointer-constp (expr type)
  (declare (xargs :guard (and (exprp expr) (typep type))))
  (declare (ignore expr))
  (type-case type
             :unknown t
             :pointer (or (type-case type.to :void)
                          (type-case type.to :unknown))
             :otherwise (type-integerp type)))

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

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

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

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

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

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

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

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

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

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