aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Added type annotations for exported program. (#50)v3.2Bernhard Schommer2018-01-151-2/+2
* Use Ptrofs.repr instead of Int.repr for Init_addrof. (#51)Bernhard Schommer2018-01-151-1/+7
* 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
* Update copyright sectionXavier Leroy2018-01-111-3/+4
* Update Changelog with recent changesXavier Leroy2018-01-111-1/+13
* Added option -o to clightgen.Bernhard Schommer2018-01-111-5/+47
* 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
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-0517-8/+60
* Handle dcompcertc and dparsedc like all dump opts.Bernhard Schommer2018-01-044-13/+18
* Remove duplicated code. Bug 20521Bernhard Schommer2018-01-041-46/+26
* Remove all temporary files at program exit (#46)Bernhard Schommer2018-01-034-19/+17
* ValueAnalysis: remove duplicate list_forall2_in_left (#212)Jérémie Koenig2018-01-031-13/+2
* Use quoted strings in clightgen.Bernhard Schommer2018-01-021-22/+24
* Coq 8.7.1 supportXavier Leroy2017-12-182-5/+6
* 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
* Moved constant expansion into Asmexpand. (#40)Bernhard Schommer2017-12-145-318/+419
* Use instructions with immediate operands that don't need replacement by the a...Michael Schmidt2017-12-141-4/+3
* Export configured architecture to JSON (#38)Michael Schmidt2017-12-132-3/+9
* Do not pass the env back from for stmt decls. (#42)Bernhard Schommer2017-12-121-7/+7
* 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.Pierre-Marie Pédrot2017-12-071-1/+1
* | 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
* | Remove unused code. BUg 22642Bernhard Schommer2017-12-082-3/+2
* | Store the different inlining cases.Bernhard Schommer2017-12-083-10/+28
* | 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
* Optimization for division by one during constant propagation (#39)Michael Schmidt2017-12-058-36/+85
* 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
* | Remove temporary .o files after linking (#36)Xavier Leroy2017-11-271-2/+5
|/
* Issue #208: make value analysis of comparisons more conservative w.r.t. point...Xavier Leroy2017-11-242-8/+15
generated by cgit (git 2.34.1) at 2024-05-17 07:52:55 +0000