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 /README.md | |
| parent | 4b7dc067af57e6aa917e54f39219ede3e447dd71 (diff) | |
| download | compcert-kvx-dd11a51feb082c6b978c9a9a6cd09272116bdfae.tar.gz compcert-kvx-dd11a51feb082c6b978c9a9a6cd09272116bdfae.zip | |
readme
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 15 |
1 files changed, 15 insertions, 0 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. |