Commit f7431b4a authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

brief installation instructions

parent 74b48ddb
......@@ -28,6 +28,20 @@ The people responsible for this version are
For inquiries on this very specific version, contact:
Sylvain.Boulme@univ-grenoble-alpes.fr
## Testing the IntrinSec target of CompCert
First, compile CompCert for `intrinsec`:
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 [`config_intrinsec.sh`](config_intrinsec.sh)).
3. then, run `make -j`.
Then, you may compile a C file into the IntrinSec assembly. For example, this produce a `nsieve.s` assembly file:
```./ccomp -S test/c/nsieve.c -o nsieve.s```
In order to run it, you need an IntrinSec assembler and an IntrinSec emulator, which we are not authorized to provide. If you are interested in, please directly contact Olivier Savry (`olivier.savry@cea.fr`).
## License
CompCert is not free software. This non-commercial release can only
be used for evaluation, research, educational and personal purposes.
......
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