		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-context-preamble-aux-aux

Signature
(atc-gen-context-preamble-aux-aux this-var-ptr typed-formals-rest) → terms
Arguments: this-var-ptr — Guard (symbolp this-var-ptr).; typed-formals-rest — Guard (atc-symbol-varinfo-alistp typed-formals-rest).
Returns: terms — Type (true-listp terms).

Definitions and Theorems

Function: atc-gen-context-preamble-aux-aux

(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: true-listp-of-atc-gen-context-preamble-aux-aux

(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)