		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 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))
  (let ((__function__ 'expr-null-pointer-constp))
    (declare (ignorable __function__))
    (or (type-case type :pointer)
        (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)