		Search-engine friendly clone of the ACL2 documentation.

Constant-propagation

Zero-valuep

Recognize c::values which count as zero for the purpose of

Signature
(zero-valuep value) → *
Arguments: value — Guard (c::valuep value).

Definitions and Theorems

Function: zero-valuep

(defun zero-valuep (value)
 (declare (xargs :guard (c::valuep value)))
 (declare (xargs :type-prescription (booleanp (zero-valuep value))))
 (let ((__function__ 'zero-valuep))
   (declare (ignorable __function__))
   (c::value-case value
                  :uchar (int= value.get 0)
                  :schar (int= value.get 0)
                  :ushort (int= value.get 0)
                  :sshort (int= value.get 0)
                  :uint (int= value.get 0)
                  :sint (int= value.get 0)
                  :ulong (int= value.get 0)
                  :slong (int= value.get 0)
                  :ullong (int= value.get 0)
                  :sllong (int= value.get 0)
                  :pointer (c::pointer-case value.core
                                            :null t
                                            :dangling nil
                                            :valid nil)
                  :array nil
                  :struct nil)))