Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Don't depend on the judgmental behavior of Bool.eqb (#217) | Jason Gross | 2018-01-17 | 1 | -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/CompCert | Bernhard Schommer | 2018-01-17 | 1 | -3/+9 |
|\ | |||||
| * | Added type annotations for exported program. (#50)v3.2 | Bernhard Schommer | 2018-01-15 | 1 | -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 Schommer | 2018-01-15 | 1 | -1/+7 |
| | | | | | | | | This should fix issue 216 and also allows it to print 64 bit offsets. | ||||
* | | Added missing help and common options. | Bernhard Schommer | 2018-01-17 | 1 | -1/+15 |
|/ | | | | | Clightgen also now has command line flags to control warnings as well as some other general options. | ||||
* | Preparations for release 3.2 | Xavier Leroy | 2018-01-13 | 2 | -6/+9 |
| | |||||
* | Improved message recommending an OCaml version to use | Xavier Leroy | 2018-01-13 | 1 | -1/+1 |
| | |||||
* | Add regression test for issue #211 | Xavier Leroy | 2018-01-13 | 3 | -1/+17 |
| | |||||
* | Mention the RISC-V port as well | Xavier Leroy | 2018-01-13 | 2 | -3/+3 |
| | |||||
* | Bump to version 3.2 | Xavier Leroy | 2018-01-13 | 1 | -1/+1 |
| | |||||
* | Move machine initialization to Frontend.init function. (#49) | Bernhard Schommer | 2018-01-11 | 4 | -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 section | Xavier Leroy | 2018-01-11 | 1 | -3/+4 |
| | | | | So that it is consistent with the LICENSE file. | ||||
* | Update Changelog with recent changes | Xavier Leroy | 2018-01-11 | 1 | -1/+13 |
| | |||||
* | Added option -o to clightgen. | Bernhard Schommer | 2018-01-11 | 1 | -5/+47 |
| | | | Also allow preprocessed source files as input. | ||||
* | Add riscv and attributes to Clightgen | Bernhard Schommer | 2018-01-10 | 1 | -0/+4 |
| | |||||
* | Minor improvements. | Bernhard Schommer | 2018-01-10 | 1 | -2/+2 |
| | |||||
* | Change README to markdown. | Bernhard Schommer | 2018-01-10 | 1 | -15/+14 |
| | |||||
* | Remove mnemonics not exported to JSON from mnemonics list | Michael Schmidt | 2018-01-09 | 1 | -4/+4 |
| | |||||
* | Update man page for new Diab target option | Michael Schmidt | 2018-01-08 | 1 | -6/+8 |
| | |||||
* | Update man page for new Diab target option | Michael Schmidt | 2018-01-08 | 1 | -0/+6 |
| | |||||
* | Change AsmToJson to be similar to other printers. | Bernhard Schommer | 2018-01-05 | 10 | -62/+87 |
| | |||||
* | Added toolchain specific option for dcc. (#47) | Bernhard Schommer | 2018-01-05 | 1 | -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 Leroy | 2018-01-05 | 17 | -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 Schommer | 2018-01-04 | 4 | -13/+18 |
| | | | | | This time with the correct place for setting the destination files. Bug 20521 | ||||
* | Remove duplicated code. Bug 20521 | Bernhard Schommer | 2018-01-04 | 1 | -46/+26 |
| | |||||
* | Remove all temporary files at program exit (#46) | Bernhard Schommer | 2018-01-03 | 4 | -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 Koenig | 2018-01-03 | 1 | -13/+2 |
| | | | The lemma is now in lib/Coqlib.v. | ||||
* | Use quoted strings in clightgen. | Bernhard Schommer | 2018-01-02 | 1 | -22/+24 |
| | |||||
* | Coq 8.7.1 support | Xavier Leroy | 2017-12-18 | 2 | -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 printer | Michael Schmidt | 2017-12-15 | 1 | -3/+6 |
| | |||||
* | Reintroduce informative comment for Ploadsymbol_lbl in target printer | Michael Schmidt | 2017-12-15 | 1 | -2/+2 |
| | |||||
* | Introduce 'cmn' instruction and optimize compare-with-immediate when negated ↵ | Michael Schmidt | 2017-12-15 | 6 | -1/+27 |
| | | | | immediates can be encoded. | ||||
* | Moved constant expansion into Asmexpand. (#40) | Bernhard Schommer | 2017-12-14 | 5 | -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 Schmidt | 2017-12-14 | 1 | -4/+3 |
| | | | | assembler (add ra, rb, #-1 --> sub ra, rb, #1) | ||||
* | Export configured architecture to JSON (#38) | Michael Schmidt | 2017-12-13 | 2 | -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 Schommer | 2017-12-12 | 1 | -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 Schommer | 2017-12-12 | 1 | -24/+25 |
| | |||||
* | Merge pull request #210 from ppedrot/fix-coq-6277 | Xavier Leroy | 2017-12-11 | 1 | -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édrot | 2017-12-07 | 1 | -1/+1 |
| | | | | | | | | We simply fully qualify the modules. This is backward compatible. | ||||
* | | Correct test for noinline. Bug 22642 | Bernhard Schommer | 2017-12-11 | 1 | -1/+1 |
| | | |||||
* | | Test for inline. Bug 22642 | Bernhard Schommer | 2017-12-08 | 1 | -1/+1 |
| | | |||||
* | | Introduce and use C2C.atom_inline function with 3-valued result | Xavier Leroy | 2017-12-08 | 2 | -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 22642 | Bernhard Schommer | 2017-12-08 | 2 | -3/+2 |
| | | |||||
* | | Store the different inlining cases. | Bernhard Schommer | 2017-12-08 | 3 | -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 22642 | Bernhard Schommer | 2017-12-07 | 1 | -3/+3 |
|/ | |||||
* | Inlining of static functions which are only called once. (#37) | Bernhard Schommer | 2017-12-07 | 7 | -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 Schmidt | 2017-12-05 | 8 | -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. | ||||
* | Added simple div_one Theorem variants. | Bernhard Schommer | 2017-12-01 | 2 | -0/+40 |
| | |||||
* | Remove unused float_abi_type. | Bernhard Schommer | 2017-11-29 | 1 | -12/+0 |
| | |||||
* | Merge branch 'master' of github.com:AbsIntPrivate/CompCert | Bernhard Schommer | 2017-11-27 | 0 | -0/+0 |
|\ |