Check if a term may represent a read of an integer by pointer.
(atc-check-integer-read term) → (mv erp yes/no fn arg type)
Function:
(defun atc-check-integer-read (term) (declare (xargs :guard (pseudo-termp term))) (let ((__function__ 'atc-check-integer-read)) (declare (ignorable __function__)) (b* (((reterr) nil nil nil (irr-type)) ((acl2::fun (no)) (retok nil nil nil (irr-type))) ((mv okp fn args) (fty-check-fn-call term)) ((unless okp) (no)) ((mv okp fixtype read) (atc-check-symbol-2part fn)) (type (fixtype-to-integer-type fixtype)) ((unless (and okp (eq read 'read) type)) (no)) ((unless (equal (symbol-package-name fn) "C")) (reterr (msg "Invalid function ~x0 encountered: ~ it has the form of a read of an integer by pointer, ~ but it is not in the \"C\" package." fn))) ((unless (list-lenp 1 args)) (reterr (raise "Internal error: ~x0 not applied to 1 argument." fn))) (arg (first args))) (retok t fn arg type))))
Theorem:
(defthm booleanp-of-atc-check-integer-read.yes/no (b* (((mv acl2::?erp ?yes/no ?fn ?arg ?type) (atc-check-integer-read term))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atc-check-integer-read.fn (b* (((mv acl2::?erp ?yes/no ?fn ?arg ?type) (atc-check-integer-read term))) (symbolp fn)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-atc-check-integer-read.arg (b* (((mv acl2::?erp ?yes/no ?fn ?arg ?type) (atc-check-integer-read term))) (pseudo-termp arg)) :rule-classes :rewrite)
Theorem:
(defthm typep-of-atc-check-integer-read.type (b* (((mv acl2::?erp ?yes/no ?fn ?arg ?type) (atc-check-integer-read term))) (typep type)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-term-count-of-atc-check-integer-read (b* (((mv acl2::?erp ?yes/no ?fn ?arg ?type) (atc-check-integer-read term))) (implies yes/no (< (pseudo-term-count arg) (pseudo-term-count term)))) :rule-classes :linear)
Theorem:
(defthm type-nonchar-integerp-of-atc-check-integer-read (b* (((mv acl2::?erp ?yes/no ?fn ?arg ?type) (atc-check-integer-read term))) (implies yes/no (type-nonchar-integerp type))))