		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-decl-obj

Map a declaration to an object declaration in the language definition.

Signature
(ldm-decl-obj decl) → (mv erp objdeclon)
Arguments: decl — Guard (declp decl).
Returns: objdeclon — Type (c::obj-declonp objdeclon).

The declaration must not be a static assertion declaration.

The declaration specifiers must include only type specifiers and storage class specifiers, each of which must form a supported sequence.

There must be a single initializer declarator.

Definitions and Theorems

Function: ldm-decl-obj

(defun ldm-decl-obj (decl)
 (declare (xargs :guard (declp decl)))
 (declare (xargs :guard (decl-unambp decl)))
 (let ((__function__ 'ldm-decl-obj))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     (c::obj-declon (c::scspecseq-none)
                    (c::tyspecseq-void)
                    (c::obj-declor-ident (c::ident "irrelevant"))
                    nil))
    ((when (decl-case decl :statassert))
     (reterr (msg "Unsupported static assertion declaration ~x0."
                  (decl-fix decl))))
    (extension (decl-decl->extension decl))
    (declspecs (decl-decl->specs decl))
    (initdeclors (decl-decl->init decl))
    ((when extension)
     (reterr
      (msg
       "Unsupported GCC extension keyword ~
                      for tag (i.e. structure/union/enumeration) ~
                      declaration.")))
    ((mv okp tyspecs stor-specs)
     (check-decl-spec-list-all-typespec/stoclass declspecs))
    ((unless okp)
     (reterr
      (msg
       "Unsupported declaration specifiers ~x0 ~
                      for object declaration."
       declspecs)))
    ((erp tyspecseq)
     (ldm-type-spec-list tyspecs))
    ((erp scspecseq)
     (ldm-stor-spec-list stor-specs))
    ((unless (and (consp initdeclors)
                  (endp (cdr initdeclors))))
     (reterr
      (msg
       "Unsupported number of initializer declarators ~x0 ~
                      for object declaration."
       initdeclors)))
    ((initdeclor initdeclor)
     (car initdeclors))
    ((erp objdeclor)
     (ldm-declor-obj initdeclor.declor))
    ((when initdeclor.asm?)
     (reterr
      (msg
       "Unsupported assembler name specifier ~x0 ~
                      for object declaration."
       initdeclor.asm?)))
    ((unless (endp initdeclor.attribs))
     (reterr
      (msg
       "Unsupported attribute specifiers ~x0 ~
                      for function declaration."
       initdeclor.attribs)))
    ((when (not initdeclor.init?))
     (retok (c::make-obj-declon :scspec scspecseq
                                :tyspec tyspecseq
                                :declor objdeclor
                                :init? nil)))
    ((erp init)
     (ldm-initer initdeclor.init?)))
   (retok (c::make-obj-declon :scspec scspecseq
                              :tyspec tyspecseq
                              :declor objdeclor
                              :init? init)))))

Theorem: obj-declonp-of-ldm-decl-obj.objdeclon

(defthm obj-declonp-of-ldm-decl-obj.objdeclon
  (b* (((mv acl2::?erp ?objdeclon)
        (ldm-decl-obj decl)))
    (c::obj-declonp objdeclon))
  :rule-classes :rewrite)

Theorem: ldm-decl-obj-ok-when-decl-obj-formalp

(defthm ldm-decl-obj-ok-when-decl-obj-formalp
  (implies (decl-obj-formalp decl)
           (b* (((mv acl2::?erp ?objdeclon)
                 (ldm-decl-obj decl)))
             (not erp))))

Theorem: ldm-decl-obj-ok-when-decl-block-formalp

(defthm ldm-decl-obj-ok-when-decl-block-formalp
  (implies (decl-block-formalp decl)
           (b* (((mv acl2::?erp ?objdeclon)
                 (ldm-decl-obj decl)))
             (not erp))))

Theorem: ldm-decl-obj-of-decl-fix-decl

(defthm ldm-decl-obj-of-decl-fix-decl
  (equal (ldm-decl-obj (decl-fix decl))
         (ldm-decl-obj decl)))

Theorem: ldm-decl-obj-decl-equiv-congruence-on-decl

(defthm ldm-decl-obj-decl-equiv-congruence-on-decl
  (implies (decl-equiv decl decl-equiv)
           (equal (ldm-decl-obj decl)
                  (ldm-decl-obj decl-equiv)))
  :rule-classes :congruence)