| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| |
| |
| |
| | |
gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-non-trapping-load
|
|/ |
|
|
|
|
| |
"omega" fails in Coq 8.7, but not in 8.8 and later.
|
|
|
|
|
|
|
|
| |
The argument is of type Tlong, not Tint.
This caused spurious errors in RTLtyping.
Also: in AArch64/PrintOp.ml, print Cmaskl{zero,notzero} with "&l"
to distinguish them from Cmask{zero,notzero}.
|
|
|
|
| |
These instructions are generated by __builtin_memcpy.
|
|
This commit adds a back-end for the AArch64 architecture, namely ARMv8
in 64-bit mode.
|