• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • 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
              • Get-prefixes
              • Vex-0f3a-execute
              • Vex-0f38-execute
              • Vex-0f-execute
              • Two-byte-opcode-execute
              • Second-three-byte-opcode-execute
              • One-byte-opcode-execute
              • First-three-byte-opcode-execute
              • Evex-0f3a-execute
              • Evex-0f38-execute
              • Evex-0f-execute
              • X86-fetch-decode-execute
              • Vex-decode-and-execute
              • Evex-decode-and-execute
              • X86-run
              • Implemented-opcodes
              • Three-byte-opcode-decode-and-execute
              • X86-run-halt-count
              • Two-byte-opcode-decode-and-execute
              • X86-run-steps
              • 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-run-halt
                • X86-fetch-decode-execute-halt
                • X86-run-steps1
              • Physical-memory
              • Decoding-and-spec-utils
              • Instructions
              • 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
          • Svl
          • Rtl
        • Software-verification
        • 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))))))