		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-omap-update-formals

Generate a term that is an omap::update nest for the formals of a function.

Signature
(atc-gen-omap-update-formals typed-formals) → (mv term init-formals)
Arguments: typed-formals — Guard (atc-symbol-varinfo-alistp typed-formals).
Returns: term — An untranslated term.; init-formals — Type (symbol-listp init-formals), given (atc-symbol-varinfo-alistp typed-formals).

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

(omap::update (ident <string>) <symbol> (omap::update ... nil) ...)

where <string> is the string for the name of the C formal and <symbol> is the symbol that is either the corresponding ACL2 formal or the corresponding ACL2 formal with the -ptr suffix. The latter is for formals of pointer or array type: as explained in atc-gen-context-preamble, the C values are represented by ACL2 variables of the form x-ptr: these are the values that go into the initial scope, not the deferenced objects.

However, formals that represent external objects are skipped. This is because in C these are not function parameters.

We also return the list of the <symbol>s, some of which are the formals, while the others are the formals suffixed by -ptr. See explanation just above.

Definitions and Theorems

Function: atc-gen-omap-update-formals

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

Theorem: symbol-listp-of-atc-gen-omap-update-formals.init-formals

(defthm symbol-listp-of-atc-gen-omap-update-formals.init-formals
  (implies (atc-symbol-varinfo-alistp typed-formals)
           (b* (((mv ?term ?init-formals)
                 (atc-gen-omap-update-formals typed-formals)))
             (symbol-listp init-formals)))
  :rule-classes :rewrite)