aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Inliningspec.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-55/+55
|\
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-55/+55
* | Adding info field for branching in RTL, LTL, XTL and all associated passesCyril SIX2020-03-111-3/+3
* | avancement (il faut utiliser Vundef visiblement)David Monniaux2019-09-021-3/+3
|/
* Inlining of static functions which are only called once. (#37)Bernhard Schommer2017-12-071-6/+6
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-11/+11
* Inliningspec made compatible with a coming fix of zifyletouzey2017-05-271-1/+1
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-5/+5
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-2/+2
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-2/+2
* Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-56/+66
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-86/+86
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-5/+4
* Extend annotations so that they can keep track of global variables and local ...Xavier Leroy2015-03-271-0/+3
* Inlining: preserve all RTL regs mentioned in the function, not justxleroy2014-03-291-65/+10
* Revised renumbering of nodes and registers so that main function is not shift...xleroy2013-10-181-32/+84
* Merge of the "princeton" branch:xleroy2013-06-161-3/+3
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-1/+32
* Pointers one pastxleroy2013-02-151-2/+2
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-3/+3
* Remove some useless "Require".xleroy2012-12-301-1/+0
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-35/+16
* Merge of the newmem branch:xleroy2012-05-211-0/+712
generated by cgit (git 2.34.1) at 2024-05-09 13:25:29 +0000