• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
        • Syntax-for-tools
        • Atc
        • Language
          • Abstract-syntax
          • Integer-ranges
          • Dynamic-semantics
          • Static-semantics
          • Grammar
          • Integer-formats
          • Types
          • Portable-ascii-identifiers
          • Values
          • Integer-operations
          • Computation-states
          • Object-designators
          • Implementation-environments
          • Operations
          • Errors
          • Tag-environments
          • Function-environments
            • Init-fun-env
            • Fun-info
            • Fun-info-option
            • Fun-env-extend
            • Fun-env-result
            • Fun-env-lookup
            • Fun-info-from-fundef
            • Fun-env
          • Character-sets
          • Flexible-array-member-removal
          • Arithmetic-operations
          • Pointer-operations
          • Bytes
          • Keywords
          • Real-operations
          • Array-operations
          • Scalar-operations
          • Structure-operations
        • Representation
        • Transformation-tools
        • Pack
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Function-environments

Init-fun-env

Initialize the function environment for a translation unit.

Signature

(init-fun-env tunit) → result

Arguments

tunit — Guard (transunitp tunit).

Returns

result — Type (fun-env-resultp result).

We go though the external declarations that form the translation unit and we build the function environment for the function definitions, starting from the empty environment.

Definitions and Theorems

Function: init-fun-env-aux

(defun init-fun-env-aux (declons fenv)
  (declare (xargs :guard (and (ext-declon-listp declons)
                              (fun-envp fenv))))
  (let ((__function__ 'init-fun-env-aux))
    (declare (ignorable __function__))
    (b* (((when (endp declons))
          (fun-env-fix fenv))
         (declon (car declons)))
      (ext-declon-case declon :obj-declon
                       (init-fun-env-aux (cdr declons) fenv)
                       :fun-declon
                       (init-fun-env-aux (cdr declons) fenv)
                       :tag-declon
                       (init-fun-env-aux (cdr declons) fenv)
                       :fundef
                       (b* (((okf fenv)
                             (fun-env-extend declon.get fenv)))
                         (init-fun-env-aux (cdr declons)
                                           fenv))))))

Theorem: fun-env-resultp-of-init-fun-env-aux

(defthm fun-env-resultp-of-init-fun-env-aux
  (b* ((result (init-fun-env-aux declons fenv)))
    (fun-env-resultp result))
  :rule-classes :rewrite)

Theorem: init-fun-env-aux-of-ext-declon-list-fix-declons

(defthm init-fun-env-aux-of-ext-declon-list-fix-declons
  (equal (init-fun-env-aux (ext-declon-list-fix declons)
                           fenv)
         (init-fun-env-aux declons fenv)))

Theorem: init-fun-env-aux-ext-declon-list-equiv-congruence-on-declons

(defthm init-fun-env-aux-ext-declon-list-equiv-congruence-on-declons
  (implies (ext-declon-list-equiv declons declons-equiv)
           (equal (init-fun-env-aux declons fenv)
                  (init-fun-env-aux declons-equiv fenv)))
  :rule-classes :congruence)

Theorem: init-fun-env-aux-of-fun-env-fix-fenv

(defthm init-fun-env-aux-of-fun-env-fix-fenv
  (equal (init-fun-env-aux declons (fun-env-fix fenv))
         (init-fun-env-aux declons fenv)))

Theorem: init-fun-env-aux-fun-env-equiv-congruence-on-fenv

(defthm init-fun-env-aux-fun-env-equiv-congruence-on-fenv
  (implies (fun-env-equiv fenv fenv-equiv)
           (equal (init-fun-env-aux declons fenv)
                  (init-fun-env-aux declons fenv-equiv)))
  :rule-classes :congruence)

Function: init-fun-env

(defun init-fun-env (tunit)
  (declare (xargs :guard (transunitp tunit)))
  (let ((__function__ 'init-fun-env))
    (declare (ignorable __function__))
    (init-fun-env-aux (transunit->declons tunit)
                      nil)))

Theorem: fun-env-resultp-of-init-fun-env

(defthm fun-env-resultp-of-init-fun-env
  (b* ((result (init-fun-env tunit)))
    (fun-env-resultp result))
  :rule-classes :rewrite)

Theorem: init-fun-env-of-transunit-fix-tunit

(defthm init-fun-env-of-transunit-fix-tunit
  (equal (init-fun-env (transunit-fix tunit))
         (init-fun-env tunit)))

Theorem: init-fun-env-transunit-equiv-congruence-on-tunit

(defthm init-fun-env-transunit-equiv-congruence-on-tunit
  (implies (transunit-equiv tunit tunit-equiv)
           (equal (init-fun-env tunit)
                  (init-fun-env tunit-equiv)))
  :rule-classes :congruence)