| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
|
|
|
| |
Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal.
Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`,
and `xomegaContradiction` with `lia` and `extlia`.
Turn back on the deprecation warning for uses of `omega`.
Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
|
|
|
|
|
|
| |
Pfmovimms, Pfmovimmd destroy X16
Pbtbl preserves X17
Inlined built-in functions destroy X16 and X30
|
|
|
|
|
| |
The two built-in function map to the fmax and fmin instruction.
Bug 30035
|
|
|
|
| |
Using the "rbit" instruction (reverse bits).
|
|
|
|
| |
This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95.
|
|
|
|
|
|
|
| |
The `__builtin_nop` function is documented only for PowerPC.
It was added to the other architectures by copy paste, but has no
known uses. So, remove `__builtin_nop` from all architectures
but PowerPC.
|
|
This commit adds a back-end for the AArch64 architecture, namely ARMv8
in 64-bit mode.
|