• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • 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
          • Sha-2
          • Yul
          • Zcash
          • Proof-checker-itp13
          • Regex
          • ACL2-programming-language
          • Json
          • Jfkr
          • Equational
          • Cryptography
          • Poseidon
          • Where-do-i-place-my-book
          • Axe
          • Bigmems
          • Builtins
          • Execloader
          • Aleo
          • Solidity
          • Paco
          • Concurrent-programs
          • Bls12-377-curves
        • Debugging
        • Std
        • Proof-automation
        • Macro-libraries
        • ACL2
        • Interfacing-tools
        • Hardware-verification
        • 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))))))