| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/
* Replaced eprintf error. Instead of having eprintf msg; exit 2 use the functions from the
Diagnostics module.
* Raise on error before calling external tools.
* Added diagnostics to clightgen.
* Fix error handling of AsmToJson.
* Cleanup error handling of Elab and C2C.
*The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.
|
| |
|
|
|
|
|
|
| |
In order to avoid more divergence between the command line options of
clightgen and ccomp the code for the common options, the language support
options, the version string and the general options.
|
|
|
|
|
| |
This change is backwards compatible, and makes flocq compatible with
https://github.com/coq/coq/pull/6596. Was applied to the Flocq master sources
https://gitlab.inria.fr/flocq/flocq/commit/db356aa5ea0fd0234e3872f70e8972086055cd57
|
|\ |
|
| |
| |
| |
| | |
Added types for global_definitions in order to avoid problems with
implicit parameters. This should fix issue 215
|
| |
| |
| |
| | |
This should fix issue 216 and also allows it to print 64 bit offsets.
|
|/
|
|
|
| |
Clightgen also now has command line flags to control warnings as
well as some other general options.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
| |
The initialization of Machine.config, as well as the calls to various initialization functions for the C front-end, are now performed by the new `Frontend.init` function.
This avoids code duplication in driver/Driver.ml and exportclight/Clightgen.ml.
|
|
|
|
| |
So that it is consistent with the LICENSE file.
|
| |
|
|
|
| |
Also allow preprocessed source files as input.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
CompCert now accepts the target configuration option of the diab
data compiler and passes it on to the preprocessor, assembler and
linker.
Bug 20521
|
|
|
|
|
|
|
|
|
|
|
| |
Some files are dual-licensed (GPL + noncommercial license), as marked redundantly in the license headers of those files, and in the LICENSE file. OVer the years those two markings got inconsistent.
This commit updates the LICENSE file and the license headers of some files so that they agree on which files are dual-licensed.
Some build-related files were dual-licensed but some others were not. Fixed by dual-licensing configure, Makefile.menhir, extraction/extraction.v, */extractionMachdep.v
Moved lib/Json* to backend/ because there is no need to dual-license those files, yet lib/* is dual-licensed. Plus: JsonAST did not really belong in lib/ anyway, as it depends on AST
which is not in lib/
|
|
|
|
|
| |
This time with the correct place for setting the destination files.
Bug 20521
|
| |
|
|
|
|
|
|
|
|
|
| |
Replaced calls to Filename.temp_file by own version Driveraux.tmp_file.
The Driveraux.tmp_file function takes care that the temporary files are
removed at exit.
Consequently there is no need to explicitly remove temp files in Driver.
|
|
|
| |
The lemma is now in lib/Coqlib.v.
|
| |
|
|
|
|
| |
It is compatible with 8.7.0 and 8.6.1, no changes required to the Coq sources of CompCert.
|
| |
|
| |
|
|
|
|
| |
immediates can be encoded.
|
|
|
|
|
| |
This commit introduces a new pass which is run after the expansion of the
builtin functions which performs the expansion and placement of
constants inside the function code.
|
|
|
|
| |
assembler (add ra, rb, #-1 --> sub ra, rb, #1)
|
|
|
| |
The architecture which was configured is now exported in a new top-level json field.
|
|
|
|
|
|
| |
* Do not pass the env back from for stmt decls.
This is the source of issue #211, the environment from the elaboration of
the declaration and expressions in the for loop should not be passed back.
|
| |
|
|\
| |
| | |
Fix check-proof target of the Makefile after merge of Coq #6277.
|
| |
| |
| |
| | |
We simply fully qualify the modules. This is backward compatible.
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
Instead of two Boolean tests C2C.atom_is_{no,}inline, have a single
C2C.atom_inline function that returns one of the three possible values
stored in the the a_inline field.
|
| | |
|
| |
| |
| |
| |
| |
| |
| | |
In order to correctly support the noinline attribute we must store
whether the function was specified with an inline specifer, had
a noinline attribute or nothing.
Bug 22642
|
|/ |
|
|
|
|
|
|
|
|
|
| |
New inlining heuristic for static functions.
Static functions that are only called once can always be inlined,
since they can be removed safely after inlining and no call
prologue, epilogue, as well as register saving and needs to be
generated.
|
|
|
|
| |
Signed and unsigned divisions by literal 1 are already optimized away during the Selection phase. This pull request also optimizes those divisions when the 1 divisor is produced by constant propagation.
|