aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-08-281-2/+0
|\
| * Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-051-2/+0
* | various fixesDavid Monniaux2019-07-193-24/+4
* | helpers broke compilationDavid Monniaux2019-07-192-11/+0
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-07-1917-128/+466
|\|
| * Improve CSE for known built-in functionsXavier Leroy2019-07-172-7/+14
| * Perform constant propagation for known built-in functionsXavier Leroy2019-07-174-16/+168
| * Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-173-112/+231
| * Compatibility with OCaml 4.08 (#302)Xavier Leroy2019-07-086-7/+6
| * Rename option `-ffavor-branchless` into `-Obranchless`Xavier Leroy2019-07-051-3/+3
| * Extended asm: print register names according to their typesXavier Leroy2019-06-171-9/+14
* | finish merging master branch (fixes problems in glpk colamd)David Monniaux2019-06-063-43/+0
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-workDavid Monniaux2019-06-063-5/+59
|\|
| * Cminortyping: relax typechecking of function callsXavier Leroy2019-06-061-12/+15
| * If-conversion optimizationXavier Leroy2019-06-064-72/+584
| * Type inference and type checking for CminorXavier Leroy2019-06-061-0/+797
* | start to have whole path if-conversion?David Monniaux2019-06-041-1/+1
* | rm old select/selectl/selectf/selectfsDavid Monniaux2019-06-032-64/+3
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-...David Monniaux2019-06-0321-150/+1552
|\ \
| * | ARM: select is not supported at type TlongXavier Leroy2019-06-011-2/+3
| * | If-conversion optimizationXavier Leroy2019-05-314-72/+579
| * | Type inference and type checking for CminorXavier Leroy2019-05-311-0/+798
| |/
| * Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-314-5/+5
| * Support a "select" operation between two valuesXavier Leroy2019-05-202-0/+86
| * Added options -fcommon and -fno-common (#164)Bernhard Schommer2019-05-101-0/+8
| * Change to AbsInt version string.Bernhard Schommer2019-05-102-2/+2
| * Expand the responsefiles earlierBernhard Schommer2019-05-102-4/+4
| * Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-263-20/+21
| * lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-235-20/+22
| * Replace nat_of_Z with Z.to_natXavier Leroy2019-04-235-17/+17
| * Print only debug info for printed functions.Bernhard Schommer2019-04-161-1/+2
| * Typo in comment about Ijumptable in RTL.vAlix Trieu2019-04-151-1/+1
| * Fix typo in section name in Selectionproof.v Alix Trieu2019-04-151-2/+2
| * RTLgenproof: destruct too deepXavier Leroy2019-03-251-2/+2
| * Minor simplifications in two proofs. (#280)Vincent Laporte2019-03-251-2/+2
* | itemize the proof (better for debugging)David Monniaux2019-04-051-10/+10
* | preparing for the builtin connectorDavid Monniaux2019-04-051-3/+69
* | removed the unproved hack to get builtins, will be reinstated laterDavid Monniaux2019-04-052-72/+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-032-3/+20
* | attempts at generating builtins, startDavid Monniaux2019-04-031-3/+6
* | ça recompile sur x86David Monniaux2019-03-228-3/+127
* | Merge branch 'mppa_postpass' into mppa-mulDavid Monniaux2019-03-223-8/+4
|\ \
generated by cgit (git 2.34.1) at 2024-06-03 00:25:57 +0000