Commit 9fe2f2c1 authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

link on the prisc22 paper

parent b3c1c827
......@@ -22,7 +22,8 @@ This is a very experimental version of CompCert introducing a [PseudoAsm](riscV/
that gives an "Asm-like" semantics to "Mach" programs with a defensive check that all indirect function calls only branch at some function entry.
The purpose is then to prove a bi-simulation between "Mach" and "PseudoAsm".
See [PseudoAsmproof](riscV/lib/PseudoAsmproof.v) and [PseudoAsmRecipSimu](riscV/lib/PseudoAsmRecipSimu.v).
See also explanations in our [PriSC paper](
The people responsible for this version are
* Sylvain Boulmé (Grenoble-INP, Verimag)
......@@ -31,6 +32,13 @@ The people responsible for this version are
For inquiries on this very specific version, contact:
## Compiling this IntrinSec target of CompCert
1. you need a GCC compiler for RISC-V 32 (e.g. `riscv32-unknown-elf-gcc` installed from `sudo apt-get -y install gcc-riscv64-linux-gnu`).
2. you need to configure CompCert compilation for `intrinsec` (e.g. use [``](
3. then, run `make -j`.
This version is really experimental and is not yet intended for code generation.
## License
CompCert is not free software. This non-commercial release can only
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment