| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |\ |
|
| | |\
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Conflicts:
.gitignore
backend/Lineartyping.v
common/Values.v
configure
cparser/Machine.ml
cparser/Machine.mli
driver/Configuration.ml
driver/Frontend.ml
runtime/Makefile
test/c/Makefile
test/c/aes.c
test/compression/Makefile
test/regression/Makefile
test/regression/extasm.c
test/regression/floats-basics.c
test/regression/floats.c
Note : test/regression should be checked, didn't test it yet
|
| | |\ \ |
|
| | | | | |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-non-trapping-load
|
| | | | | | |
|
| | |\ \ \ \
| | |_|/ /
| |/| | /
| | | |/
| | |/| |
mppa-work-upstream-merge
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This commit adds a back-end for the AArch64 architecture, namely ARMv8
in 64-bit mode.
|
| | | | | |
|
| |\| | | |
|
| | | |/
| |/| |
|
| |/ / |
|
| | | |
|
| |\|
| |
| |
| | |
mppa-work-upstream-merge
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
Move its definitions to modules C (the type `builtins`) and Env
(the operations that deal with the initial environment).
Reasons for the refactoring:
1- The name "Builtins" will soon be reused for a Coq module
2- `Env.initial()` makes more sense than `Builtins.environment()`.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
* Do not use `Pervasives.xxx` qualified names
Starting with OCaml 4.08, `Pervasives` is deprecated in favor of `Stdlib`,
and uses of `Pervasives` cause fatal warnings.
This commit uses unqualified names instead, as no ambiguity occurs.
* Clarify "open" statements
OCaml 4.08.0 has stricter warnings concerning open statements that
shadow module names.
Closes: #300
|
| | |
| |
| |
| | |
Updated man page + better usage message.
|
| | |
| |
| |
| |
| | |
Easier to type, and consistent with `-Os` (optimize for smaller code /
optimize for fewer conditional branches).
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Extends the instruction selection pass with an if-conversion optimization:
some if/then/else statements are converted into "select" operations,
which in turn can be compiled down to branchless instruction sequences
if the target architecture supports them.
The statements that are converted are of the form
if (cond) { x = a1; } else { x = a2; }
if (cond) { x = a1; }
if (cond) { /*skip*/; } else { x = a2; }
where a1, a2 are "safe" expressions, containing no operations that can
fail at run-time, such as memory loads or integer divisions.
A heuristic in backend/Selectionaux.ml controls when the optimization occurs,
depending on command-line flags and the complexity of the "then" and "else"
branches.
|
| | | |
|
| |\ \
| | |
| | |
| | | |
mppa-if-conversion
|
| | |/
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Extends the instruction selection pass with an if-conversion optimization:
some if/then/else statements are converted into "select" operations,
which in turn can be compiled down to branchless instruction sequences
if the target architecture supports them.
The statements that are converted are of the form
if (cond) { x = a1; } else { x = a2; }
if (cond) { x = a1; }
if (cond) { /*skip*/; } else { x = a2; }
where a1, a2 are "safe" expressions, containing no operations that can
fail at run-time, such as memory loads or integer divisions.
A heuristic in backend/Selectionaux.ml controls when the optimization occurs,
depending on command-line flags and the complexity of the "then" and "else"
branches.
|
| | |
| |
| |
| |
| |
| | |
This is a manual, partial merge of Github pull request #296 by @Fourchaux.
flocq/, cparser/MenhirLib/ and parts of test/ have not been changed
because these are local copies and the fixes should be performed upstream.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The option -fcommon controls whether uninitialized global
variables are placed in the COMMON section. If the option is given
in the negated form, -fno-common, variables are not placed in the
COMMON section. They are placed in the same sections as gcc does.
If the variables are not placed in the COMMON section merging of
tentative definitions is inhibited and multiple definitions lead
to a linker error, as it does for gcc.
|
| | |
| |
| |
| |
| | |
The AbsInt build number no longer contains "release", so it must
be printed additionally.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
* Move the expansion of response files to module Commandline,
during the initialization of `Commandline.argv`.
This way we're sure it's done exactly once.
* Make `Commandline.argv` a `string array` instead of a `string array ref`.
We no longer need to update it after initialization!
* Improve reporting of errors during expansion of response files.
|
| | |
| |
| |
| |
| |
| | |
Add a check for alignment on command-line switches `-falign-*`.
The check is similar to the one for the alignment attribute and
ensures that only powers of two can be specified.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
As suggested in #282, it can be useful to #ifdef code depending on
specific versions of CompCert.
Assuming a version number of the form MM.mm ,
the following macros are predefined:
__COMPCERT_MAJOR__=MM (the major version number)
__COMPCERT_MINOR__=mm (the minor version number)
__COMPCERT_VERSION__=MMmm (two decimal digits for the minor, e.g. 305 for version 3.5)
We also define __COMPCERT_BUILDNR__ if the build number is not empty in file ./VERSION.
Closes: #282
|
| | | |
|
| |\ \ |
|
| | | | |
|
| |/ / |
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| |/ /
| |
| |
| | |
(-fpostpass nameofscheduler)
|
| | | |
|
| |\ \
| | |
| | |
| | | |
gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
|
| | | | |
|
| | | | |
|
| |/ / |
|
| | | |
|
| | | |
|
