		Search-engine friendly clone of the ACL2 documentation.

Term-checkers-atc

Atc-check-integer-write

Check if a term may represent a write of an integer by pointer.

Signature
(atc-check-integer-write val) → (mv erp yes/no fn arg type)
Arguments: val — Guard (pseudo-termp val).
Returns: yes/no — Type (booleanp yes/no).; fn — Type (symbolp fn).; arg — Type (pseudo-termp arg).; type — Type (typep type).

A write of an integer by pointer is represented by a let of the form

(let ((<var> (<type>-write <int>))) ...)

where <var> is a variable of pointer-to-integer type and <int> is a term that yields the integer to write.

This ACL2 function takes as argument the value term of the let, i.e. (<type>-write <int>), and checks if it has the expected form, returning, if successful, the function <type>-write, the argument <int>, and the integer type.

Definitions and Theorems

Function: atc-check-integer-write

(defun atc-check-integer-write (val)
 (declare (xargs :guard (pseudo-termp val)))
 (let ((__function__ 'atc-check-integer-write))
  (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 val))
    ((unless okp) (no))
    ((mv okp fixtype write)
     (atc-check-symbol-2part fn))
    (type (fixtype-to-integer-type fixtype))
    ((unless (and okp (eq write 'write) type))
     (no))
    ((unless (equal (symbol-package-name fn) "C"))
     (reterr
      (msg
       "Invalid function ~x0 encountered: ~
                      it has the form of a write 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: booleanp-of-atc-check-integer-write.yes/no

(defthm booleanp-of-atc-check-integer-write.yes/no
  (b* (((mv acl2::?erp ?yes/no ?fn ?arg ?type)
        (atc-check-integer-write val)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-integer-write.fn

(defthm symbolp-of-atc-check-integer-write.fn
  (b* (((mv acl2::?erp ?yes/no ?fn ?arg ?type)
        (atc-check-integer-write val)))
    (symbolp fn))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-check-integer-write.arg

(defthm pseudo-termp-of-atc-check-integer-write.arg
  (b* (((mv acl2::?erp ?yes/no ?fn ?arg ?type)
        (atc-check-integer-write val)))
    (pseudo-termp arg))
  :rule-classes :rewrite)

Theorem: typep-of-atc-check-integer-write.type

(defthm typep-of-atc-check-integer-write.type
  (b* (((mv acl2::?erp ?yes/no ?fn ?arg ?type)
        (atc-check-integer-write val)))
    (typep type))
  :rule-classes :rewrite)

Theorem: pseudo-term-count-of-atc-check-integer-write

(defthm pseudo-term-count-of-atc-check-integer-write
  (b* (((mv acl2::?erp ?yes/no ?fn ?arg ?type)
        (atc-check-integer-write val)))
    (implies yes/no
             (< (pseudo-term-count arg)
                (pseudo-term-count val))))
  :rule-classes :linear)

Theorem: type-nonchar-integerp-of-atc-check-integer-write

(defthm type-nonchar-integerp-of-atc-check-integer-write
  (b* (((mv acl2::?erp ?yes/no ?fn ?arg ?type)
        (atc-check-integer-write val)))
    (implies yes/no (type-nonchar-integerp type))))