		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-add-var-formals

Generate a term that is an add-var nest for the formals of a function.

Signature
(atc-gen-add-var-formals fn typed-formals compst-var) → term
Arguments: fn — Guard (symbolp fn).; typed-formals — Guard (atc-symbol-varinfo-alistp typed-formals).; compst-var — Guard (symbolp compst-var).
Returns: term — An untranslated term.

This is used in the generated theorem that describes the initial computation state for a function execution. It has the form

(add-var  (ident <string>)
          <symbol>
          (add-var ... (add-frame (ident <fn>) compst)...))

where <string> is the string for the name of the C formal, <symbol> is the symbol that is either the corresponding ACL2 formal or the corresponding ACL2 formal with the -ptr suffix (according to the criterion in atc-gen-omap-update-formals), and the nest ends with (add-frame (ident <fn>) compst), where <fn> is the string for the function name.

Definitions and Theorems

Function: atc-gen-add-var-formals

(defun atc-gen-add-var-formals (fn typed-formals compst-var)
 (declare
      (xargs :guard (and (symbolp fn)
                         (atc-symbol-varinfo-alistp typed-formals)
                         (symbolp compst-var))))
 (let ((__function__ 'atc-gen-add-var-formals))
  (declare (ignorable __function__))
  (b* (((when (endp typed-formals))
        (cons 'add-frame
              (cons (cons 'ident
                          (cons (symbol-name fn) 'nil))
                    (cons compst-var 'nil))))
       ((cons var info) (car typed-formals))
       (type (atc-var-info->type info))
       (externalp (atc-var-info->externalp info))
       (add-var-rest (atc-gen-add-var-formals fn (cdr typed-formals)
                                              compst-var))
       (var/varptr (if (or (type-case type :pointer)
                           (type-case type :array))
                       (add-suffix-to-fn var "-PTR")
                     var)))
    (if externalp add-var-rest
      (cons 'add-var
            (cons (cons 'ident
                        (cons (symbol-name var) 'nil))
                  (cons var/varptr
                        (cons add-var-rest 'nil))))))))