aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Selection.v
Commit message (Expand)AuthorAgeFilesLines
* rm old select/selectl/selectf/selectfsDavid Monniaux2019-06-031-61/+0
* Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-...David Monniaux2019-06-031-10/+83
|\
| * If-conversion optimizationXavier Leroy2019-05-311-9/+84
* | preparing for the builtin connectorDavid Monniaux2019-04-051-3/+69
* | removed the unproved hack to get builtins, will be reinstated laterDavid Monniaux2019-04-051-66/+6
* | Oselectf, Oselectfs with conditionDavid Monniaux2019-04-051-8/+2
* | selectl with conditionDavid Monniaux2019-04-051-4/+1
* | more on selectDavid Monniaux2019-04-041-4/+1
* | select_soundDavid Monniaux2019-04-041-1/+1
* | ternary ops for float/doubleDavid Monniaux2019-04-031-2/+34
* | problem in ValueAOpDavid Monniaux2019-04-031-1/+17
* | begin implementing ternary builtinDavid Monniaux2019-04-031-4/+13
* | selection of builtin.. progress...David Monniaux2019-04-031-13/+14
* | some more on builtinsDavid Monniaux2019-04-031-3/+14
* | attempts at generating builtins, startDavid Monniaux2019-04-031-3/+6
* | ça recompile sur x86David Monniaux2019-03-221-1/+1
* | la division flottante fonctionneDavid Monniaux2019-03-201-1/+4
* | added helper functions but strangeDavid Monniaux2019-03-191-1/+6
|/
* Prefixed runtime functions.Bernhard Schommer2017-08-251-15/+15
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-2/+2
* Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-041-1/+4
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-021-3/+3
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-36/+28
* Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-37/+31
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-6/+6
* Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-111-21/+89
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-17/+25
* Updated the Caml part. Added some more tests in annot1.c.Xavier Leroy2015-03-271-1/+12
* Extend annotations so that they can keep track of global variables and local ...Xavier Leroy2015-03-271-1/+9
* Protect against redefinition of the __i64_xxx helper library functions.Xavier Leroy2015-01-201-27/+26
* - Support "switch" statements over 64-bit integersxleroy2014-08-171-33/+94
* Merge of "newspilling" branch:xleroy2014-07-231-0/+15
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-0/+1
* Treat casts int64 -> float32 as primitive operations instead of twoxleroy2013-07-031-0/+2
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-291-7/+9
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-9/+44
* Remove some useless "Require".xleroy2012-12-301-4/+0
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-061-50/+6
* Merge of the newmem branch:xleroy2012-05-211-10/+20
* Take advantage of Cmaskzero and Cmasknotzero.xleroy2012-02-241-1/+4
* Merge of the "volatile" branch:xleroy2012-02-041-0/+3
* Revised handling of annotation statements, and more generally built-in functi...xleroy2011-06-131-1/+1
* Merge of branch "unsigned-offsets":xleroy2011-04-091-1/+1
* Merge of the reuse-temps branch:xleroy2010-09-021-2/+2
* Support for inlined built-ins.xleroy2010-06-291-12/+39
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-1/+1
* Forgot to add some filesxleroy2009-08-181-0/+212
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-1196/+0
* Flag to turn on/off the recognition of fused multiply-add and multiply-subxleroy2008-07-311-14/+20
* Fusion partielle de la branche contsem: xleroy2008-07-081-2/+4
generated by cgit (git 2.34.1) at 2024-07-06 17:59:23 +0000