• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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
          • X86isa-state
          • Syscalls
          • Cpuid
            • Feature-flag
            • Default-cpuid-flag-fn
            • Feature-flags
            • Linear-memory
            • Rflag-specifications
            • Characterizing-undefined-behavior
            • Top-level-memory
            • App-view
            • X86-decoder
            • Physical-memory
            • Decoding-and-spec-utils
            • Instructions
              • Two-byte-opcodes
              • One-byte-opcodes
              • Fp-opcodes
              • Instruction-semantic-functions
              • X86-illegal-instruction
              • Implemented-opcodes
              • Opcode-maps
                • Cpuid
                  • Feature-flag
                  • Default-cpuid-flag-fn
                  • Feature-flags
                  • Opcode-maps-structures
                  • Implemented-opcodes
                  • Chk-exc-fn
                  • Filtering-instructions
                  • Addressing-method-code-p
                  • Operand-type-code-p
                  • Eval-pre-map
                • X86-general-protection
                • X86-device-not-available
                • X86-step-unimplemented
                • Privileged-opcodes
                • Three-byte-opcodes
              • Register-readers-and-writers
              • X86-modes
              • Segmentation
              • Other-non-deterministic-computations
              • Environment
              • Paging
            • Implemented-opcodes
            • To-do
            • Proof-utilities
            • Peripherals
            • Model-validation
            • Modelcalls
            • Concrete-simulation-examples
            • Utils
            • Debugging-code-proofs
          • Axe
          • Execloader
        • Math
        • Testing-utilities
      • Cpuid

      Feature-flags

      Signature
      (feature-flags features) → *
      Arguments
      features — Guard (true-listp features).

      Definitions and Theorems

      Function: feature-flags

      (defun feature-flags (features)
       (declare (xargs :guard (true-listp features)))
       (declare
        (xargs :guard (subsetp-equal features *supported-feature-flags*)))
       (let ((__function__ 'feature-flags))
         (declare (ignorable __function__))
         (cond ((atom features) 1)
               ((eql (feature-flag (first features)) 0)
                0)
               (t (feature-flags (rest features))))))