• 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
        • Linear-memory
        • Rflag-specifications
          • Rflags-reads-and-writes
          • General-sf-spec-fn
          • General-cf-spec-fn
          • General-pf-spec-fn
          • General-of-spec-fn
          • Zf-spec
          • Sbb-af-spec8
          • Sbb-af-spec64
          • Sbb-af-spec32
          • Sbb-af-spec16
          • Adc-af-spec8
          • Adc-af-spec64
          • Adc-af-spec32
          • Adc-af-spec16
          • Sub-af-spec8
          • Sub-af-spec64
          • Sub-af-spec32
          • Sub-af-spec16
          • Add-af-spec8
          • Add-af-spec64
          • Add-af-spec32
          • Add-af-spec16
          • Pf-spec64
          • Pf-spec32
          • Pf-spec16
          • Of-spec64
          • Sf-spec64
          • Sf-spec32
          • Sf-spec16
          • Pf-spec8
          • Of-spec8
          • Of-spec32
          • Of-spec16
          • Cf-spec8
          • Cf-spec64
          • Cf-spec32
          • Cf-spec16
          • Sf-spec8
        • Characterizing-undefined-behavior
        • Top-level-memory
        • App-view
        • X86-decoder
        • 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
    • 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

• Machine

Rflag-specifications

Specifications of rflags

Subtopics

Rflags-reads-and-writes

Reading from and writing to the rflags register in the x86 state

General-sf-spec-fn

General-cf-spec-fn

General-pf-spec-fn

General-of-spec-fn

Zf-spec

Sbb-af-spec8

Sbb-af-spec64

Sbb-af-spec32

Sbb-af-spec16

Adc-af-spec8

Adc-af-spec64

Adc-af-spec32

Adc-af-spec16

Sub-af-spec8

Sub-af-spec64

Sub-af-spec32

Sub-af-spec16

Add-af-spec8

Add-af-spec64

Add-af-spec32

Add-af-spec16

Pf-spec64

Pf-spec32

Pf-spec16

Of-spec64

Sf-spec64

Sf-spec32

Sf-spec16

Pf-spec8

Of-spec8

Of-spec32

Of-spec16

Cf-spec8

Cf-spec64

Cf-spec32

Cf-spec16

Sf-spec8