| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |\
| |
| |
| |
| |
| |
| |
| |
| | |
PARTIAL MERGE (PARTLY BROKEN).
See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE
WARNING:
interface of va_args and assembly sections have changed
|
| | |
| |
| |
| |
| |
| |
| | |
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`.
|
| |/ |
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
| |
Sometimes the result of a void function is assigned to a variable.
This can occur with C conditional expressions ?: at type void,
e.g. the "assert" macro of MacOS.
A similar relaxation was already there in RTLtyping.
|
|
|
This module is similar to RTLtyping: it performs type inference and
type checking, but on the Cminor intermediate representation rather
than the RTL IR. For each function, it returns a mapping from variables
to types. Its first use will be if-conversion optimization.
|
