• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
      • X86isa
        • Program-execution
        • Sdm-instruction-set-summary
        • Tlb
        • Running-linux
        • Introduction
        • Asmtest
        • X86isa-build-instructions
        • Publications
        • Contributors
        • Machine
        • Implemented-opcodes
        • To-do
        • Proof-utilities
        • Peripherals
        • Model-validation
        • Modelcalls
        • Concrete-simulation-examples
          • Fibonacci32-cosim
            • X86isa-one-fib32-cosim
            • Check-fib32-output
            • Run-x86isa-fib32
            • Make-fib32-addr-alst
              • Fib32
            • Fibonacci-cosim
            • Factorial-cosim
            • Nop-cosim
            • Datacopy-cosim
          • Utils
          • Debugging-code-proofs
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Fibonacci32-cosim

    Make-fib32-addr-alst

    Signature
    (make-fib32-addr-alst start-addr halt-addr) → *

    Definitions and Theorems

    Function: make-fib32-addr-alst

    (defun make-fib32-addr-alst (start-addr halt-addr)
      (declare (xargs :guard t))
      (let ((__function__ 'make-fib32-addr-alst))
        (declare (ignorable __function__))
        (if (or (not (integerp start-addr))
                (not (integerp halt-addr))
                (not (< start-addr halt-addr)))
            (list halt-addr)
          (cons start-addr
                (make-fib32-addr-alst (1+ start-addr)
                                      halt-addr)))))