• 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
        • Syntax-for-tools
        • Atc
        • Language
          • Abstract-syntax
          • Integer-ranges
          • Implementation-environments
          • Dynamic-semantics
          • Static-semantics
          • Grammar
          • Integer-formats
          • Types
          • Portable-ascii-identifiers
          • Values
          • Integer-operations
            • Convert-integer-value
            • Result-integer-value
            • Uaconvert-values
            • Bitnot-integer-value
            • Bitand-integer-values
            • Promote-value
            • Rem-integer-values
            • Shr-integer-values
            • Shl-integer-values
            • Value-integer
            • Div-integer-values
            • Bitxor-integer-values
            • Bitior-integer-values
            • Sub-integer-values
            • Mul-integer-values
            • Add-integer-values
            • Ne-integer-values
            • Lt-integer-values
            • Le-integer-values
            • Gt-integer-values
            • Ge-integer-values
            • Eq-integer-values
            • Minus-integer-value
            • Plus-integer-value
            • Value-integer->get
            • Lognot-integer-value
            • Test-integer-value
            • Value-integer-and-value-integer->get
          • Computation-states
          • Object-designators
          • Operations
          • Errors
          • Tag-environments
          • Function-environments
          • Character-sets
          • Flexible-array-member-removal
          • Arithmetic-operations
          • Pointer-operations
          • Bytes
          • Keywords
          • Real-operations
          • Array-operations
          • Scalar-operations
          • Structure-operations
        • Representation
        • Transformation-tools
        • Insertion-sort
        • Pack
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • X86isa
      • 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
  • Language

Integer-operations

Operations on C integers.

Subtopics

Convert-integer-value
Convert an integer value to an integer type [C17:6.3.1.3].
Result-integer-value
Calculate the integer value result of an operation.
Uaconvert-values
Apply the usual arithmetic conversions to two arithmetic values [C17:6.3.1.8].
Bitnot-integer-value
Apply ~ to an integer value [C17:6.5.3.3/4].
Bitand-integer-values
Apply & to integer values [C17:6.5.10/4].
Promote-value
Apply the integer promotions to a value [C17:6.3.1.1/2].
Rem-integer-values
Apply % to integer values [C17:6.5.5/5] [C17:6.5.5/6].
Shr-integer-values
Apply >> to integer values [C17:6.5.7/3] [C17:6.5.7/5].
Shl-integer-values
Apply << to integer values [C17:6.5.7/3] [C17:6.5.7/4].
Value-integer
Turn a mathematical (i.e. ACL2) integer into a C integer value.
Div-integer-values
Apply / to integer values [C17:6.5.5/5] [C17:6.5.5/6].
Bitxor-integer-values
Apply ^ to integer values [C17:6.5.11/4].
Bitior-integer-values
Apply | to integer values [C17:6.5.12/4].
Sub-integer-values
Apply binary - to integer values [C17:6.5.6/6].
Mul-integer-values
Apply binary * to integer values [C17:6.5.5/4].
Add-integer-values
Apply binary + to integer values [C17:6.5.6/5].
Ne-integer-values
Apply != to integer values [C17:6.5.9/3].
Lt-integer-values
Apply < to integer values [C17:6.5.8/6].
Le-integer-values
Apply <= to integer values [C17:6.5.8/6].
Gt-integer-values
Apply > to integer values [C17:6.5.8/6].
Ge-integer-values
Apply >= to integer values [C17:6.5.8/6].
Eq-integer-values
Apply == to integer values [C17:6.5.9/3].
Minus-integer-value
Apply unary - to an integer value [C17:6.5.3.3/3].
Plus-integer-value
Apply unary + to an integer value [C17:6.5.3.3/2].
Value-integer->get
Turn a C integer value into a mathematical (i.e. ACL2) integer.
Lognot-integer-value
Apply ! to an integer value [C17:6.5.3.3/5].
Test-integer-value
Test an integer value logically.
Value-integer-and-value-integer->get
Theorems about value-integer and value-integer->get.