Jasmin

Language reference

  • Syntax reference
  • Semantics reference
    • Scalar types
    • Arrays in Jasmin programs
    • System calls
    • Variable Spilling

Compiler

  • Compilation passes
  • Advanced details

Tools

  • How to compile a Jasmin program to assembly
  • Easycrypt extraction
  • Safety checker
  • Linting Jasmin programs
  • Constant-time programming
  • Selective Speculative Load Hardening
  • How to execute the formal semantics
  • How to pretty-print a Jasmin program

Miscellaneous

  • Installation Guide
  • FAQ
  • Emacs mode
Jasmin
  • Semantics reference
  • Edit on GitHub

Semantics reference

  • Scalar types
    • Integers
      • Compilation
    • Machine words
      • Compilation
      • Verification
    • Word-Sized Integers (aka. wint)
      • Syntax
      • Safety
      • Conversion
      • Compilation
      • Verification
  • Arrays in Jasmin programs
    • Declaration
    • Access
      • Explicit scaling
      • Type punning
    • Intuition about reg ptr and stack ptr
  • System calls
  • Variable Spilling
    • Spilling to MMX Registers
    • Liveness and Spilling
      • Example: Without Spilling
      • Example: With Spilling
    • Debugging Spills
Previous Next

© Copyright Jasmin contributors.

Built with Sphinx using a theme provided by Read the Docs.