aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* 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.
* 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.
* Added simple div_one Theorem variants.Bernhard Schommer2017-12-012-0/+40
|
* Remove unused float_abi_type.Bernhard Schommer2017-11-291-12/+0
|
* Merge branch 'master' of github.com:AbsIntPrivate/CompCertBernhard Schommer2017-11-270-0/+0
|\
| * Remove temporary .o files after linking (#36)Xavier Leroy2017-11-271-2/+5
| | | | | | | | | | | | | | When -c is not given, .o files are now generated in /tmp, but they are still not erased. This commit uses an "at_exit" action to erase those temporary .o files before CompCert exits. Using at_exit is easier to implement than explicit erasure (like we do for other temporary files), yet should not result in temporary files lingering in /tmp longer than strictly necessary, since the call to the linker is the last thing that CompCert does before exiting, hence temporary .o files are erased just after the linker returns.
* | Remove temporary .o files after linking (#36)Xavier Leroy2017-11-271-2/+5
|/ | | | | | | When -c is not given, .o files are now generated in /tmp, but they are still not erased. This commit uses an "at_exit" action to erase those temporary .o files before CompCert exits. Using at_exit is easier to implement than explicit erasure (like we do for other temporary files), yet should not result in temporary files lingering in /tmp longer than strictly necessary, since the call to the linker is the last thing that CompCert does before exiting, hence temporary .o files are erased just after the linker returns.
* Issue #208: make value analysis of comparisons more conservative w.r.t. ↵Xavier Leroy2017-11-242-8/+15
| | | | | | | pointers (#209) Comparisons such as "(uintptr_t) &global == 0x1234" are undefined behavior in CompCert but their status in ISO C is unclear and they may occur in real-world code. Make sure they are statically analyzed as Btop.
generated by cgit (git 2.34.1) at 2024-06-13 11:12:15 +0000