aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Always try inlining functionsYann Herklotz2023-04-271-4/+1
* Change preference for new register in allocatorBernhard Schommer2023-03-061-29/+34
* Ignore self assign in if-conversionBernhard Schommer2023-02-202-4/+19
* Disable tail calls in variadic functionsMichael Schmidt2023-01-232-5/+6
* Use `exfalso` instead of `elimtype False` (#470)Pierre-Marie Pédrot2022-12-222-3/+3
* Update doc commentXavier Leroy2022-12-081-2/+2
* Add `Declare Scope` where appropriate (#440)Xavier Leroy2022-09-193-0/+5
* RTLgen: use the state and error monad for reserve_labels (#371)Pierre Nigron2022-09-193-24/+20
* Improved auto goal selection (#443)Andrej Dudenhefner2022-09-084-5/+5
* Recognize more if-then-else statements that can be if-convertedXavier Leroy2022-09-052-126/+138
* Remove unused functions.Bernhard Schommer2022-09-031-7/+0
* More simplifications for literal printingBernhard Schommer2022-09-032-13/+16
* Refactor emitting of constants.Bernhard Schommer2022-09-032-2/+15
* Add `iter_literal*` functions with guaranteed iteration orderXavier Leroy2022-09-031-0/+12
* Support mergeable sections for fixed-size literalsXavier Leroy2022-08-293-4/+39
* Enforce evaluation order in IRC.add_interf and IRC.add_prefXavier Leroy2021-12-071-2/+2
* An improved PTree data structure (#420)Xavier Leroy2021-11-162-3/+3
* Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-032-2/+2
* Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-151-2/+5
* Handle the new warnings of OCaml 4.13Xavier Leroy2021-09-131-3/+3
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-082-8/+10
* Emit no entry for variables without init in json.Bernhard Schommer2021-04-291-1/+7
* Use List.repeat from Coq's standard library instead of list_repeatXavier Leroy2021-04-191-1/+1
* Fix regression on PowerPC / DiabXavier Leroy2021-02-231-2/+7
* Section handling: finer control of variable initializationXavier Leroy2021-02-233-10/+25
* Introduce and use PrintAsmaux.variable_sectionXavier Leroy2021-02-231-7/+12
* Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-2110-60/+60
* Improve branch tunnelingXavier Leroy2021-01-132-60/+328
* Revised correctness proof for record_gotoXavier Leroy2021-01-131-68/+29
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-2927-636/+636
* Changed cc_varargs to an option typeBernhard Schommer2020-12-251-1/+1
* Add support for __builtin_fabsfXavier Leroy2020-07-272-0/+6
* Introduce additional "branch" build information.Bernhard Schommer2020-07-081-2/+2
* Move shared code in new file.Bernhard Schommer2020-06-286-5/+44
* Eliminate known builtins whose result is ignoredXavier Leroy2020-06-252-40/+54
* Transform non-recursive Fixpoint into DefinitionXavier Leroy2020-06-212-2/+2
* Move reserved_registers to CPragmas.Bernhard Schommer2020-04-202-7/+1
* Weaker ec_readonly condition over external calls (#225)Xavier Leroy2020-03-021-3/+2
* Define IRC.class_of_type for types Tany32, Tany64Xavier Leroy2020-03-021-1/+2
* Platform-independent implementation of Conventions.size_arguments (#222)Xavier Leroy2020-02-241-0/+67
* Cosmetic: in OCaml code, write "open! Module" instead of "open !Module"Xavier Leroy2020-02-212-2/+2
* Refine the type of function results in AST.signatureXavier Leroy2020-02-2113-90/+101
* Remove no longer needed file PrintLTLinBernhard Schommer2019-11-121-115/+0
* Make explicit the use of hints from OrderedType (#316)Vincent Laporte2019-10-022-8/+8
* Reworked json export.Bernhard Schommer2019-09-123-29/+37
* Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-171-2/+2
* AArch64 portXavier Leroy2019-08-087-37/+97
* Asmgenproof0: add predicate exec_straight0Xavier Leroy2019-08-071-0/+26
* Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-071-2/+0
* Improve CSE for known built-in functionsXavier Leroy2019-07-172-7/+14
generated by cgit (git 2.34.1) at 2024-05-04 02:20:52 +0000