Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Refine the type of function results in AST.signature | Xavier Leroy | 2020-02-21 | 1 | -1/+1 |
| | | | | | | | | | | Before it was "option typ". Now it is a proper inductive type that can also express small integer types (8/16-bit unsigned/signed integers). One benefit is that external functions get more precise types that control better their return values. As a consequence, the CompCert C type preservation property now holds unconditionally, without extra typing hypotheses on external functions. | ||||
* | AArch64 port | Xavier Leroy | 2019-08-08 | 1 | -0/+33 |
This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode. |