| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
|
| |
This avoids a new warning of Coq 8.13.
Eventually these `Global Hint` should become `#[export] Hint`,
with a cleaner but different meaning than `Global Hint`.
|
| |
|
|
|
|
|
|
|
|
|
| |
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`.
|
| |
|
|
|
| |
This commit adds support for macOS (and probably iOS) running on
AArch64 / ARM 64-bit / "Apple silicon" processors.
|
| |
|
|
|
|
|
|
|
| |
In addressing modes for load and store instructions, the offset must be a multiple of the memory size being accessed. When accessing global variables, this may not be the case if the alignment of the variable is less than its size. Errors occur at link time.
This PR extends the check for a representable offset for the addressing of global
variables to also check whether the variable is correctly aligned. Only if both conditions are
met can we generate the short sequence Padrp / ADadr. Otherwise we go through the generic
loadsymbol sequence.
|
| |
|
|
| |
"omega" fails in Coq 8.7, but not in 8.8 and later.
|
|
|
This commit adds a back-end for the AArch64 architecture, namely ARMv8
in 64-bit mode.
|
