aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Selection.v
Commit message (Expand)AuthorAgeFilesLines
* Ignore self assign in if-conversionBernhard Schommer2023-02-201-1/+5
* Update doc commentXavier Leroy2022-12-081-2/+2
* Recognize more if-then-else statements that can be if-convertedXavier Leroy2022-09-051-3/+8
* Add support for __builtin_fabsfXavier Leroy2020-07-271-0/+2
* Eliminate known builtins whose result is ignoredXavier Leroy2020-06-251-6/+15
* Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-171-6/+47
* If-conversion optimizationXavier Leroy2019-06-061-9/+84
* 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
* Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...xleroy2008-05-301-0/+1
* Meilleure selection pour if ((a && b) != 0), etcxleroy2008-03-271-7/+86
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+12
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...xleroy2007-08-281-16/+9
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-0/+1103
generated by cgit (git 2.34.1) at 2024-06-02 22:16:20 +0000