| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Generate a nop instruction after ais annotations.
In order to prevent the merging of ais annotations with following
Labels a nop instruction is inserted, but only if the annotation
is followed immediately by a label.
The insertion of nop instructions is performed during the
expansion of builtin and pseudo assembler instructions and is
processor independent, by inserting a __builtin_nop built-in.
* Add Pnop instruction to ARM, RISC-V, and x86
ARM as well as RISC-V don't have nop instructions that can
be easily encoded by for example add with zero instructions.
For x86 we used to use `mov X0, X0` for nop but this may
not be as efficient as the true nop instruction.
* Implement __builtin_nop on all supported target architectures.
This builtin is not yet made available on the C side for all architectures.
Bug 24067
|
|
|
|
|
|
| |
This extension enables more addressing modes to be encoded as builtin arguments and used in conjunction with volatile memory accesses.
Current status: x86 port only, the only new addressing mode handled is reg + offset.
|
|
|
|
|
|
| |
Hide the reference used internally behind the interface and added
some functions to access the needed values.
Bug 18394
|
| |
|
|
|
|
|
|
|
| |
Instead of making each filed mutuable we use a reference to a record
of type implem. Now only the default implementation and the default
debug information need to be upated to add a new function.
Bug 17392.
|
|
|
|
|
|
| |
If a label is printed before a list of debug annotations we can use it
for the debug annotations and don't need to add an extra label.
Bug 17392
|
|
|
|
|
|
| |
Like for arm and ppc the functions for section names and start and
end addresses of compilation units are defined and the print_annot
function is moved to Asmexpandaux.ml.
|
|
|
|
|
|
| |
The function is generalized to work for all backends and takes as
additional arguments functions for the printing of the simple
instructions and the translation function for the arguments.
|
| |
|
|
|
|
|
| |
This reverts commit 777566e81b9762d6bdc773a1f63d56a7ac97433c, reversing
changes made to daf9ac64fc9611ecf09d70560a6fa1ba80b9c9c1.
|
|
the same way as it is done for PPC.
|