(atc-gen-context-preamble-aux-aux this-var-ptr typed-formals-rest) → terms
Function:
(defun atc-gen-context-preamble-aux-aux (this-var-ptr typed-formals-rest) (declare (xargs :guard (and (symbolp this-var-ptr) (atc-symbol-varinfo-alistp typed-formals-rest)))) (let ((__function__ 'atc-gen-context-preamble-aux-aux)) (declare (ignorable __function__)) (b* (((when (endp typed-formals-rest)) nil) ((cons other-var other-info) (car typed-formals-rest))) (if (and (member-equal (type-kind (atc-var-info->type other-info)) '(:pointer :array)) (not (atc-var-info->externalp other-info))) (cons (cons 'object-disjointp (cons (cons 'value-pointer->designator (cons this-var-ptr 'nil)) (cons (cons 'value-pointer->designator (cons (add-suffix-to-fn other-var "-PTR") 'nil)) 'nil))) (atc-gen-context-preamble-aux-aux this-var-ptr (cdr typed-formals-rest))) (atc-gen-context-preamble-aux-aux this-var-ptr (cdr typed-formals-rest))))))
Theorem:
(defthm true-listp-of-atc-gen-context-preamble-aux-aux (b* ((terms (atc-gen-context-preamble-aux-aux this-var-ptr typed-formals-rest))) (true-listp terms)) :rule-classes :rewrite)