Skip to content
Snippets Groups Projects
Commit 74b48ddb authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

m

parent 73c1cd8d
No related branches found
No related tags found
No related merge requests found
......@@ -16,6 +16,18 @@ features, installation instructions, using the compiler, etc), please
refer to the [Web site](https://compcert.org/) and especially
the [user's manual](https://compcert.org/man/).
## Verimag version for IntrinSec target
This is a very experimental version of CompCert.
The people responsible for this version are
* Sylvain Boulmé (Grenoble-INP, Verimag)
* Paolo Torrini (Grenoble-INP, Verimag)
For inquiries on this very specific version, contact:
Sylvain.Boulme@univ-grenoble-alpes.fr
## License
CompCert is not free software. This non-commercial release can only
be used for evaluation, research, educational and personal purposes.
......
......@@ -75,6 +75,7 @@ let fast_cmove ty =
| "powerpc", "e5500" ->
(match ty with Tint -> true | Tlong -> true | _ -> false)
| "powerpc", _ -> false
| "intrinsec", _ -> false
| "riscV", _ -> false
| "x86", _ ->
(match ty with Tint -> true | Tlong -> Archi.ptr64 | _ -> false)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment