• 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
        • Set
        • Soft
        • C
          • Syntax-for-tools
          • Atc
          • Language
            • Abstract-syntax
            • Integer-ranges
            • Implementation-environments
            • Dynamic-semantics
            • Static-semantics
            • Grammar
            • Integer-formats
            • Types
            • Portable-ascii-identifiers
            • Values
            • Integer-operations
            • Computation-states
              • Write-object
              • Objdesign-of-var
              • Compustate-scopes-numbers
              • Create-var
              • Read-object
              • Compustate
              • Frame
                • Frame-fix
                • Frame-equiv
                • Make-frame
                • Frame->scopes
                • Frame->function
                • Change-frame
                • Framep
              • Enter-scope
              • Compustate-scopes-numbers-aux
              • Compustate-option
              • Push-frame
              • Exit-scope
              • Compustate-frames-number
              • Compustate-option-result
              • Scope-list-result
              • Pop-frame
              • Compustate-result
              • Scope-result
              • Compustate-top-frame-scopes-number
              • Top-frame
              • Heap
              • Scope
              • Scope-list
              • Frame-list
            • Object-designators
            • Operations
            • Errors
            • Tag-environments
            • Function-environments
            • Character-sets
            • Flexible-array-member-removal
            • Arithmetic-operations
            • Pointer-operations
            • Bytes
            • Keywords
            • Real-operations
            • Array-operations
            • Scalar-operations
            • Structure-operations
          • Representation
          • Transformation-tools
          • Insertion-sort
          • Pack
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Computation-states

Frame

Fixtype of frames.

This is a product type introduced by fty::defprod.

Fields
function — ident
scopes — scope-list
Additional Requirements

The following invariant is enforced on the fields:

(consp scopes)

Every time a function is called, a frame is created, which contains information about the function and its variables' values.

The variables are organized into a stack (i.e. list) of scopes, which grows leftward and shrinks rightward (i.e. scopes are added via cons and removed via cdr). There is always at least one scope, i.e. the one for the function body's block.

As defined later, the call stack is also represented as a stack (i.e. list) of frames.

Subtopics

Frame-fix
Fixing function for frame structures.
Frame-equiv
Basic equivalence relation for frame structures.
Make-frame
Basic constructor macro for frame structures.
Frame->scopes
Get the scopes field from a frame.
Frame->function
Get the function field from a frame.
Change-frame
Modifying constructor for frame structures.
Framep
Recognizer for frame structures.