• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Soft
        • Bv
        • Imp-language
        • C
          • Syntax-for-tools
          • Atc
          • Language
            • Abstract-syntax
            • Integer-ranges
            • 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
            • Implementation-environments
            • 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
          • Pack
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Number-theory
        • Cryptography
        • Lists-light
        • Builtins
        • Axe
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Language

Integer-operations

Operations on C integers.

Subtopics

Convert-integer-value
Convert an integer value to an integer type [C: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 [C:6.3.1.8].
Bitnot-integer-value
Apply ~ to an integer value [C:6.5.3.3/4].
Bitand-integer-values
Apply & to integer values [C:6.5.10/4].
Promote-value
Apply the integer promotions to a value [C:6.3.1.1/2].
Rem-integer-values
Apply % to integer values [C:6.5.5/5] [C:6.5.5/6].
Shr-integer-values
Apply >> to integer values [C:6.5.7/3] [C:6.5.7/5].
Shl-integer-values
Apply << to integer values [C:6.5.7/3] [C: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 [C:6.5.5/5] [C:6.5.5/6].
Bitxor-integer-values
Apply ^ to integer values [C:6.5.11/4].
Bitior-integer-values
Apply | to integer values [C:6.5.12/4].
Sub-integer-values
Apply binary - to integer values [C:6.5.6/6].
Mul-integer-values
Apply binary * to integer values [C:6.5.5/4].
Add-integer-values
Apply binary + to integer values [C:6.5.6/5].
Ne-integer-values
Apply != to integer values [C:6.5.9/3].
Lt-integer-values
Apply < to integer values [C:6.5.8/6].
Le-integer-values
Apply <= to integer values [C:6.5.8/6].
Gt-integer-values
Apply > to integer values [C:6.5.8/6].
Ge-integer-values
Apply >= to integer values [C:6.5.8/6].
Eq-integer-values
Apply == to integer values [C:6.5.9/3].
Minus-integer-value
Apply unary - to an integer value [C:6.5.3.3/3].
Plus-integer-value
Apply unary + to an integer value [C: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 [C: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.