diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-05-27 10:33:16 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-05-27 10:33:16 +0200 |
| commit | dd11a51feb082c6b978c9a9a6cd09272116bdfae (patch) | |
| tree | 947d5b3c9e06a58367602e16ef7af26c15ff868e | |
| parent | 4b7dc067af57e6aa917e54f39219ede3e447dd71 (diff) | |
| download | compcert-kvx-dd11a51feb082c6b978c9a9a6cd09272116bdfae.tar.gz compcert-kvx-dd11a51feb082c6b978c9a9a6cd09272116bdfae.zip | |
readme
| -rw-r--r-- | README.md | 15 | ||||
| -rw-r--r-- | README_Kalray.md | 4 |
2 files changed, 17 insertions, 2 deletions
@@ -16,6 +16,18 @@ features, installation instructions, using the compiler, etc), please refer to the [Web site](http://compcert.inria.fr/) and especially the [user's manual](http://compcert.inria.fr/man/). +## VERIMAG version +This is a special version with additions from Verimag and Kalray : + * Some general-purpose optimization phases (e.g. profiling). + * A backend for the KVX processor. + +The people responsible for this version are + * Sylvain Boulmé (Grenoble-INP, Verimag) + * David Monniaux (CNRS, Verimag) + * Cyril Six (Kalray) + +See also `README_Kalray.md` and `PROFILING.md`. + ## License CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes. @@ -29,6 +41,7 @@ The CompCert verified compiler is Copyright Institut National de Recherche en Informatique et en Automatique (INRIA) and AbsInt Angewandte Informatik GmbH. +The additions are Copyright Grenoble-INP, CNRS and Kalray. ## Contact General discussions on CompCert take place on the @@ -37,3 +50,5 @@ mailing list. For inquiries on the commercial version of CompCert, please contact info@absint.com + +For inquiries on the Verimag-specific additions, contact the researchers. diff --git a/README_Kalray.md b/README_Kalray.md index c6509597..7dba03dd 100644 --- a/README_Kalray.md +++ b/README_Kalray.md @@ -27,6 +27,6 @@ make make test ``` -The reference files were generated using `k1-cos-gcc -O1`. +The reference files were generated using `kvx-cos-gcc -O1`. -We also have our own tests in `test/mppa/` - to run them, execute the script `simucheck.sh` located in that folder. These consist in comparing `compcert` output to `k1-cos-gcc` output. +We also have our own tests in `test/kvx/` - to run them, execute the script `simucheck.sh` located in that folder. These consist in comparing `compcert` output to `kvx-cos-gcc` output. |