aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Selection.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-6/+17
|\
| * Add support for __builtin_fabsfXavier Leroy2020-07-271-0/+2
| * Eliminate known builtins whose result is ignoredXavier Leroy2020-06-251-6/+15
* | __builtin_expect seems to workDavid Monniaux2020-04-071-11/+30
* | start implementing expect as exprDavid Monniaux2020-04-071-1/+2
* | __builtin_expect defined as its first argumentDavid Monniaux2019-09-251-1/+2
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-07-191-9/+47
|\|
| * 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
* | 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
generated by cgit (git 2.34.1) at 2024-05-09 05:24:24 +0000