aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Inlining.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-241-2/+5
|\
| * Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-151-2/+5
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-7/+7
|\|
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-7/+7
* | Adding info field for branching in RTL, LTL, XTL and all associated passesCyril SIX2020-03-111-2/+2
* | avancement (il faut utiliser Vundef visiblement)David Monniaux2019-09-021-2/+2
|/
* Inlining of static functions which are only called once. (#37)Bernhard Schommer2017-12-071-4/+9
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-8/+8
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-061-0/+1
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-6/+6
* Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-9/+3
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-11/+11
* Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.Xavier Leroy2015-08-221-1/+1
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-9/+12
* Extend annotations so that they can keep track of global variables and local ...Xavier Leroy2015-03-271-0/+12
* Inlining: preserve all RTL regs mentioned in the function, not justxleroy2014-03-291-29/+3
* Revised renumbering of nodes and registers so that main function is not shift...xleroy2013-10-181-4/+6
* Merge of the "princeton" branch:xleroy2013-06-161-2/+0
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-6/+12
* Pointers one pastxleroy2013-02-151-1/+1
* Remove some useless "Require".xleroy2012-12-301-1/+0
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-11/+7
* Merge of the newmem branch:xleroy2012-05-211-0/+477