Jasmin compiler
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
compiler
proofs
scripts
.gitignore
.travis.yml
LICENSE
MANIFEST
Makefile
README.md
coqword.nix
default.nix

README.md

Jasmin

This repository contains the following subdirectories:

  • compiler/ : Compiler from jasmin-lang to assembly.
  • proofs/ : Coq implementations of compiler passes / checkers.

Dependencies

  • For the compiler: check compiler/README.md
  • For the proofs:
    • Coq (tested with 8.7.2)
    • The Mathematical Components library for Coq (tested with 1.7.0)

Testing

  1. To compile and test the compiler:
    • $ cd compiler
    • $ make CIL build
    • $ make tests
  2. To compile Coq proofs:
    • $ cd proofs
    • $ make

License

All our code is MIT licensed. Since we use GPL licensed third party Coq theories and extract code from the LGPL licensed Coq standard library, our compiler is GPL licensed.