aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Refactor the handling of errors and warnings (#44)Bernhard Schommer2018-02-0826-138/+147
| | | | | | | | | | | | | | | | | * 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.
* Removed superfluous check.Bernhard Schommer2018-02-061-4/+0
|
* Share code for common options.Bernhard Schommer2018-01-293-131/+120
| | | | | | 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.
* Don't depend on the judgmental behavior of Bool.eqb (#217)Jason Gross2018-01-171-1/+1
| | | | | 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
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2018-01-171-3/+9
|\
| * Added type annotations for exported program. (#50)v3.2Bernhard Schommer2018-01-151-2/+2
| | | | | | | | Added types for global_definitions in order to avoid problems with implicit parameters. This should fix issue 215
| * Use Ptrofs.repr instead of Int.repr for Init_addrof. (#51)Bernhard Schommer2018-01-151-1/+7
| | | | | | | | This should fix issue 216 and also allows it to print 64 bit offsets.
* | Added missing help and common options.Bernhard Schommer2018-01-171-1/+15
|/ | | | | Clightgen also now has command line flags to control warnings as well as some other general options.
* Preparations for release 3.2Xavier Leroy2018-01-132-6/+9
|
* Improved message recommending an OCaml version to useXavier Leroy2018-01-131-1/+1
|
* Add regression test for issue #211Xavier Leroy2018-01-133-1/+17
|
* Mention the RISC-V port as wellXavier Leroy2018-01-132-3/+3
|
* Bump to version 3.2Xavier Leroy2018-01-131-1/+1
|
* Move machine initialization to Frontend.init function. (#49)Bernhard Schommer2018-01-114-42/+30
| | | | | 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.
* Update copyright sectionXavier Leroy2018-01-111-3/+4
| | | | So that it is consistent with the LICENSE file.
* Update Changelog with recent changesXavier Leroy2018-01-111-1/+13
|
* Added option -o to clightgen.Bernhard Schommer2018-01-111-5/+47
| | | Also allow preprocessed source files as input.
* Add riscv and attributes to ClightgenBernhard Schommer2018-01-101-0/+4
|
* Minor improvements.Bernhard Schommer2018-01-101-2/+2
|
* Change README to markdown.Bernhard Schommer2018-01-101-15/+14
|
* Remove mnemonics not exported to JSON from mnemonics listMichael Schmidt2018-01-091-4/+4
|
* Update man page for new Diab target optionMichael Schmidt2018-01-081-6/+8
|
* Update man page for new Diab target optionMichael Schmidt2018-01-081-0/+6
|
* Change AsmToJson to be similar to other printers.Bernhard Schommer2018-01-0510-62/+87
|
* Added toolchain specific option for dcc. (#47)Bernhard Schommer2018-01-051-1/+16
| | | | | | CompCert now accepts the target configuration option of the diab data compiler and passes it on to the preprocessor, assembler and linker. Bug 20521
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-0517-8/+60
| | | | | | | | | | | 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/
* Handle dcompcertc and dparsedc like all dump opts.Bernhard Schommer2018-01-044-13/+18
| | | | | This time with the correct place for setting the destination files. Bug 20521
* Remove duplicated code. Bug 20521Bernhard Schommer2018-01-041-46/+26
|
* Remove all temporary files at program exit (#46)Bernhard Schommer2018-01-034-19/+17
| | | | | | | | | 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.
* ValueAnalysis: remove duplicate list_forall2_in_left (#212)Jérémie Koenig2018-01-031-13/+2
| | | The lemma is now in lib/Coqlib.v.
* Use quoted strings in clightgen.Bernhard Schommer2018-01-021-22/+24
|
* Coq 8.7.1 supportXavier Leroy2017-12-182-5/+6
| | | | It is compatible with 8.7.0 and 8.6.1, no changes required to the Coq sources of CompCert.
* Reintroduce informative comments for Pflid_lbl/Pflis_lbl in target printerMichael Schmidt2017-12-151-3/+6
|
* Reintroduce informative comment for Ploadsymbol_lbl in target printerMichael Schmidt2017-12-151-2/+2
|
* Introduce 'cmn' instruction and optimize compare-with-immediate when negated ↵Michael Schmidt2017-12-156-1/+27
| | | | immediates can be encoded.
* Moved constant expansion into Asmexpand. (#40)Bernhard Schommer2017-12-145-318/+419
| | | | | 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.
* Use instructions with immediate operands that don't need replacement by the ↵Michael Schmidt2017-12-141-4/+3
| | | | assembler (add ra, rb, #-1 --> sub ra, rb, #1)
* Export configured architecture to JSON (#38)Michael Schmidt2017-12-132-3/+9
| | | 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. (#42)Bernhard Schommer2017-12-121-7/+7
| | | | | | * 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.
* Deactivate ais_annotations again.Bernhard Schommer2017-12-121-24/+25
|
* Merge pull request #210 from ppedrot/fix-coq-6277Xavier Leroy2017-12-111-1/+1
|\ | | | | Fix check-proof target of the Makefile after merge of Coq #6277.
| * Fix check-proof target of the Makefile after merge of Coq #6277.Pierre-Marie Pédrot2017-12-071-1/+1
| | | | | | | | We simply fully qualify the modules. This is backward compatible.
* | Correct test for noinline. Bug 22642Bernhard Schommer2017-12-111-1/+1
| |
* | Test for inline. Bug 22642Bernhard Schommer2017-12-081-1/+1
| |
* | Introduce and use C2C.atom_inline function with 3-valued resultXavier Leroy2017-12-082-14/+11
| | | | | | | | | | | | 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.
* | Remove unused code. BUg 22642Bernhard Schommer2017-12-082-3/+2
| |
* | Store the different inlining cases.Bernhard Schommer2017-12-083-10/+28
| | | | | | | | | | | | | | 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
* | Do not inline varag functions. Bug 22642Bernhard Schommer2017-12-071-3/+3
|/
* Inlining of static functions which are only called once. (#37)Bernhard Schommer2017-12-077-13/+105
| | | | | | | | | 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.
* Optimization for division by one during constant propagation (#39)Michael Schmidt2017-12-058-36/+85
| | | | 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.
generated by cgit (git 2.34.1) at 2024-07-03 05:09:33 +0000